fact: Definition IncoherentWeakUnivalence := { 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 }.
imports: HoTT.Basics HoTT.Types Idempotents Metatheory.Core