Require Import HoTT.Basics HoTT.Types.Require Import HoTT.Basics HoTT.Types.
Require Import Extensions HoTT.Truncations.
Require Import Accessible Lex Nullification.

Local Open Scope path_scope.


(** * Topological localizations *)

(** A topological localization -- or, as we will say, a topological nullification -- is a nullification at a family of hprops, or more generally an accessible modality whose generators of accessibility are all hprops.  This is not quite the same as Lurie's definition: in Higher Topos Theory, a topological localization is an accessible *left exact* localization at a pullback-stable class generated by a set of monomorphisms.  "Pullback-stable class generated by" is roughly incorporated into our internal notion of accessibility, so the main new difference here is that when the generation is internal in this way, the localization at a family of hprops is *automatically* left exact. *)

Notation Topological O := (forall i, IsHProp (acc_ngen O i)).

(** ** Topological modalities are lex *)

(** We prove left-exactness by proving that the universe of modal types is modal, using univalence.  It's unclear whether univalence is necessary or not in general; in one special case (open modalities) funext suffices.  But it's plausible that it would be necessary in general, because lex-ness of nullification is a statement about the path-spaces of a HIT, and characterizing those in any way usually requires some amount of univalence. *)

Instance lex_topological `{Univalence}
       (O : Modality) `{IsAccModality O} `{Topological O}
  : Lex O.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i)
Lex O
Proof.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i)
Lex O
    snapply lex_from_inO_typeO; [ exact _ | intros i ].
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
ooExtendableAlong (acc_lgen O i)
  (fun _ : lgen_codomain (acc_lgen O) i => Type_ O)
    apply ((equiv_ooextendable_isequiv _ _)^-1%equiv).
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
IsEquiv
  (fun g : lgen_codomain (acc_lgen O) i -> Type_ O => g oD acc_lgen O i)
    srapply isequiv_adjointify; cbn.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
(acc_ngen O i -> Type_ (modality_subuniv O)) ->
Unit -> Type_ (modality_subuniv O)
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
(fun x : acc_ngen O i -> Type_ (modality_subuniv O) =>
 ?Goal x oD (fun _ : acc_ngen O i => tt)) ==
idmap
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
(fun x : Unit -> Type_ (modality_subuniv O) =>
 ?Goal (x oD (fun _ : acc_ngen O i => tt))) ==
idmap
    -
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
(acc_ngen O i -> Type_ (modality_subuniv O)) ->
Unit -> Type_ (modality_subuniv O) intros B _.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
Type_ (modality_subuniv O)
      refine ((forall a, B a) ; _).
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
In (modality_subuniv O) (forall a : acc_ngen O i, B a)
      exact _.
    -
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
(fun x : acc_ngen O i -> Type_ (modality_subuniv O) =>
 (fun B : acc_ngen O i -> Type_ (modality_subuniv O) =>
  unit_name
    (forall a : acc_ngen O i, B a;
    inO_forall O (acc_ngen O i) (fun x0 : acc_ngen O i => B x0)
      (fun x0 : acc_ngen O i => inO_TypeO (B x0))))
   x
 oD (fun _ : acc_ngen O i => tt)) ==
idmap intros B.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
unit_name
  (forall a : acc_ngen O i, B a;
  inO_forall O (acc_ngen O i) (fun x : acc_ngen O i => B x)
    (fun x : acc_ngen O i => inO_TypeO (B x)))
oD (fun _ : acc_ngen O i => tt) = B
      apply path_arrow; intros a.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
(unit_name
   (forall a0 : acc_ngen O i, B a0;
   inO_forall O (acc_ngen O i) (fun x : acc_ngen O i => B x)
     (fun x : acc_ngen O i => inO_TypeO (B x)))
 oD (fun _ : acc_ngen O i => tt)) a =
B a
      apply path_TypeO, path_universe_uncurried.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
((unit_name
    (forall a0 : acc_ngen O i, B a0;
    inO_forall O (acc_ngen O i) (fun x : acc_ngen O i => B x)
      (fun x : acc_ngen O i => inO_TypeO (B x)))
  oD (fun _ : acc_ngen O i => tt)) a).1 <~>
(B a).1
      unfold composeD; simpl.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
(forall a0 : acc_ngen O i, B a0) <~> (B a).1
      simple refine (equiv_adjointify _ _ _ _).
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
(forall a0 : acc_ngen O i, B a0) -> (B a).1
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
(B a).1 -> forall a0 : acc_ngen O i, B a0
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
?f o ?g == idmap
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
?g o ?f == idmap
      +
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
(forall a0 : acc_ngen O i, B a0) -> (B a).1 intros f.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
f: forall a0 : acc_ngen O i, B a0
(B a).1 exact (f a).
      +
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
(B a).1 -> forall a0 : acc_ngen O i, B a0 intros b a'.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
b: (B a).1
a': acc_ngen O i
B a' exact (transport B (path_ishprop a a') b).
      +
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
(fun f : forall a0 : acc_ngen O i, B a0 => f a)
o (fun (b : (B a).1) (a' : acc_ngen O i) =>
   transport (fun x : acc_ngen O i => B x) (path_ishprop a a') b) ==
idmap intros b.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
b: (B a).1
transport (fun x : acc_ngen O i => B x) (path_ishprop a a) b = b
        exact (transport2 B (path_contr _ 1) b).
      +
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
(fun (b : (B a).1) (a' : acc_ngen O i) =>
 transport (fun x : acc_ngen O i => B x) (path_ishprop a a') b)
o (fun f : forall a0 : acc_ngen O i, B a0 => f a) == idmap intros f.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
f: forall a0 : acc_ngen O i, B a0
(fun a' : acc_ngen O i =>
 transport (fun x : acc_ngen O i => B x) (path_ishprop a a') (f a)) =
f apply path_forall; intros a'.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
f: forall a0 : acc_ngen O i, B a0
a': acc_ngen O i
transport (fun x : acc_ngen O i => B x) (path_ishprop a a') (f a) = f a'
        exact (apD f _).
    -
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
(fun x : Unit -> Type_ (modality_subuniv O) =>
 (fun B : acc_ngen O i -> Type_ (modality_subuniv O) =>
  unit_name
    (forall a : acc_ngen O i, B a;
    inO_forall O (acc_ngen O i) (fun x0 : acc_ngen O i => B x0)
      (fun x0 : acc_ngen O i => inO_TypeO (B x0))))
   (x oD (fun _ : acc_ngen O i => tt))) ==
idmap intros B.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: Unit -> Type_ (modality_subuniv O)
unit_name
  (forall a : acc_ngen O i, (B oD (fun _ : acc_ngen O i => tt)) a;
  inO_forall O (acc_ngen O i)
    (fun x : acc_ngen O i => (B oD (fun _ : acc_ngen O i => tt)) x)
    (fun x : acc_ngen O i =>
     inO_TypeO ((B oD (fun _ : acc_ngen O i => tt)) x))) =
B
      apply path_arrow; intros [].
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: Unit -> Type_ (modality_subuniv O)
(forall a : acc_ngen O i, (B oD (fun _ : acc_ngen O i => tt)) a;
inO_forall O (acc_ngen O i)
  (fun x : acc_ngen O i => (B oD (fun _ : acc_ngen O i => tt)) x)
  (fun x : acc_ngen O i => inO_TypeO ((B oD (fun _ : acc_ngen O i => tt)) x))) =
B tt
      apply path_TypeO, path_universe_uncurried.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: Unit -> Type_ (modality_subuniv O)
(forall a : acc_ngen O i, (B oD (fun _ : acc_ngen O i => tt)) a;
inO_forall O (acc_ngen O i)
  (fun x : acc_ngen O i => (B oD (fun _ : acc_ngen O i => tt)) x)
  (fun x : acc_ngen O i => inO_TypeO ((B oD (fun _ : acc_ngen O i => tt)) x))).1 <~>
(B tt).1
      unfold composeD; simpl.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: Unit -> Type_ (modality_subuniv O)
(acc_ngen O i -> B tt) <~> (B tt).1
      pose (e := isequiv_ooextendable _ _
                                      (fst (inO_iff_isnull O (B tt)) (inO_TypeO (B tt)) i)).
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: Unit -> Type_ (modality_subuniv O)
e:= isequiv_ooextendable
  (fun _ : lgen_codomain (null_to_local_generators (acc_ngen O)) i => B tt)
  (null_to_local_generators (acc_ngen O) i)
  (fst (inO_iff_isnull O (B tt)) (inO_TypeO (B tt)) i): IsEquiv
  (fun
     g : forall b : lgen_codomain (null_to_local_generators (acc_ngen O)) i,
         (fun _ : lgen_codomain (null_to_local_generators (acc_ngen O)) i =>
          TypeO_pr1 (modality_subuniv O) (B tt)) b =>
   g oD null_to_local_generators (acc_ngen O) i)
(acc_ngen O i -> B tt) <~> (B tt).1
      unfold composeD in e; simpl in e.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: Unit -> Type_ (modality_subuniv O)
e:= isequiv_ooextendable (unit_name (B tt)) (fun _ : acc_ngen O i => tt)
  (fst (inO_iff_isnull O (B tt)) (inO_TypeO (B tt)) i): IsEquiv (fun (g : Unit -> B tt) (_ : acc_ngen O i) => g tt)
(acc_ngen O i -> B tt) <~> (B tt).1
      refine (_ oE (Build_Equiv _ _ _ e)^-1).
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i0 : ngen_indices (acc_ngen O), IsHProp (acc_ngen O i0)
i: lgen_indices (acc_lgen O)
B: Unit -> Type_ (modality_subuniv O)
e:= isequiv_ooextendable (unit_name (B tt)) (fun _ : acc_ngen O i => tt)
  (fst (inO_iff_isnull O (B tt)) (inO_TypeO (B tt)) i): IsEquiv (fun (g : Unit -> B tt) (_ : acc_ngen O i) => g tt)
(Unit -> B tt) <~> (B tt).1
      exact (equiv_contr_forall _).
Defined.


Instance lex_nullification `{Univalence}
      (S : NullGenerators) `{forall i, IsHProp (S i)}
: Lex (Nul S).
H: Univalence
S: NullGenerators
H0: forall i : ngen_indices S, IsHProp (S i)
Lex (Nul S)
Proof.
H: Univalence
S: NullGenerators
H0: forall i : ngen_indices S, IsHProp (S i)
Lex (Nul S)
  rapply lex_topological.
Defined.


(** ** Lex modalities generated by n-types are topological *)

(** For [n >= 0], nullification at a family of [n]-types need not be lex.  For instance, the (-1)-truncation is nullification at [Bool].  However, if the nullification at a family of [n]-types *is* lex, then it is topological. *)

(** This is kind of annoying to prove, not just because the proof is fiddly, but because we have to pass back and forth between different generating families for the "same" modality.  It's a bit easier to prove it about nullifications than about arbitrary accessible lex modalities. *)

Definition topological_lex_trunc_acc `{Funext}
             (B : NullGenerators) {Olex : Lex (Nul B)}
             (n : trunc_index) (gtr : forall a, IsTrunc n (ngen_type B a))
    : { D : NullGenerators &
            (forall c, IsHProp (ngen_type D c)) *
            (Nul D <=> Nul B) }.
H: Funext
B: NullGenerators
Olex: Lex (Nul B)
n: trunc_index
gtr: forall a : ngen_indices B, IsTrunc n (B a)
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B)}
Proof.
H: Funext
B: NullGenerators
Olex: Lex (Nul B)
n: trunc_index
gtr: forall a : ngen_indices B, IsTrunc n (B a)
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B)}
    destruct n.
H: Funext
B: NullGenerators
Olex: Lex (Nul B)
gtr: forall a : ngen_indices B, Contr (B a)
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B)}
H: Funext
B: NullGenerators
Olex: Lex (Nul B)
n: trunc_index
gtr: forall a : ngen_indices B, IsTrunc n.+1 (B a)
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B)}
    {
H: Funext
B: NullGenerators
Olex: Lex (Nul B)
gtr: forall a : ngen_indices B, Contr (B a)
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B)} exists (Build_NullGenerators Empty (fun _ => Unit)).
H: Funext
B: NullGenerators
Olex: Lex (Nul B)
gtr: forall a : ngen_indices B, Contr (B a)
(forall
 c : ngen_indices
       {| ngen_indices := Empty; ngen_type := fun _ : Empty => Unit |},
 IsHProp ({| ngen_indices := Empty; ngen_type := fun _ : Empty => Unit |} c)) *
(Nul {| ngen_indices := Empty; ngen_type := fun _ : Empty => Unit |} <=>
 Nul B)
      split; [ exact _ | split; intros X _; [ | intros [] ] ].
H: Funext
B: NullGenerators
Olex: Lex (Nul B)
gtr: forall a : ngen_indices B, Contr (B a)
X: Type
In (Nul B) X
      intros i.
H: Funext
B: NullGenerators
Olex: Lex (Nul B)
gtr: forall a : ngen_indices B, Contr (B a)
X: Type
i: lgen_indices (null_to_local_generators B)
ooExtendableAlong (null_to_local_generators B i)
  (fun _ : lgen_codomain (null_to_local_generators B) i => X)
      apply ooextendable_equiv, isequiv_contr_contr. }
H: Funext
B: NullGenerators
Olex: Lex (Nul B)
n: trunc_index
gtr: forall a : ngen_indices B, IsTrunc n.+1 (B a)
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B)}
    pose (O := Nul B).
H: Funext
B: NullGenerators
Olex: Lex (Nul B)
n: trunc_index
gtr: forall a : ngen_indices B, IsTrunc n.+1 (B a)
O:= Nul B: Modality
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B)}
    pose (OeqB := reflexive_O_eq O : O <=> (Nul B)).
H: Funext
B: NullGenerators
Olex: Lex (Nul B)
n: trunc_index
gtr: forall a : ngen_indices B, IsTrunc n.+1 (B a)
O:= Nul B: Modality
OeqB:= reflexive_O_eq O : O <=> Nul B: O <=> Nul B
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B)}
    change (Nul B) with O in Olex.
H: Funext
B: NullGenerators
O:= Nul B: Modality
Olex: Lex O
n: trunc_index
gtr: forall a : ngen_indices B, IsTrunc n.+1 (B a)
OeqB:= reflexive_O_eq O : O <=> Nul B: O <=> Nul B
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B)}
    clearbody O OeqB.
H: Funext
B: NullGenerators
O: Modality
Olex: Lex O
n: trunc_index
gtr: forall a : ngen_indices B, IsTrunc n.+1 (B a)
OeqB: O <=> Nul B
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B)}
    revert B OeqB gtr.
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
forall B : NullGenerators,
O <=> Nul B ->
(forall a : ngen_indices B, IsTrunc n.+1 (B a)) ->
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B)}
    induction n; intros B OeqB gtr.
H: Funext
O: Modality
Olex: Lex O
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsHProp (B a)
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B)}
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B)}
    {
H: Funext
O: Modality
Olex: Lex O
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsHProp (B a)
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B)} exists B; split; [ assumption | reflexivity ]. }
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B)}
    pose (A := ngen_indices B).
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B)}
    pose (C := A + { a:A & B(a) * B(a) }).
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) * (Nul D <=> Nul B)}
    pose (D := Build_NullGenerators
                 C (fun c:C => match c with
                               | inl a => merely (B a)
                               | inr (a ; (b1, b2)) => (b1 = b2)
                               end : Type)).
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B)}
    assert (Dtrunc : forall c:C, IsTrunc n.+1 (D c)).
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
forall c : C, IsTrunc n.+1 (D c)
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B)}
    {
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
forall c : C, IsTrunc n.+1 (D c) intros [a | [a [b1 b2]]]; [ cbn | exact _ ].
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
a: A
IsTrunc n.+1 (Trunc (-1) (B a))
      (* Because [trunc_hprop] can't be used as an idmap... *)
      destruct n; exact _. }
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B)}
    assert (OeqD : O <=> (Nul D)).
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
O <=> Nul D
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
OeqD: O <=> Nul D
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B)}
    {
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
O <=> Nul D split; intros X.
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
In O X -> In (Nul D) X
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
In (Nul D) X -> In O X
      -
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
In O X -> In (Nul D) X intros X_inO c.
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c0 : ngen_indices D0, IsHProp (D0 c0)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c0 : C =>
    match c0 with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c0 : C, IsTrunc n.+1 (D c0)
X: Type
X_inO: In O X
c: lgen_indices (null_to_local_generators D)
ooExtendableAlong (null_to_local_generators D c)
  (fun _ : lgen_codomain (null_to_local_generators D) c => X)
        assert (Bc : forall a:A, IsConnected O (B a)).
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c0 : ngen_indices D0, IsHProp (D0 c0)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c0 : C =>
    match c0 with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c0 : C, IsTrunc n.+1 (D c0)
X: Type
X_inO: In O X
c: lgen_indices (null_to_local_generators D)
forall a : A, IsConnected O (B a)
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c0 : ngen_indices D0, IsHProp (D0 c0)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c0 : C =>
    match c0 with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c0 : C, IsTrunc n.+1 (D c0)
X: Type
X_inO: In O X
c: lgen_indices (null_to_local_generators D)
Bc: forall a : A, IsConnected O (B a)
ooExtendableAlong (null_to_local_generators D c)
  (fun _ : lgen_codomain (null_to_local_generators D) c => X)
        {
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c0 : ngen_indices D0, IsHProp (D0 c0)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c0 : C =>
    match c0 with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c0 : C, IsTrunc n.+1 (D c0)
X: Type
X_inO: In O X
c: lgen_indices (null_to_local_generators D)
forall a : A, IsConnected O (B a) intros a.
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c0 : ngen_indices D0, IsHProp (D0 c0)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c0 : C =>
    match c0 with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c0 : C, IsTrunc n.+1 (D c0)
X: Type
X_inO: In O X
c: lgen_indices (null_to_local_generators D)
a: A
IsConnected O (B a)
          rapply (@isconnected_O_leq O (Nul B)).
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c0 : ngen_indices D0, IsHProp (D0 c0)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c0 : C =>
    match c0 with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c0 : C, IsTrunc n.+1 (D c0)
X: Type
X_inO: In O X
c: lgen_indices (null_to_local_generators D)
a: A
IsConnected (Nul B) (B a)
          exact (isconnected_acc_ngen (Nul B) a). }
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c0 : ngen_indices D0, IsHProp (D0 c0)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c0 : C =>
    match c0 with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c0 : C, IsTrunc n.+1 (D c0)
X: Type
X_inO: In O X
c: lgen_indices (null_to_local_generators D)
Bc: forall a : A, IsConnected O (B a)
ooExtendableAlong (null_to_local_generators D c)
  (fun _ : lgen_codomain (null_to_local_generators D) c => X)
        apply (ooextendable_const_isconnected_inO O);
          [ destruct c as [a | [a [b1 b2]]] | exact X_inO ].
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
X_inO: In O X
a: A
Bc: forall a0 : A, IsConnected O (B a0)
IsConnected O (lgen_domain (null_to_local_generators D) (inl a))
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b0 := fst proj0 in let b3 := snd proj0 in b0 = b3
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
X_inO: In O X
a: A
b1, b2: B a
Bc: forall a0 : A, IsConnected O (B a0)
IsConnected O (lgen_domain (null_to_local_generators D) (inr (a; (b1, b2))))
        +
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
X_inO: In O X
a: A
Bc: forall a0 : A, IsConnected O (B a0)
IsConnected O (lgen_domain (null_to_local_generators D) (inl a)) apply isconnected_from_elim_to_O.
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
X_inO: In O X
a: A
Bc: forall a0 : A, IsConnected O (B a0)
NullHomotopy.NullHomotopy
  (to O (lgen_domain (null_to_local_generators D) (inl a)))
          destruct (isconnected_elim O (O (merely (B a)))
                                     (fun b => to O _ (tr b)))
            as [x h].
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
X_inO: In O X
a: A
Bc: forall a0 : A, IsConnected O (B a0)
x: O (merely (B a))
h: forall x0 : B a, to O (merely (B a)) (tr x0) = x
NullHomotopy.NullHomotopy
  (to O (lgen_domain (null_to_local_generators D) (inl a)))
          exists x; intros y; cbn in y.
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
X_inO: In O X
a: A
Bc: forall a0 : A, IsConnected O (B a0)
x: O (merely (B a))
h: forall x0 : B a, to O (merely (B a)) (tr x0) = x
y: Trunc (-1) (B a)
to O (lgen_domain (null_to_local_generators D) (inl a)) y = x
          strip_truncations.
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
X_inO: In O X
a: A
Bc: forall a0 : A, IsConnected O (B a0)
x: O (merely (B a))
h: forall x0 : B a, to O (merely (B a)) (tr x0) = x
y: B a
to O (lgen_domain (null_to_local_generators D) (inl a)) (tr y) = x
          exact (h y).
        +
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b0 := fst proj0 in let b3 := snd proj0 in b0 = b3
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
X_inO: In O X
a: A
b1, b2: B a
Bc: forall a0 : A, IsConnected O (B a0)
IsConnected O (lgen_domain (null_to_local_generators D) (inr (a; (b1, b2)))) cbn.
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b0 := fst proj0 in let b3 := snd proj0 in b0 = b3
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
X_inO: In O X
a: A
b1, b2: B a
Bc: forall a0 : A, IsConnected O (B a0)
IsConnected O (b1 = b2) rapply isconnected_paths.
      -
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
In (Nul D) X -> In O X intros Dnull; rapply (@inO_leq (Nul B) O).
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
In (Nul B) X
        intros a; cbn in a; cbn.
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
ooExtendableAlong (fun _ : B a => tt) (unit_name X)
        apply ((equiv_ooextendable_isequiv
                  (unit_name X) (fun _:B a => tt))^-1).
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
IsEquiv (fun g : Unit -> X => g oD (fun _ : B a => tt))
        apply isequiv_contr_map; intros f; cbn in f.
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
Contr (hfiber (fun g : Unit -> X => g oD (fun _ : B a => tt)) f)
        refine (contr_equiv' { x:X & forall u:B a, x = f u } _).
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
{x : X & forall u : B a, x = f u} <~>
hfiber (fun g : Unit -> X => g oD (fun _ : B a => tt)) f
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
Contr {x : X & forall u : B a, x = f u}
        {
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
{x : X & forall u : B a, x = f u} <~>
hfiber (fun g : Unit -> X => g oD (fun _ : B a => tt)) f refine (equiv_functor_sigma' (equiv_unit_rec X) _).
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
forall a0 : X,
(forall u : B a, a0 = f u) <~> equiv_unit_rec X a0 oD (fun _ : B a => tt) = f
          intros x; unfold composeD; cbn.
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
x: X
(forall u : B a, x = f u) <~> (fun _ : B a => x) = f
          apply equiv_path_arrow. }
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
Contr {x : X & forall u : B a, x = f u}
        refine ((isconnected_elim (Nul D) (A := D (inl a)) _ _).1).
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
IsConnected (Nul D) (D (inl a))
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
D (inl a) -> Contr {x : X & forall u : B a, x = f u}
        {
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
IsConnected (Nul D) (D (inl a)) tapply isconnected_acc_ngen. }
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
D (inl a) -> Contr {x : X & forall u : B a, x = f u}
        intros b; cbn in b.
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
b: Trunc (-1) (B a)
Contr {x : X & forall u : B a, x = f u} strip_truncations.
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
b: B a
Contr {x : X & forall u : B a, x = f u}
        assert (bc : IsConnMap (Nul D) (unit_name b)).
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
b: B a
IsConnMap (Nul D) (unit_name b)
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
b: B a
bc: IsConnMap (Nul D) (unit_name b)
Contr {x : X & forall u : B a, x = f u}
        {
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
b: B a
IsConnMap (Nul D) (unit_name b) intros x; unfold hfiber.
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
b, x: B a
IsConnected (Nul D) {_ : Unit & b = x}
          apply (isconnected_equiv (Nul D) (b = x)
                                   (equiv_contr_sigma _)^-1).
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
b, x: B a
IsConnected (Nul D) (b = x)
          exact (isconnected_acc_ngen (Nul D) (inr (a;(b,x)))). }
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
b: B a
bc: IsConnMap (Nul D) (unit_name b)
Contr {x : X & forall u : B a, x = f u}
        pose (p := conn_map_elim (Nul D) (unit_name b)
                                 (fun u => f b = f u) (fun _ => 1)).
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
b: B a
bc: IsConnMap (Nul D) (unit_name b)
p:= conn_map_elim (Nul D) (unit_name b) (fun u : B a => f b = f u) (unit_name 1): forall b0 : B a, (fun u : B a => f b = f u) b0
Contr {x : X & forall u : B a, x = f u}
        apply (Build_Contr _ (f b ; p)); intros [x q].
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
b: B a
bc: IsConnMap (Nul D) (unit_name b)
p:= conn_map_elim (Nul D) (unit_name b) (fun u : B a => f b = f u) (unit_name 1): forall b0 : B a, (fun u : B a => f b = f u) b0
x: X
q: forall u : B a, x = f u
(f b; p) = (x; q)
        refine (path_sigma' _ (q b)^ _); apply path_forall.
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
b: B a
bc: IsConnMap (Nul D) (unit_name b)
p:= conn_map_elim (Nul D) (unit_name b) (fun u : B a => f b = f u) (unit_name 1): forall b0 : B a, (fun u : B a => f b = f u) b0
x: X
q: forall u : B a, x = f u
transport (fun x0 : X => forall u : B a, x0 = f u) (q b)^ p == q
        refine (conn_map_elim (Nul D) (unit_name b) _ _); intros [].
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
b: B a
bc: IsConnMap (Nul D) (unit_name b)
p:= conn_map_elim (Nul D) (unit_name b) (fun u : B a => f b = f u) (unit_name 1): forall b0 : B a, (fun u : B a => f b = f u) b0
x: X
q: forall u : B a, x = f u
transport (fun x0 : X => forall u : B a, x0 = f u) (q b)^ p b = q b
        rewrite transport_forall_constant, transport_paths_l, inv_V.
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
b: B a
bc: IsConnMap (Nul D) (unit_name b)
p:= conn_map_elim (Nul D) (unit_name b) (fun u : B a => f b = f u) (unit_name 1): forall b0 : B a, (fun u : B a => f b = f u) b0
x: X
q: forall u : B a, x = f u
q b @ p b = q b
        rewrite (conn_map_comp (Nul D) (unit_name b)
                               (fun u:B a => f b = f u)
                               (fun _ => 1) tt : p b = 1).
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a0 : ngen_indices B0, IsTrunc n.+1 (B0 a0)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a0 : ngen_indices B, IsTrunc n.+2 (B a0)
A:= ngen_indices B: Type
C:= A + {a0 : A & B a0 * B a0}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a0 => merely (B a0)
    | inr s =>
        let s0 := s in
        let a0 := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
X: Type
Dnull: In (Nul D) X
a: ngen_indices B
f: B a -> X
b: B a
bc: IsConnMap (Nul D) (unit_name b)
p:= conn_map_elim (Nul D) (unit_name b) (fun u : B a => f b = f u) (unit_name 1): forall b0 : B a, (fun u : B a => f b = f u) b0
x: X
q: forall u : B a, x = f u
q b @ 1 = q b
        apply concat_p1. }
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
OeqD: O <=> Nul D
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B)}
    destruct (IHn D OeqD _) as [E [HE EeqD]].
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
OeqD: O <=> Nul D
E: NullGenerators
HE: forall c : ngen_indices E, IsHProp (E c)
EeqD: Nul E <=> Nul D
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B)}
    exists E; split; [ exact HE | ].
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
OeqD: O <=> Nul D
E: NullGenerators
HE: forall c : ngen_indices E, IsHProp (E c)
EeqD: Nul E <=> Nul D
Nul E <=> Nul B
    refine (transitivity EeqD _).
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
OeqD: O <=> Nul D
E: NullGenerators
HE: forall c : ngen_indices E, IsHProp (E c)
EeqD: Nul E <=> Nul D
Nul D <=> Nul B
    refine (transitivity _ OeqB).
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: forall B0 : NullGenerators,
O <=> Nul B0 ->
(forall a : ngen_indices B0, IsTrunc n.+1 (B0 a)) ->
{D0 : NullGenerators &
(forall c : ngen_indices D0, IsHProp (D0 c)) * (Nul D0 <=> Nul B0)}
B: NullGenerators
OeqB: O <=> Nul B
gtr: forall a : ngen_indices B, IsTrunc n.+2 (B a)
A:= ngen_indices B: Type
C:= A + {a : A & B a * B a}: Type
D:= {|
  ngen_indices := C;
  ngen_type :=
    fun c : C =>
    match c with
    | inl a => merely (B a)
    | inr s =>
        let s0 := s in
        let a := s0.1 in
        let proj2 := s0.2 in
        let proj0 := proj2 in
        let b1 := fst proj0 in let b2 := snd proj0 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
OeqD: O <=> Nul D
E: NullGenerators
HE: forall c : ngen_indices E, IsHProp (E c)
EeqD: Nul E <=> Nul D
Nul D <=> O
    symmetry; assumption.
Defined.