(n : nat) (A : Type) `{IsConnected O A} (C : Type) `{In O C} : ExtendableAlong n (const_tt A) (fun _ => C). Proof. generalize dependent C; simple_induction n n IHn; intros C ?; [ exact tt | split ]. - intros f. exists (fun _ : Unit => (isconnected_elim C f).1); intros a. symmetry; apply ((isconnected_elim C f).2). - intros h k. refine (extendable_postcompose' n _ _ _ _ (IHn (h tt = k tt) (inO_paths _ _ _ _))). intros []; apply equiv_idmap. 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.