{O' : Subuniverse} (O : Subuniverse) {A:Type} `{Reflects O' A} (B: O_reflector O' A -> Type) {inO_sigma : In O' {z:O_reflector O' A & B z}} (g : forall x, B (to O' A x)) : ExtensionAlong (to O' A) B g. Proof. set (Z := sig B) in *. pose (g' := (fun a:A => (to O' A a ; g a)) : A -> Z). pose (f' := O_rec (O := O') g'). pose (eqf := (O_rec_beta g') : f' o to O' A == g'). pose (eqid := O_indpaths (pr1 o f') idmap (fun x => ap@{k i} pr1 (eqf x))). exists (fun z => transport B (eqid z) ((f' z).2)). intros a. unfold eqid. refine (_ @ pr2_path (O_rec_beta g' a)). refine (ap (fun p => transport B p (O_rec g' (to O' A a)).2) _). srapply O_indpaths_beta. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Factorization Limits.Pullback.