{ etop : forall A B, (A <~> B) -> (A = B) & forall A B (f : A <~> B), equiv_path A B (etop A B f) = f }.
Require Import HoTT.Basics HoTT.Types. Require Import Idempotents. Require Import Metatheory.Core.