{O' : ReflectiveSubuniverse} (O : Subuniverse) {A : Type} (B: O_reflector O' A -> Type) {inO_sigma : In O' {z:O_reflector O' A & B z}} : ooExtendableAlong (to O' A) B. Proof. intros n; generalize dependent A. induction n as [|n IHn]; intros; [ exact tt | cbn ]. refine (extension_from_inO_sigma O B , _). intros h k; nrapply IHn. set (Z := sig B) in *. pose (W := sig (fun a => B a * B a)). nrefine (inO_equiv_inO' (Pullback (A := W) (fun a:O_reflector O' A => (a;(h a,k a))) (fun z:Z => (z.1;(z.2,z.2)))) _). { refine (inO_pullback O' _ _). exact (inO_equiv_inO' _ (equiv_sigprod_pullback B B)^-1). } unfold Pullback. apply equiv_functor_sigma_id; intros z; cbn. refine (_ oE equiv_functor_sigma_id _). 2:intros; symmetry; apply equiv_path_sigma. refine (_ oE equiv_functor_sigma_id (fun z => equiv_functor_sigma_id (fun p => _))). 2:symmetry; apply equiv_path_prod. cbn. make_equiv_contr_basedpaths. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Factorization Limits.Pullback.