(H : forall {A B C D} (f : A -> B) (g : C -> D) (h : A -> C) (k : B -> D), (IsConnMap O f) -> (IsConnMap O g) -> (MapIn O h) -> (MapIn O k) -> forall (p : k o f == g o h), IsPullback p) : Lex O. Proof. apply lex_from_isequiv_ismodal_isconnected_types. intros A B f AC BC fM. specialize (H A Unit B Unit (const_tt _) (const_tt _) f idmap _ _ _ _ (fun _ => 1)). unfold IsPullback, pullback_corec in H. refine (@isequiv_compose _ _ _ H _ (fun x => x.2.1) _). unfold Pullback. refine (@isequiv_compose _ {b:Unit & B} (functor_sigma idmap (fun a => pr1)) _ _ pr2 _). refine (@isequiv_compose _ _ (equiv_sigma_prod0 Unit B) _ _ snd _). apply (equiv_isequiv (prod_unit_l B)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. Require Import Modality Accessible Modalities.Localization Descent Separated.