ap_O_path_universe' `{Univalence} {A B : Type} (f : A <~> B) : ap O (path_universe_uncurried f) = path_universe_uncurried (equiv_O_functor f). Proof. revert f. equiv_intro (equiv_path A B) p. refine (ap (ap O) (eta_path_universe p) @ _). destruct p; simpl. apply moveL_equiv_V. apply path_equiv, path_arrow, O_indpaths; intros x. symmetry; apply to_O_natural. 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.