{ etop : forall A B (f : A -> B) (g : B -> A), (f o g == idmap) -> (g o f == idmap) -> (A = B) & forall A B f g H K, equiv_path A B (etop A B f g H K) == f }.
Require Import HoTT.Basics HoTT.Types. Require Import Idempotents. Require Import Metatheory.Core.