`{Univalence} (O1 O2 : Subuniverse) : (O1 <=> O2) <~> (O1 = O2). Proof. refine (_ oE (issig_O_eq O1 O2)^-1). revert O1 O2; refine (equiv_path_along_equiv issig_subuniverse _). cbn; intros O1 O2. refine (equiv_path_sigma_hprop O1 O2 oE _). destruct O1 as [O1 [O1h ?]]; destruct O2 as [O2 [O2h ?]]; cbn. refine (equiv_path_arrow _ _ oE _). srapply (equiv_iff_hprop). - srapply istrunc_sigma; unfold O_leq; exact _. - intros [h k] A; specialize (h A); specialize (k A); cbn in *. apply path_universe_uncurried, equiv_iff_hprop; assumption. - intros h; split; intros A e; specialize (h A); cbn in *. 1:rewrite <- h. 2:rewrite h. all:exact e. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.