`{Univalence} {A B : Type} (e : A <~> B) : comp (A <~> B) (tr e) <~> comp (A -> B) (tr (equiv_fun e)). Proof. refine (_ oE equiv_functor_O_cover (issig_equiv _ _)^-1 _); cbn. rapply equiv_comp_property. Defined.
Require Import Basics Types HFiber Truncations.Core Truncations.SeparatedTrunc Pointed