`{Univalence} {A B : Type} (f : A -> B) `{IsEquiv _ _ f} : ap O (path_universe f) = path_universe (O_functor f) := ' (Build_Equiv _ _ f _).
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.