(* -*- mode: coq; mode: visual-line -*- *)
Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback.
Require Import Descent Lex Separated.

(** We construct "canonical" binary meets of reflective subuniverses (that is, whose underlying subuniverse is an intersection), without assuming accessibility.  In particular, we will show:

1. Given two reflective subuniverses L and O, if [L O X] is [O]-modal, then it is a reflection into the canonical meet.  In particular, this is always the case if [L] preserves [O]-modal types; this is Theorem 3.30 of RSS.

1. If L and O are lex modalities satisfying an additional "composability" condition, then the composite functor [L o O] converges to a reflection into the canonical meet after n+2 applications when applied to an n-type for some finite n.

The latter gives in particular a synthetic approach to higher sheafification (stack completion).  As described at https://ncatlab.org/nlab/show/plus+construction+on+presheaves, for any site C the topos of presheaves on its Grothendieck topology is cohesive and even totally connected, so that its shape and sharp modalities are both lex.  Their canonical meet is the topos of sheaves for the given topology, and the composite functor [shape o sharp] is the usual "plus construction" on (higher) presheaves.  Thus, we recover synthetically the result that an n-truncated type can be stackified by (n+2) applications of the plus construction.  We also refer to [L o O] as a "plus construction" in the general case of reflective subuniverses.  *)

Section RSUMeet.
  Context (L O : ReflectiveSubuniverse).

  (** The canonical meet of two subuniverses is their intersection. *)

  Definition Meet : Subuniverse.
L, O: ReflectiveSubuniverse
Subuniverse
  Proof.
L, O: ReflectiveSubuniverse
Subuniverse
    unshelve econstructor.
L, O: ReflectiveSubuniverse
Type -> Type
L, O: ReflectiveSubuniverse
Funext -> forall T : Type, IsHProp (?In_internal T)
L, O: ReflectiveSubuniverse
forall T U : Type,
?In_internal T ->
forall f : T -> U, IsEquiv f -> ?In_internal U
    -
L, O: ReflectiveSubuniverse
Type -> Type intros X; exact (In L X * In O X).
    -
L, O: ReflectiveSubuniverse
Funext ->
forall T : Type,
IsHProp ((fun X : Type => In L X * In O X) T) intros ? X; exact _.
    -
L, O: ReflectiveSubuniverse
forall T U : Type,
(fun X : Type => In L X * In O X) T ->
forall f : T -> U,
IsEquiv f -> (fun X : Type => In L X * In O X) U intros T U [? ?] f feq; split; apply (inO_equiv_inO _ f).
  Defined.

  Global Instance inO_inmeet_l (X : Type) `{im : In Meet X} : In L X := fst im.
  Global Instance inO_inmeet_r (X : Type) `{im : In Meet X} : In O X := snd im.

  (** The basic tool in studying its reflectivity is the "plus construction" that applies the two reflectors in sequence. *)

  Definition Plus (X : Type) := L (O X).

  Global Instance inO_plus_l (X : Type) : In L (Plus X) := _.

  (** This is not necessarily a reflector, but it is a well-pointed endofunctor. *)

  Definition to_plus (X : Type) : X -> Plus X
    := to L (O X) o to O X.

  Definition plus_functor {X Y : Type} (f : X -> Y) : Plus X -> Plus Y
    := O_functor L (O_functor O f).

  Definition to_plus_natural {X Y : Type} (f : X -> Y)
    : plus_functor f o to_plus X == to_plus Y o f.
L, O: ReflectiveSubuniverse
X, Y: Type
f: X -> Y
plus_functor f o to_plus X == to_plus Y o f
  Proof.
L, O: ReflectiveSubuniverse
X, Y: Type
f: X -> Y
plus_functor f o to_plus X == to_plus Y o f
    intros x.
L, O: ReflectiveSubuniverse
X, Y: Type
f: X -> Y
x: X
plus_functor f (to_plus X x) = to_plus Y (f x)
    unfold plus_functor, to_plus.
L, O: ReflectiveSubuniverse
X, Y: Type
f: X -> Y
x: X
O_functor L (O_functor O f) (to L (O X) (to O X x)) =
to L (O Y) (to O Y (f x))
    refine (to_O_natural L (O_functor O f) (to O X x) @ _).
L, O: ReflectiveSubuniverse
X, Y: Type
f: X -> Y
x: X
to L (O Y) (O_functor O f (to O X x)) =
to L (O Y) (to O Y (f x))
    apply ap.
L, O: ReflectiveSubuniverse
X, Y: Type
f: X -> Y
x: X
O_functor O f (to O X x) = to O Y (f x)
    apply to_O_natural.
  Defined.

  Definition wellpointed_plus (X : Type)
    : to_plus (Plus X) == plus_functor (to_plus X).
L, O: ReflectiveSubuniverse
X: Type
to_plus (Plus X) == plus_functor (to_plus X)
  Proof.
L, O: ReflectiveSubuniverse
X: Type
to_plus (Plus X) == plus_functor (to_plus X)
    rapply (@O_indpaths L).
L, O: ReflectiveSubuniverse
X: Type
(fun x : O X => to_plus (Plus X) (to L (O X) x)) ==
(fun x : O X =>
 plus_functor (to_plus X) (to L (O X) x))
    intros ox.
L, O: ReflectiveSubuniverse
X: Type
ox: O X
to_plus (Plus X) (to L (O X) ox) =
plus_functor (to_plus X) (to L (O X) ox)
    unfold to_plus, plus_functor; cbn.
L, O: ReflectiveSubuniverse
X: Type
ox: O X
to L (O (Plus X)) (to O (Plus X) (to L (O X) ox)) =
O_functor L
  (O_functor O (fun x : X => to L (O X) (to O X x)))
  (to L (O X) ox)
    refine (_ @ (to_O_natural L _ ox)^).
L, O: ReflectiveSubuniverse
X: Type
ox: O X
to L (O (Plus X)) (to O (Plus X) (to L (O X) ox)) =
to L (O (Plus X))
  (O_functor O (fun x : X => to L (O X) (to O X x)) ox)
    apply ap.
L, O: ReflectiveSubuniverse
X: Type
ox: O X
to O (Plus X) (to L (O X) ox) =
O_functor O (fun x : X => to L (O X) (to O X x)) ox
    revert ox; apply O_indpaths; intros x.
L, O: ReflectiveSubuniverse
X: Type
x: X
to O (Plus X) (to L (O X) (to O X x)) =
O_functor O (fun x : X => to L (O X) (to O X x))
  (to O X x)
    exact ((to_O_natural O _ x)^).
  Defined.

  (** Moreover, it has the desired factorization property of a reflector (though it may not belong to the meet subuniverse itself). *)

  Definition ooextendable_plus {X Y : Type} `{In Meet Y}
    : ooExtendableAlong (to_plus X) (fun _  => Y).
L, O: ReflectiveSubuniverse
X, Y: Type
H: In Meet Y
ooExtendableAlong (to_plus X) (fun _ : Plus X => Y)
  Proof.
L, O: ReflectiveSubuniverse
X, Y: Type
H: In Meet Y
ooExtendableAlong (to_plus X) (fun _ : Plus X => Y)
    apply (ooextendable_compose _ (to O X) (to L (O X)));
      rapply extendable_to_O.
  Defined.

  Definition plus_rec {P Q : Type} `{In Meet Q} (f : P -> Q)
    : Plus P -> Q
    := (fst (ooextendable_plus 1%nat) f).1.

  Definition plus_rec_beta {P Q : Type} `{In Meet Q} (f : P -> Q) (x : P)
    : plus_rec f (to_plus P x) = f x
    := (fst (ooextendable_plus 1%nat) f).2 x.

  Definition plus_indpaths {P Q : Type} `{In Meet Q} (g h : Plus P -> Q)
             (p : g o to_plus P == h o to_plus P)
    : g == h
    := (fst (snd (ooextendable_plus 2%nat) g h) p).1.

  Definition plus_indpaths_beta {P Q : Type} `{In Meet Q} (g h : Plus P -> Q)
             (p : g o (to_plus P) == h o (to_plus P)) (x : P)
    : plus_indpaths g h p (to_plus P x) = p x
    := (fst (snd (ooextendable_plus 2%nat) g h) p).2 x.

  (** Moreover, its fixed points, as a pointed endofunctor, are the types in the meet. *)

  Definition isequiv_plus_inmeet (X : Type) `{In Meet X} : IsEquiv (to_plus X).
L, O: ReflectiveSubuniverse
X: Type
H: In Meet X
IsEquiv (to_plus X)
  Proof.
L, O: ReflectiveSubuniverse
X: Type
H: In Meet X
IsEquiv (to_plus X)
    apply (@isequiv_compose _ _ (to O X) _ _ (to L (O X))).
L, O: ReflectiveSubuniverse
X: Type
H: In Meet X
IsEquiv (to L (O X))
    apply isequiv_to_O_inO.
L, O: ReflectiveSubuniverse
X: Type
H: In Meet X
In L (O X)
    apply (inO_equiv_inO X (to O X)).
  Defined.

  Definition inmeet_isequiv_plus (X : Type) `{IsEquiv _ _ (to_plus X)} : In Meet X.
L, O: ReflectiveSubuniverse
X: Type
H: IsEquiv (to_plus X)
In Meet X
  Proof.
L, O: ReflectiveSubuniverse
X: Type
H: IsEquiv (to_plus X)
In Meet X
    split.
L, O: ReflectiveSubuniverse
X: Type
H: IsEquiv (to_plus X)
In L X
L, O: ReflectiveSubuniverse
X: Type
H: IsEquiv (to_plus X)
In O X
    -
L, O: ReflectiveSubuniverse
X: Type
H: IsEquiv (to_plus X)
In L X apply (inO_equiv_inO (Plus X) (to_plus X)^-1).
    -
L, O: ReflectiveSubuniverse
X: Type
H: IsEquiv (to_plus X)
In O X srapply inO_to_O_retract.
L, O: ReflectiveSubuniverse
X: Type
H: IsEquiv (to_plus X)
O X -> X
L, O: ReflectiveSubuniverse
X: Type
H: IsEquiv (to_plus X)
?mu o to O X == idmap
      +
L, O: ReflectiveSubuniverse
X: Type
H: IsEquiv (to_plus X)
O X -> X exact ((to_plus X)^-1 o (to L (O X))).
      +
L, O: ReflectiveSubuniverse
X: Type
H: IsEquiv (to_plus X)
(to_plus X)^-1 o to L (O X) o to O X == idmap intros x; apply (eissect (to_plus X)).
  Defined.

  (** It follows that if [Plus X] ever *does* lie in the meet, then it is a reflection. *)

  Global Instance prereflects_plus_inO (X : Type) `{In O (Plus X)}
    : PreReflects Meet X.
L, O: ReflectiveSubuniverse
X: Type
H: In O (Plus X)
PreReflects Meet X
  Proof.
L, O: ReflectiveSubuniverse
X: Type
H: In O (Plus X)
PreReflects Meet X
    unshelve econstructor.
L, O: ReflectiveSubuniverse
X: Type
H: In O (Plus X)
Type
L, O: ReflectiveSubuniverse
X: Type
H: In O (Plus X)
In Meet ?O_reflector
L, O: ReflectiveSubuniverse
X: Type
H: In O (Plus X)
X -> ?O_reflector
    -
L, O: ReflectiveSubuniverse
X: Type
H: In O (Plus X)
Type exact (Plus X).
    -
L, O: ReflectiveSubuniverse
X: Type
H: In O (Plus X)
In Meet (Plus X) split; exact _.
    -
L, O: ReflectiveSubuniverse
X: Type
H: In O (Plus X)
X -> Plus X apply to_plus.
  Defined.

  Global Instance reflects_plus_inO (X : Type) `{In O (Plus X)}
    : Reflects Meet X.
L, O: ReflectiveSubuniverse
X: Type
H: In O (Plus X)
Reflects Meet X
  Proof.
L, O: ReflectiveSubuniverse
X: Type
H: In O (Plus X)
Reflects Meet X
    constructor; intros; apply ooextendable_plus.
  Defined.

  (** Recalling that a type is connected for a reflective subuniverse if and only if its reflector is nullhomotopic, we define a type to be "plus-connected" if its map to plus is nullhomotopic.  If the meet is reflective, this coincides with connectedness for that reflective subuniverse. *)

  Definition PlusConnected (X : Type) := NullHomotopy (to_plus X).

  Definition plusconnected_equiv {X Y : Type} (f : X <~> Y)
    : PlusConnected X -> PlusConnected Y.
L, O: ReflectiveSubuniverse
X, Y: Type
f: X <~> Y
PlusConnected X -> PlusConnected Y
  Proof.
L, O: ReflectiveSubuniverse
X, Y: Type
f: X <~> Y
PlusConnected X -> PlusConnected Y
    intros [px e].
L, O: ReflectiveSubuniverse
X, Y: Type
f: X <~> Y
px: Plus X
e: forall x : X, to_plus X x = px
PlusConnected Y
    exists (plus_functor f px); intros y.
L, O: ReflectiveSubuniverse
X, Y: Type
f: X <~> Y
px: Plus X
e: forall x : X, to_plus X x = px
y: Y
to_plus Y y = plus_functor f px
    refine (_ @ ap (plus_functor f) (e (f^-1 y))).
L, O: ReflectiveSubuniverse
X, Y: Type
f: X <~> Y
px: Plus X
e: forall x : X, to_plus X x = px
y: Y
to_plus Y y = plus_functor f (to_plus X (f^-1 y))
    rewrite to_plus_natural.
L, O: ReflectiveSubuniverse
X, Y: Type
f: X <~> Y
px: Plus X
e: forall x : X, to_plus X x = px
y: Y
to_plus Y y = to_plus Y (f (f^-1 y))
    symmetry; apply ap, eisretr.
  Defined.

  (** Similarly, we say a map is plus-connected if all of its fibers are. *)

  Definition PlusConnMap {X Y : Type} (f : X -> Y) := forall y, PlusConnected (hfiber f y).

End RSUMeet.

(** Let's now assume we are trying to intersect two lex modalities. *)

Section LexMeet.
  Context (L O : Modality) `{Lex L} `{Lex O}.

  (** The plus construction, being a composite of two lex functors, is also lex.  Thus, it preserves path-types. *)
  Definition plus_path {X : Type} (x y : X)
    : Plus L O (x = y) <~> (to_plus L O X x = to_plus L O X y).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x, y: X
Plus L O (x = y) <~> to_plus L O X x = to_plus L O X y
  Proof.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x, y: X
Plus L O (x = y) <~> to_plus L O X x = to_plus L O X y
    refine (equiv_path_O L (to O X x) (to O X y) oE _).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x, y: X
Plus L O (x = y) <~> L (to O X x = to O X y)
    apply equiv_O_functor.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x, y: X
O (x = y) <~> to O X x = to O X y
    rapply equiv_path_O.
  Defined.

  Definition plus_path_to_plus {X : Type} (x y : X)
    : plus_path x y o to_plus L O (x = y) == @ap _ _ (to_plus L O X) x y.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x, y: X
plus_path x y o to_plus L O (x = y) ==
ap (to_plus L O X)
  Proof.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x, y: X
plus_path x y o to_plus L O (x = y) ==
ap (to_plus L O X)
    intros p; unfold plus_path, to_plus, equiv_path_O, equiv_path_OO, path_OO.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x, y: X
p: x = y
({|
   equiv_fun := O_rec (ap (to L (O_reflector O X)));
   equiv_isequiv :=
     isequiv_path_OO L L (to O X x) (to O X y)
 |}
 oE equiv_O_functor L
      {|
        equiv_fun := O_rec (ap (to O X));
        equiv_isequiv := isequiv_path_OO O O x y
      |}) (to L (O (x = y)) (to O (x = y) p)) =
ap (fun x : X => to L (O X) (to O X x)) p
    cbn.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x, y: X
p: x = y
O_rec
  (ap
     (to (modality_subuniv L)
        (O_reflector (modality_subuniv O) X)))
  (O_functor L
     (O_rec (ap (to (modality_subuniv O) X)))
     (to (modality_subuniv L) (O (x = y))
        (to (modality_subuniv O) (x = y) p))) =
ap
  (fun x : X =>
   to (modality_subuniv L) (O X)
     (to (modality_subuniv O) X x)) p
    rewrite to_O_natural.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x, y: X
p: x = y
O_rec
  (ap
     (to (modality_subuniv L)
        (O_reflector (modality_subuniv O) X)))
  (to L
     (to (modality_subuniv O) X x =
      to (modality_subuniv O) X y)
     (O_rec (ap (to (modality_subuniv O) X))
        (to (modality_subuniv O) (x = y) p))) =
ap
  (fun x : X =>
   to (modality_subuniv L) (O X)
     (to (modality_subuniv O) X x)) p
    rewrite O_rec_beta.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x, y: X
p: x = y
ap
  (to (modality_subuniv L)
     (O_reflector (modality_subuniv O) X))
  (O_rec (ap (to (modality_subuniv O) X))
     (to (modality_subuniv O) (x = y) p)) =
ap
  (fun x : X =>
   to (modality_subuniv L) (O X)
     (to (modality_subuniv O) X x)) p
    rewrite (ap_compose (to O X) (to L (O X))).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x, y: X
p: x = y
ap
  (to (modality_subuniv L)
     (O_reflector (modality_subuniv O) X))
  (O_rec (ap (to (modality_subuniv O) X))
     (to (modality_subuniv O) (x = y) p)) =
ap (to L (O X)) (ap (to O X) p)
    apply ap.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x, y: X
p: x = y
O_rec (ap (to (modality_subuniv O) X))
  (to (modality_subuniv O) (x = y) p) = ap (to O X) p
    apply O_rec_beta.
  Defined.

  (** This implies that plus-connected types are closed under path-spaces. *)
  Definition plusconnected_path {X : Type} (x y : X)
             (pc : PlusConnected L O X) : PlusConnected L O (x = y).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x, y: X
pc: PlusConnected L O X
PlusConnected L O (x = y)
  Proof.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x, y: X
pc: PlusConnected L O X
PlusConnected L O (x = y)
    unfold PlusConnected in *.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x, y: X
pc: NullHomotopy (to_plus L O X)
NullHomotopy (to_plus L O (x = y))
    apply (cancelL_nullhomotopy_equiv _ (plus_path x y)).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x, y: X
pc: NullHomotopy (to_plus L O X)
NullHomotopy
  (fun x0 : x = y =>
   plus_path x y (to_plus L O (x = y) x0))
    apply (nullhomotopy_homotopic (fun u => (plus_path_to_plus x y u)^)).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x, y: X
pc: NullHomotopy (to_plus L O X)
NullHomotopy (ap (to_plus L O X))
    apply nullhomotopy_ap; assumption.
  Defined.

  (** And hence plus-connected maps are closed under diagonals. *)
  Definition plusconnmap_diagonal {X Y : Type} (f : X -> Y)
    : PlusConnMap L O f -> PlusConnMap L O (diagonal f).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
PlusConnMap L O f -> PlusConnMap L O (diagonal f)
  Proof.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
PlusConnMap L O f -> PlusConnMap L O (diagonal f)
    intros pc p.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
pc: PlusConnMap L O f
p: Pullback f f
PlusConnected L O (hfiber (diagonal f) p)
    refine (plusconnected_equiv L O (hfiber_diagonal f p)^-1 _).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
pc: PlusConnMap L O f
p: Pullback f f
PlusConnected L O ((p.1; (p.2).2) = ((p.2).1; 1))
    apply plusconnected_path, pc.
  Defined.

  (** The plus-construction also preserves fibers. *)
  Definition plus_hfiber {X Y : Type} (f : X -> Y) (y : Y)
    : Plus L O (hfiber f y) <~> hfiber (plus_functor L O f) (to_plus L O Y y).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
y: Y
Plus L O (hfiber f y) <~>
hfiber (plus_functor L O f) (to_plus L O Y y)
  Proof.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
y: Y
Plus L O (hfiber f y) <~>
hfiber (plus_functor L O f) (to_plus L O Y y)
    refine (equiv_O_functor_hfiber L (O_functor O f) (to O Y y) oE _).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
y: Y
Plus L O (hfiber f y) <~>
L (hfiber (O_functor O f) (to O Y y))
    apply equiv_O_functor.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
y: Y
O (hfiber f y) <~> hfiber (O_functor O f) (to O Y y)
    rapply equiv_O_functor_hfiber.
  Defined.

  Definition plus_hfiber_to_plus {X Y : Type} (f : X -> Y) (y : Y)
    : plus_hfiber f y o to_plus L O (hfiber f y)
      == functor_hfiber (fun u => (to_plus_natural L O f u)^) y.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
y: Y
plus_hfiber f y o to_plus L O (hfiber f y) ==
functor_hfiber
  (fun u : X => (to_plus_natural L O f u)^) y
  Proof.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
y: Y
plus_hfiber f y o to_plus L O (hfiber f y) ==
functor_hfiber
  (fun u : X => (to_plus_natural L O f u)^) y
    intros [x q]; unfold plus_hfiber, to_plus.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
y: Y
x: X
q: f x = y
(equiv_O_functor_hfiber L (O_functor O f) (to O Y y)
 oE equiv_O_functor L (equiv_O_functor_hfiber O f y))
  (to L (O (hfiber f y)) (to O (hfiber f y) (x; q))) =
functor_hfiber
  (fun u : X => (to_plus_natural L O f u)^) y (x; q)
    cbn.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
y: Y
x: X
q: f x = y
O_functor_hfiber L (O_functor O f)
  (to (modality_subuniv O) Y y)
  (O_functor L (O_functor_hfiber O f y)
     (to (modality_subuniv L) (O (hfiber f y))
        (to (modality_subuniv O) (hfiber f y) (x; q)))) =
functor_hfiber
  (fun u : X => (to_plus_natural L O f u)^) y (x; q)
    rewrite to_O_natural.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
y: Y
x: X
q: f x = y
O_functor_hfiber L (O_functor O f)
  (to (modality_subuniv O) Y y)
  (to L
     (hfiber (O_functor O f)
        (to (modality_subuniv O) Y y))
     (O_functor_hfiber O f y
        (to (modality_subuniv O) (hfiber f y) (x; q)))) =
functor_hfiber
  (fun u : X => (to_plus_natural L O f u)^) y (x; q)
    rewrite O_functor_hfiber_natural.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
y: Y
x: X
q: f x = y
functor_hfiber
  (fun u : O X => (to_O_natural L (O_functor O f) u)^)
  (to (modality_subuniv O) Y y)
  (O_functor_hfiber O f y
     (to (modality_subuniv O) (hfiber f y) (x; q))) =
functor_hfiber
  (fun u : X => (to_plus_natural L O f u)^) y (x; q)
    unfold O_functor_hfiber, functor_hfiber, functor_sigma; cbn.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
y: Y
x: X
q: f x = y
(to (modality_subuniv L) (O X)
   (O_rec
      (fun X0 : hfiber f y =>
       (to (modality_subuniv O) X X0.1;
       to_O_natural O f X0.1 @
       ap (to (modality_subuniv O) Y) X0.2))
      (to (modality_subuniv O) (hfiber f y) (x; q))).1;
((to_O_natural L (O_functor O f)
    (O_rec
       (fun X0 : hfiber f y =>
        (to (modality_subuniv O) X X0.1;
        to_O_natural O f X0.1 @
        ap (to (modality_subuniv O) Y) X0.2))
       (to (modality_subuniv O) (hfiber f y) (x; q))).1)^)^ @
ap (to (modality_subuniv L) (O Y))
  (O_rec
     (fun X0 : hfiber f y =>
      (to (modality_subuniv O) X X0.1;
      to_O_natural O f X0.1 @
      ap (to (modality_subuniv O) Y) X0.2))
     (to (modality_subuniv O) (hfiber f y) (x; q))).2) =
(to (modality_subuniv L) (O X)
   (to (modality_subuniv O) X x);
((to_plus_natural L O f x)^)^ @
ap
  (fun x : Y =>
   to (modality_subuniv L) (O Y)
     (to (modality_subuniv O) Y x)) q)
    rewrite O_rec_beta; cbn.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
y: Y
x: X
q: f x = y
(to (modality_subuniv L) (O X)
   (to (modality_subuniv O) X x);
((to_O_natural L (O_functor O f)
    (to (modality_subuniv O) X x))^)^ @
ap (to (modality_subuniv L) (O Y))
  (to_O_natural O f x @
   ap (to (modality_subuniv O) Y) q)) =
(to (modality_subuniv L) (O X)
   (to (modality_subuniv O) X x);
((to_plus_natural L O f x)^)^ @
ap
  (fun x : Y =>
   to (modality_subuniv L) (O Y)
     (to (modality_subuniv O) Y x)) q)
    apply ap.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
y: Y
x: X
q: f x = y
((to_O_natural L (O_functor O f)
    (to (modality_subuniv O) X x))^)^ @
ap (to (modality_subuniv L) (O Y))
  (to_O_natural O f x @
   ap (to (modality_subuniv O) Y) q) =
((to_plus_natural L O f x)^)^ @
ap
  (fun x : Y =>
   to (modality_subuniv L) (O Y)
     (to (modality_subuniv O) Y x)) q
    unfold to_plus_natural.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
y: Y
x: X
q: f x = y
((to_O_natural L (O_functor O f)
    (to (modality_subuniv O) X x))^)^ @
ap (to (modality_subuniv L) (O Y))
  (to_O_natural O f x @
   ap (to (modality_subuniv O) Y) q) =
((to_O_natural L (O_functor O f) (to O X x) @
  ap (to L (O Y)) (to_O_natural O f x))^)^ @
ap
  (fun x : Y =>
   to (modality_subuniv L) (O Y)
     (to (modality_subuniv O) Y x)) q
    rewrite !inv_V, ap_pp, concat_p_pp.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
y: Y
x: X
q: f x = y
(to_O_natural L (O_functor O f)
   (to (modality_subuniv O) X x) @
 ap (to (modality_subuniv L) (O Y))
   (to_O_natural O f x)) @
ap (to (modality_subuniv L) (O Y))
  (ap (to (modality_subuniv O) Y) q) =
(to_O_natural L (O_functor O f) (to O X x) @
 ap (to L (O Y)) (to_O_natural O f x)) @
ap
  (fun x : Y =>
   to (modality_subuniv L) (O Y)
     (to (modality_subuniv O) Y x)) q
    apply whiskerL.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
y: Y
x: X
q: f x = y
ap (to (modality_subuniv L) (O Y))
  (ap (to (modality_subuniv O) Y) q) =
ap
  (fun x : Y =>
   to (modality_subuniv L) (O Y)
     (to (modality_subuniv O) Y x)) q
    rewrite <- ap_compose.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X, Y: Type
f: X -> Y
y: Y
x: X
q: f x = y
ap
  (fun x : Y =>
   to (modality_subuniv L) (O Y)
     (to (modality_subuniv O) Y x)) q =
ap
  (fun x : Y =>
   to (modality_subuniv L) (O Y)
     (to (modality_subuniv O) Y x)) q
    reflexivity.
  Defined.

  (** And pullbacks. *)
  Definition equiv_plus_pullback {A B C : Type} (f : B -> A) (g : C -> A)
    : Plus L O (Pullback f g) <~> Pullback (plus_functor L O f) (plus_functor L O g).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
A, B, C: Type
f: B -> A
g: C -> A
Plus L O (Pullback f g) <~>
Pullback (plus_functor L O f) (plus_functor L O g)
  Proof.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
A, B, C: Type
f: B -> A
g: C -> A
Plus L O (Pullback f g) <~>
Pullback (plus_functor L O f) (plus_functor L O g)
    refine (equiv_O_pullback L (O_functor O f) (O_functor O g) oE _).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
A, B, C: Type
f: B -> A
g: C -> A
Plus L O (Pullback f g) <~>
L (Pullback (O_functor O f) (O_functor O g))
    apply equiv_O_functor.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
A, B, C: Type
f: B -> A
g: C -> A
O (Pullback f g) <~>
Pullback (O_functor O f) (O_functor O g)
    rapply equiv_O_pullback.
  Defined.

  (** And diagonals. *)
  Definition diagonal_plus_functor {A B : Type} (f : A -> B)
    : diagonal (plus_functor L O f) == equiv_plus_pullback f f o plus_functor L O (diagonal f).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
A, B: Type
f: A -> B
diagonal (plus_functor L O f) ==
equiv_plus_pullback f f
o plus_functor L O (diagonal f)
  Proof.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
A, B: Type
f: A -> B
diagonal (plus_functor L O f) ==
equiv_plus_pullback f f
o plus_functor L O (diagonal f)
    intros x.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
A, B: Type
f: A -> B
x: Plus L O A
diagonal (plus_functor L O f) x =
equiv_plus_pullback f f
  (plus_functor L O (diagonal f) x)
    refine (diagonal_O_functor L (O_functor O f) x @ _).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
A, B: Type
f: A -> B
x: Plus L O A
equiv_O_pullback L (O_functor O f) (O_functor O f)
  (O_functor L (diagonal (O_functor O f)) x) =
equiv_plus_pullback f f
  (plus_functor L O (diagonal f) x)
    apply (ap (equiv_O_pullback L (O_functor O f) (O_functor O f))).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
A, B: Type
f: A -> B
x: Plus L O A
O_functor L (diagonal (O_functor O f)) x =
equiv_O_functor L (equiv_O_pullback O f f)
  (plus_functor L O (diagonal f) x)
    refine (O_functor_homotopy L _ _ (diagonal_O_functor O f) x @ _).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
A, B: Type
f: A -> B
x: Plus L O A
O_functor L
  (fun x : O A =>
   equiv_O_pullback O f f (O_functor O (diagonal f) x))
  x =
equiv_O_functor L (equiv_O_pullback O f f)
  (plus_functor L O (diagonal f) x)
    unfold plus_functor.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
A, B: Type
f: A -> B
x: Plus L O A
O_functor L
  (fun x : O A =>
   equiv_O_pullback O f f (O_functor O (diagonal f) x))
  x =
equiv_O_functor L (equiv_O_pullback O f f)
  (O_functor L (O_functor O (diagonal f)) x)
    exact (O_functor_compose L _ _ x).
  Defined.

  (** Recall that a modality is characterized by connectedness of the units.  Analogously, we can now prove that the plus-units are all plus-connected.  This is equivalently a sort of coherence axiom for the homotopy [wellpointed_plus], that when precomposed with [to_plus] it becomes [to_plus_natural]. *)
  Definition plusconnmap_to_plus (X : Type) : PlusConnMap L O (to_plus L O X).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
PlusConnMap L O (to_plus L O X)
  Proof.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
PlusConnMap L O (to_plus L O X)
    intros y; unfold PlusConnected.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
y: Plus L O X
NullHomotopy (to_plus L O (hfiber (to_plus L O X) y))
    apply (cancelL_nullhomotopy_equiv _ (plus_hfiber (to_plus L O X) y)).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
y: Plus L O X
NullHomotopy
  (fun x : hfiber (to_plus L O X) y =>
   plus_hfiber (to_plus L O X) y
     (to_plus L O (hfiber (to_plus L O X) y) x))
    apply (nullhomotopy_homotopic (fun u => (plus_hfiber_to_plus (to_plus L O X) y u)^)).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
y: Plus L O X
NullHomotopy
  (functor_hfiber
     (fun u : X =>
      (to_plus_natural L O (to_plus L O X) u)^) y)
    unfold NullHomotopy, hfiber.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
y: Plus L O X
{y0
: {x : Plus L O X &
  plus_functor L O (to_plus L O X) x =
  to_plus L O (Plus L O X) y} &
forall x : {x : X & to_plus L O X x = y},
functor_hfiber
  (fun u : X =>
   (to_plus_natural L O (to_plus L O X) u)^) y x = y0}
    unshelve refine ((y ; _) ; _).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
y: Plus L O X
plus_functor L O (to_plus L O X) y =
to_plus L O (Plus L O X) y
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
y: Plus L O X
forall x : {x : X & to_plus L O X x = y},
functor_hfiber
  (fun u : X =>
   (to_plus_natural L O (to_plus L O X) u)^) y x =
(y; ?Goal)
    {
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
y: Plus L O X
plus_functor L O (to_plus L O X) y =
to_plus L O (Plus L O X) y symmetry; apply wellpointed_plus. }
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
y: Plus L O X
forall x : {x : X & to_plus L O X x = y},
functor_hfiber
  (fun u : X =>
   (to_plus_natural L O (to_plus L O X) u)^) y x =
(y; (wellpointed_plus L O X y)^)
    intros [x p]; destruct p.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x: X
functor_hfiber
  (fun u : X =>
   (to_plus_natural L O (to_plus L O X) u)^)
  (to_plus L O X x) (x; 1) =
(to_plus L O X x;
(wellpointed_plus L O X (to_plus L O X x))^)
    unfold functor_hfiber, functor_sigma; cbn.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x: X
(to_plus L O X x;
((to_plus_natural L O (to_plus L O X) x)^)^ @ 1) =
(to_plus L O X x;
(wellpointed_plus L O X (to_plus L O X x))^)
    apply ap.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x: X
((to_plus_natural L O (to_plus L O X) x)^)^ @ 1 =
(wellpointed_plus L O X (to_plus L O X x))^
    rewrite inv_V, concat_p1.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x: X
to_plus_natural L O (to_plus L O X) x =
(wellpointed_plus L O X (to_plus L O X x))^
    unfold wellpointed_plus.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x: X
to_plus_natural L O (to_plus L O X) x =
(O_indpaths (to_plus L O (Plus L O X))
   (plus_functor L O (to_plus L O X))
   (fun ox : O X =>
    ap (to L (O (Plus L O X)))
      (O_indpaths
         (fun x : O_reflector O X =>
          to O (Plus L O X) (to L (O X) x))
         (O_functor O
            (fun x : X => to L (O X) (to O X x)))
         (fun x : X =>
          (to_O_natural O
             (fun x0 : X => to L (O X) (to O X x0)) x)^)
         ox) @
    (to_O_natural L
       (O_functor O
          (fun x : X => to L (O X) (to O X x))) ox)^)
   (to_plus L O X x))^
    rewrite !O_indpaths_beta.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x: X
to_plus_natural L O (to_plus L O X) x =
(ap (to L (O (Plus L O X)))
   (to_O_natural O
      (fun x : X => to L (O X) (to O X x)) x)^ @
 (to_O_natural L
    (O_functor O (fun x : X => to L (O X) (to O X x)))
    (to O X x))^)^
    rewrite inv_pp, ap_V, !inv_V.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
x: X
to_plus_natural L O (to_plus L O X) x =
to_O_natural L
  (O_functor O (fun x : X => to L (O X) (to O X x)))
  (to O X x) @
ap (to L (O (Plus L O X)))
  (to_O_natural O (fun x : X => to L (O X) (to O X x))
     x)
    reflexivity.
  Defined.

  (** Recall also (from [nsep_iff_trunc_to_O]) that a type is n-separated for a lex modality [O] if and only if its [O]-unit is an n-truncated map.  We can now prove the analogous fact for the plus-construction.  We state this using [MapIn (Tr n)] instead of [IsTrunc n] because we have more useful lemmas for [MapIn]. *)
  Definition nsep_iff_trunc_plus (n : trunc_index) (X : Type)
    : In (nSep n (Meet L O)) X <-> MapIn (Tr n) (to_plus L O X).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
n: trunc_index
X: Type
In (nSep n (Meet L O)) X <->
MapIn (Tr n) (to_plus L O X)
  Proof.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
n: trunc_index
X: Type
In (nSep n (Meet L O)) X <->
MapIn (Tr n) (to_plus L O X)
    revert X; induction n as [|n IHn]; intros X; split; intros H.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
H: In (nSep (-2) (Meet L O)) X
MapIn (Tr (-2)) (to_plus L O X)
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
H: MapIn (Tr (-2)) (to_plus L O X)
In (nSep (-2) (Meet L O)) X
L, O: Modality
Lex0: Lex L
Lex1: Lex O
n: trunc_index
IHn: forall X : Type,
In (nSep n (Meet L O)) X <->
MapIn (Tr n) (to_plus L O X)
X: Type
H: In (nSep n.+1 (Meet L O)) X
MapIn (Tr n.+1) (to_plus L O X)
L, O: Modality
Lex0: Lex L
Lex1: Lex O
n: trunc_index
IHn: forall X : Type,
In (nSep n (Meet L O)) X <->
MapIn (Tr n) (to_plus L O X)
X: Type
H: MapIn (Tr n.+1) (to_plus L O X)
In (nSep n.+1 (Meet L O)) X
    -
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
H: In (nSep (-2) (Meet L O)) X
MapIn (Tr (-2)) (to_plus L O X) apply contr_map_isequiv.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
H: In (nSep (-2) (Meet L O)) X
IsEquiv (to_plus L O X)
      rapply isequiv_plus_inmeet.
    -
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
H: MapIn (Tr (-2)) (to_plus L O X)
In (nSep (-2) (Meet L O)) X apply inmeet_isequiv_plus.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
X: Type
H: MapIn (Tr (-2)) (to_plus L O X)
IsEquiv (to_plus L O X)
      rapply isequiv_contr_map.
    -
L, O: Modality
Lex0: Lex L
Lex1: Lex O
n: trunc_index
IHn: forall X : Type,
In (nSep n (Meet L O)) X <->
MapIn (Tr n) (to_plus L O X)
X: Type
H: In (nSep n.+1 (Meet L O)) X
MapIn (Tr n.+1) (to_plus L O X) apply istruncmap_from_ap; intros x y.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
n: trunc_index
IHn: forall X : Type,
In (nSep n (Meet L O)) X <->
MapIn (Tr n) (to_plus L O X)
X: Type
H: In (nSep n.+1 (Meet L O)) X
x, y: X
IsTruncMap n (ap (to_plus L O X))
      apply istruncmap_mapinO_tr.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
n: trunc_index
IHn: forall X : Type,
In (nSep n (Meet L O)) X <->
MapIn (Tr n) (to_plus L O X)
X: Type
H: In (nSep n.+1 (Meet L O)) X
x, y: X
MapIn (Tr n) (ap (to_plus L O X))
      pose (i := fst (IHn _) (H x y)).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
n: trunc_index
IHn: forall X : Type,
In (nSep n (Meet L O)) X <->
MapIn (Tr n) (to_plus L O X)
X: Type
H: In (nSep n.+1 (Meet L O)) X
x, y: X
i:= fst (IHn (x = y)) (H x y): MapIn (Tr n) (to_plus L O (x = y))
MapIn (Tr n) (ap (to_plus L O X))
      apply (mapinO_homotopic _ _ (plus_path_to_plus x y)).
    -
L, O: Modality
Lex0: Lex L
Lex1: Lex O
n: trunc_index
IHn: forall X : Type,
In (nSep n (Meet L O)) X <->
MapIn (Tr n) (to_plus L O X)
X: Type
H: MapIn (Tr n.+1) (to_plus L O X)
In (nSep n.+1 (Meet L O)) X intros x y.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
n: trunc_index
IHn: forall X : Type,
In (nSep n (Meet L O)) X <->
MapIn (Tr n) (to_plus L O X)
X: Type
H: MapIn (Tr n.+1) (to_plus L O X)
x, y: X
In (nSep n (Meet L O)) (x = y)
      apply (snd (IHn (x = y))).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
n: trunc_index
IHn: forall X : Type,
In (nSep n (Meet L O)) X <->
MapIn (Tr n) (to_plus L O X)
X: Type
H: MapIn (Tr n.+1) (to_plus L O X)
x, y: X
MapIn (Tr n) (to_plus L O (x = y))
      pose (i := istruncmap_ap n (to_plus L O X) x y).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
n: trunc_index
IHn: forall X : Type,
In (nSep n (Meet L O)) X <->
MapIn (Tr n) (to_plus L O X)
X: Type
H: MapIn (Tr n.+1) (to_plus L O X)
x, y: X
i:= istruncmap_ap n (to_plus L O X) x y: IsTruncMap n (ap (to_plus L O X))
MapIn (Tr n) (to_plus L O (x = y))
      apply mapinO_tr_istruncmap in i.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
n: trunc_index
IHn: forall X : Type,
In (nSep n (Meet L O)) X <->
MapIn (Tr n) (to_plus L O X)
X: Type
H: MapIn (Tr n.+1) (to_plus L O X)
x, y: X
i: MapIn (Tr n) (ap (to_plus L O X))
MapIn (Tr n) (to_plus L O (x = y))
      apply (mapinO_homotopic _ ((plus_path x y)^-1 o (@ap _ _ (to_plus L O X) x y))).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
n: trunc_index
IHn: forall X : Type,
In (nSep n (Meet L O)) X <->
MapIn (Tr n) (to_plus L O X)
X: Type
H: MapIn (Tr n.+1) (to_plus L O X)
x, y: X
i: MapIn (Tr n) (ap (to_plus L O X))
(fun x0 : x = y =>
 (plus_path x y)^-1 (ap (to_plus L O X) x0)) ==
to_plus L O (x = y)
L, O: Modality
Lex0: Lex L
Lex1: Lex O
n: trunc_index
IHn: forall X : Type,
In (nSep n (Meet L O)) X <->
MapIn (Tr n) (to_plus L O X)
X: Type
H: MapIn (Tr n.+1) (to_plus L O X)
x, y: X
i: MapIn (Tr n) (ap (to_plus L O X))
MapIn (Tr n)
  (fun x0 : x = y =>
   (plus_path x y)^-1 (ap (to_plus L O X) x0))
      {
L, O: Modality
Lex0: Lex L
Lex1: Lex O
n: trunc_index
IHn: forall X : Type,
In (nSep n (Meet L O)) X <->
MapIn (Tr n) (to_plus L O X)
X: Type
H: MapIn (Tr n.+1) (to_plus L O X)
x, y: X
i: MapIn (Tr n) (ap (to_plus L O X))
(fun x0 : x = y =>
 (plus_path x y)^-1 (ap (to_plus L O X) x0)) ==
to_plus L O (x = y) intros p; apply moveR_equiv_V; symmetry; apply plus_path_to_plus. }
L, O: Modality
Lex0: Lex L
Lex1: Lex O
n: trunc_index
IHn: forall X : Type,
In (nSep n (Meet L O)) X <->
MapIn (Tr n) (to_plus L O X)
X: Type
H: MapIn (Tr n.+1) (to_plus L O X)
x, y: X
i: MapIn (Tr n) (ap (to_plus L O X))
MapIn (Tr n)
  (fun x0 : x = y =>
   (plus_path x y)^-1 (ap (to_plus L O X) x0))
      rapply mapinO_compose.
  Defined.

  (** We now make one more assumption, that the plus-construction inverts plus-connected embeddings.  In the case of the plus-construction for stacks, this corresponds roughly to the "local character" condition on a Grothendieck topology. *)
  Context (composing : forall (X Y : Type) (f : X -> Y)
                              (fe : IsEmbedding f) (fc : PlusConnMap L O f),
              IsEquiv (plus_functor L O f)).

  (** This implies, by induction, that the plus-construction decreases the truncation-level of any finitely truncated plus-connected map. *)
  Definition istruncmap_plus_functor {n : trunc_index} {X Y : Type} (f : X -> Y)
             `{MapIn (Tr n.+1) _ _ f} (pc : PlusConnMap L O f)
    : MapIn (Tr n) (plus_functor L O f).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X, Y: Type
f: X -> Y
H: MapIn (Tr n.+1) f
pc: PlusConnMap L O f
MapIn (Tr n) (plus_functor L O f)
  Proof.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X, Y: Type
f: X -> Y
H: MapIn (Tr n.+1) f
pc: PlusConnMap L O f
MapIn (Tr n) (plus_functor L O f)
    generalize dependent f; revert X Y; induction n as [|n IHn]; intros X Y f ? pc.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
X, Y: Type
f: X -> Y
H: MapIn (Tr (-1)) f
pc: PlusConnMap L O f
MapIn (Tr (-2)) (plus_functor L O f)
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
IHn: forall (X Y : Type) (f : X -> Y),
MapIn (Tr n.+1) f ->
PlusConnMap L O f ->
MapIn (Tr n) (plus_functor L O f)
X, Y: Type
f: X -> Y
H: MapIn (Tr n.+2) f
pc: PlusConnMap L O f
MapIn (Tr n.+1) (plus_functor L O f)
    {
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
X, Y: Type
f: X -> Y
H: MapIn (Tr (-1)) f
pc: PlusConnMap L O f
MapIn (Tr (-2)) (plus_functor L O f) apply mapinO_tr_istruncmap, contr_map_isequiv, composing; assumption. }
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
IHn: forall (X Y : Type) (f : X -> Y),
MapIn (Tr n.+1) f ->
PlusConnMap L O f ->
MapIn (Tr n) (plus_functor L O f)
X, Y: Type
f: X -> Y
H: MapIn (Tr n.+2) f
pc: PlusConnMap L O f
MapIn (Tr n.+1) (plus_functor L O f)
    pose (O_eq_Tr n).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
IHn: forall (X Y : Type) (f : X -> Y),
MapIn (Tr n.+1) f ->
PlusConnMap L O f ->
MapIn (Tr n) (plus_functor L O f)
X, Y: Type
f: X -> Y
H: MapIn (Tr n.+2) f
pc: PlusConnMap L O f
o:= O_eq_Tr n: Tr n.+1 <=> Sep (Tr n)
MapIn (Tr n.+1) (plus_functor L O f)
    apply (mapinO_O_leq (Sep (Tr n)) _), mapinO_from_diagonal.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
IHn: forall (X Y : Type) (f : X -> Y),
MapIn (Tr n.+1) f ->
PlusConnMap L O f ->
MapIn (Tr n) (plus_functor L O f)
X, Y: Type
f: X -> Y
H: MapIn (Tr n.+2) f
pc: PlusConnMap L O f
o:= O_eq_Tr n: Tr n.+1 <=> Sep (Tr n)
MapIn (Tr n) (diagonal (plus_functor L O f))
    nrapply (mapinO_homotopic (Tr n) _ (fun u => (diagonal_plus_functor f u)^)).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
IHn: forall (X Y : Type) (f : X -> Y),
MapIn (Tr n.+1) f ->
PlusConnMap L O f ->
MapIn (Tr n) (plus_functor L O f)
X, Y: Type
f: X -> Y
H: MapIn (Tr n.+2) f
pc: PlusConnMap L O f
o:= O_eq_Tr n: Tr n.+1 <=> Sep (Tr n)
MapIn (Tr n)
  (fun u : Plus L O X =>
   equiv_plus_pullback f f
     (plus_functor L O (diagonal f) u))
    apply mapinO_compose.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
IHn: forall (X Y : Type) (f : X -> Y),
MapIn (Tr n.+1) f ->
PlusConnMap L O f ->
MapIn (Tr n) (plus_functor L O f)
X, Y: Type
f: X -> Y
H: MapIn (Tr n.+2) f
pc: PlusConnMap L O f
o:= O_eq_Tr n: Tr n.+1 <=> Sep (Tr n)
MapIn (Tr n) (plus_functor L O (diagonal f))
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
IHn: forall (X Y : Type) (f : X -> Y),
MapIn (Tr n.+1) f ->
PlusConnMap L O f ->
MapIn (Tr n) (plus_functor L O f)
X, Y: Type
f: X -> Y
H: MapIn (Tr n.+2) f
pc: PlusConnMap L O f
o:= O_eq_Tr n: Tr n.+1 <=> Sep (Tr n)
MapIn (Tr n) (equiv_plus_pullback f f)
    2:rapply mapinO_isequiv.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
IHn: forall (X Y : Type) (f : X -> Y),
MapIn (Tr n.+1) f ->
PlusConnMap L O f ->
MapIn (Tr n) (plus_functor L O f)
X, Y: Type
f: X -> Y
H: MapIn (Tr n.+2) f
pc: PlusConnMap L O f
o:= O_eq_Tr n: Tr n.+1 <=> Sep (Tr n)
MapIn (Tr n) (plus_functor L O (diagonal f))
    apply IHn.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
IHn: forall (X Y : Type) (f : X -> Y),
MapIn (Tr n.+1) f ->
PlusConnMap L O f ->
MapIn (Tr n) (plus_functor L O f)
X, Y: Type
f: X -> Y
H: MapIn (Tr n.+2) f
pc: PlusConnMap L O f
o:= O_eq_Tr n: Tr n.+1 <=> Sep (Tr n)
MapIn (Tr n.+1) (diagonal f)
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
IHn: forall (X Y : Type) (f : X -> Y),
MapIn (Tr n.+1) f ->
PlusConnMap L O f ->
MapIn (Tr n) (plus_functor L O f)
X, Y: Type
f: X -> Y
H: MapIn (Tr n.+2) f
pc: PlusConnMap L O f
o:= O_eq_Tr n: Tr n.+1 <=> Sep (Tr n)
PlusConnMap L O (diagonal f)
    -
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
IHn: forall (X Y : Type) (f : X -> Y),
MapIn (Tr n.+1) f ->
PlusConnMap L O f ->
MapIn (Tr n) (plus_functor L O f)
X, Y: Type
f: X -> Y
H: MapIn (Tr n.+2) f
pc: PlusConnMap L O f
o:= O_eq_Tr n: Tr n.+1 <=> Sep (Tr n)
MapIn (Tr n.+1) (diagonal f) rapply mapinO_diagonal.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
IHn: forall (X Y : Type) (f : X -> Y),
MapIn (Tr n.+1) f ->
PlusConnMap L O f ->
MapIn (Tr n) (plus_functor L O f)
X, Y: Type
f: X -> Y
H: MapIn (Tr n.+2) f
pc: PlusConnMap L O f
o:= O_eq_Tr n: Tr n.+1 <=> Sep (Tr n)
MapIn (Sep (Tr n.+1)) f
      pose (O_eq_Tr n.+1).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
IHn: forall (X Y : Type) (f : X -> Y),
MapIn (Tr n.+1) f ->
PlusConnMap L O f ->
MapIn (Tr n) (plus_functor L O f)
X, Y: Type
f: X -> Y
H: MapIn (Tr n.+2) f
pc: PlusConnMap L O f
o:= O_eq_Tr n: Tr n.+1 <=> Sep (Tr n)
o0:= O_eq_Tr n.+1: Tr n.+2 <=> Sep (Tr n.+1)
MapIn (Sep (Tr n.+1)) f
      rapply (mapinO_O_leq _ (Sep (Tr n.+1))).
    -
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
IHn: forall (X Y : Type) (f : X -> Y),
MapIn (Tr n.+1) f ->
PlusConnMap L O f ->
MapIn (Tr n) (plus_functor L O f)
X, Y: Type
f: X -> Y
H: MapIn (Tr n.+2) f
pc: PlusConnMap L O f
o:= O_eq_Tr n: Tr n.+1 <=> Sep (Tr n)
PlusConnMap L O (diagonal f) apply plusconnmap_diagonal; assumption.
  Defined.

  (** It follows, by applying this to the plus-unit and using well-pointedness, that the plus-construction on *types* decreases their plus-separatedness. *)
  Definition nsep_plus (n : trunc_index) (X : Type) `{In (nSep n.+1 (Meet L O)) X}
    : In (nSep n (Meet L O)) (Plus L O X).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
H: In (nSep n.+1 (Meet L O)) X
In (nSep n (Meet L O)) (Plus L O X)
  Proof.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
H: In (nSep n.+1 (Meet L O)) X
In (nSep n (Meet L O)) (Plus L O X)
    apply nsep_iff_trunc_plus.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
H: In (nSep n.+1 (Meet L O)) X
MapIn (Tr n) (to_plus L O (Plus L O X))
    nrefine (mapinO_homotopic _ _ (fun u => (wellpointed_plus L O X u)^)).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
H: In (nSep n.+1 (Meet L O)) X
MapIn (Tr n) (plus_functor L O (to_plus L O X))
    apply mapinO_tr_istruncmap, istruncmap_plus_functor.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
H: In (nSep n.+1 (Meet L O)) X
MapIn (Tr n.+1) (to_plus L O X)
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
H: In (nSep n.+1 (Meet L O)) X
PlusConnMap L O (to_plus L O X)
    -
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
H: In (nSep n.+1 (Meet L O)) X
MapIn (Tr n.+1) (to_plus L O X) apply istruncmap_mapinO_tr, nsep_iff_trunc_plus; assumption.
    -
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
H: In (nSep n.+1 (Meet L O)) X
PlusConnMap L O (to_plus L O X) apply plusconnmap_to_plus.
  Defined.

  (** Therefore, if a type starts out as n-plus-separated, then n+2 applications of the plus-construction suffice to make it (-2)-plus-separated, i.e. in the meet subuniverse.  Hence it has a reflection. *)
  Global Instance prereflects_plus_nsep (n : trunc_index) (X : Type) `{In (nSep n (Meet L O)) X}
    : PreReflects (Meet L O) X.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
H: In (nSep n (Meet L O)) X
PreReflects (Meet L O) X
  Proof.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
H: In (nSep n (Meet L O)) X
PreReflects (Meet L O) X
    generalize dependent X; induction n as [|n IHn]; intros X ?.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
X: Type
H: In (nSep (-2) (Meet L O)) X
PreReflects (Meet L O) X
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
IHn: forall X : Type,
In (nSep n (Meet L O)) X ->
PreReflects (Meet L O) X
X: Type
H: In (nSep n.+1 (Meet L O)) X
PreReflects (Meet L O) X
    {
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
X: Type
H: In (nSep (-2) (Meet L O)) X
PreReflects (Meet L O) X rapply prereflects_in. }
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
IHn: forall X : Type,
In (nSep n (Meet L O)) X ->
PreReflects (Meet L O) X
X: Type
H: In (nSep n.+1 (Meet L O)) X
PreReflects (Meet L O) X
    specialize (IHn (Plus L O X) (nsep_plus n X)).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
IHn: PreReflects (Meet L O) (Plus L O X)
H: In (nSep n.+1 (Meet L O)) X
PreReflects (Meet L O) X
    unshelve econstructor.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
IHn: PreReflects (Meet L O) (Plus L O X)
H: In (nSep n.+1 (Meet L O)) X
Type
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
IHn: PreReflects (Meet L O) (Plus L O X)
H: In (nSep n.+1 (Meet L O)) X
In (Meet L O) ?O_reflector
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
IHn: PreReflects (Meet L O) (Plus L O X)
H: In (nSep n.+1 (Meet L O)) X
X -> ?O_reflector
    -
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
IHn: PreReflects (Meet L O) (Plus L O X)
H: In (nSep n.+1 (Meet L O)) X
Type exact (O_reflector (Meet L O) (Plus L O X)).
    -
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
IHn: PreReflects (Meet L O) (Plus L O X)
H: In (nSep n.+1 (Meet L O)) X
In (Meet L O) (O_reflector (Meet L O) (Plus L O X)) exact _.
    -
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
IHn: PreReflects (Meet L O) (Plus L O X)
H: In (nSep n.+1 (Meet L O)) X
X -> O_reflector (Meet L O) (Plus L O X) exact (to (Meet L O) (Plus L O X) o to_plus L O X).
  Defined.

  Global Instance reflects_plus_nsep (n : trunc_index) (X : Type) `{In (nSep n (Meet L O)) X}
    : Reflects (Meet L O) X.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
H: In (nSep n (Meet L O)) X
Reflects (Meet L O) X
  Proof.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
H: In (nSep n (Meet L O)) X
Reflects (Meet L O) X
    generalize dependent X; induction n as [|n IHn]; intros X ?.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
X: Type
H: In (nSep (-2) (Meet L O)) X
Reflects (Meet L O) X
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
IHn: forall (X : Type)
(H : In (nSep n (Meet L O)) X),
Reflects (Meet L O) X
X: Type
H: In (nSep n.+1 (Meet L O)) X
Reflects (Meet L O) X
    {
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
X: Type
H: In (nSep (-2) (Meet L O)) X
Reflects (Meet L O) X rapply reflects_in. }
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
IHn: forall (X : Type)
(H : In (nSep n (Meet L O)) X),
Reflects (Meet L O) X
X: Type
H: In (nSep n.+1 (Meet L O)) X
Reflects (Meet L O) X
    specialize (IHn (Plus L O X) (nsep_plus n X)).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
H: In (nSep n.+1 (Meet L O)) X
IHn: Reflects (Meet L O) (Plus L O X)
Reflects (Meet L O) X
    constructor; intros.
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
H: In (nSep n.+1 (Meet L O)) X
IHn: Reflects (Meet L O) (Plus L O X)
Q: Type
Q_inO: In (Meet L O) Q
ooExtendableAlong (to (Meet L O) X)
  (fun _ : O_reflector (Meet L O) X => Q)
    apply (ooextendable_compose _ (to_plus L O X) (to (Meet L O) (Plus L O X))).
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
H: In (nSep n.+1 (Meet L O)) X
IHn: Reflects (Meet L O) (Plus L O X)
Q: Type
Q_inO: In (Meet L O) Q
ooExtendableAlong (to (Meet L O) (Plus L O X))
  (fun _ : O_reflector (Meet L O) X => Q)
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
H: In (nSep n.+1 (Meet L O)) X
IHn: Reflects (Meet L O) (Plus L O X)
Q: Type
Q_inO: In (Meet L O) Q
ooExtendableAlong (to_plus L O X)
  (fun _ : Plus L O X => Q)
    -
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
H: In (nSep n.+1 (Meet L O)) X
IHn: Reflects (Meet L O) (Plus L O X)
Q: Type
Q_inO: In (Meet L O) Q
ooExtendableAlong (to (Meet L O) (Plus L O X))
  (fun _ : O_reflector (Meet L O) X => Q) apply (@extendable_to_O (Meet L O) (Plus L O X)); assumption.
    -
L, O: Modality
Lex0: Lex L
Lex1: Lex O
composing: forall (X Y : Type) (f : X -> Y),
IsEmbedding f ->
PlusConnMap L O f ->
IsEquiv (plus_functor L O f)
n: trunc_index
X: Type
H: In (nSep n.+1 (Meet L O)) X
IHn: Reflects (Meet L O) (Plus L O X)
Q: Type
Q_inO: In (Meet L O) Q
ooExtendableAlong (to_plus L O X)
  (fun _ : Plus L O X => Q) rapply ooextendable_plus.
  Defined.

End LexMeet.