jc_factors@{} : jc_factor2 o jc_factor1 == f. Admitted. Global Instance jc_factor1_issurj@{} : IsSurjection jc_factor1. Admitted. Global Instance jc_factor2_isemb : IsEmbedding jc_factor2. Admitted. End JoinConstruction. Fail Goal forall (O : ReflectiveSubuniverse), In (Sep O) (Type_ O). Global Instance SepO_lex_leq `{Univalence} (O : ReflectiveSubuniverse) {X : Type} `{Reflects (Sep O) X} : Descends (Sep O) O X. Proof. assert (e : forall (P : X -> Type_ O), { Q : (O_reflector (Sep O) X -> Type_ O) & forall x, Q (to (Sep O) X x) <~> P x }). 2:{ unshelve econstructor; intros P' P_inO; pose (P := fun x => (P' x; P_inO x) : Type_ O); pose (ee := e P). - exact ee.1. - simpl; exact _. - intros x; cbn; apply ee.2. } intros P. assert (ls : forall A B : Type_ O, { Z : Type & Z <~> (A = B) }). { intros A B. pose (q := almost_inSepO_typeO O A B). exact (q.1; snd q.2). } pose (p := jc_factor2 P ls). set (J := jc_image P ls) in p. assert (In (Sep O) J). { intros x y. pose (q := almost_inSepO_typeO O (p x) (p y)). refine (inO_equiv_inO' q.1 _). refine (_ oE _). - symmetry; srapply (equiv_ap_isembedding p). - exact (snd q.2). } pose (O_rec (O := Sep O) (jc_factor1 P ls)). exists (p o j). intros x; subst p j. rewrite O_rec_beta. apply equiv_path. exact ((jc_factors P ls x)..1). Defined.
Require Import HoTT.Basics HoTT.Types HoTT.Cubical.DPath. Require Import HFiber Extensions Factorization Limits.Pullback. Require Import Modality Accessible Descent. Require Import Truncations.Core. Require Import Homotopy.Suspension.