`{Univalence} {A B : Type} (f : A -> B) `{IsConnMap O _ _ f} (extP : forall P : A -> Type_ O, ExtensionAlong f (fun _ : B => Type_ O) P) : ooExtendableAlong f (fun _ => Type_ O). Proof. intros [|[|n]]. - exact tt. - split; [ apply extP | intros; exact tt ]. - split; [ apply extP | ]. intros P Q; rapply (ooextendable_postcompose' (fun b => P b <~> Q b)). + intros x; refine (equiv_path_TypeO _ _ _ oE equiv_path_universe _ _). + rapply ooextendable_conn_map_inO. 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.