(* -*- 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 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. *)

Global 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
    snrapply lex_from_inO_typeO; [ exact _ | intros i ].
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
(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)) a = 
B a
      apply path_TypeO, path_universe_uncurried.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
((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)) a).1 <~> 
(B a).1
      unfold composeD; simpl.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
(forall a : acc_ngen O i, B a) <~> (B a).1
      simple refine (equiv_adjointify _ _ _ _).
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
(forall a : acc_ngen O i, B a) -> (B a).1
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
(B a).1 -> forall a : acc_ngen O i, B a
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
(forall a : acc_ngen O i, B a) -> (B a).1 intros f.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
f: forall a : acc_ngen O i, B a
(B a).1 exact (f a).
      +
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
(B a).1 -> forall a : acc_ngen O i, B a intros b a'.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
(fun f : forall a : acc_ngen O i, B a => 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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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
        refine (transport2 B (path_contr _ 1) b).
      +
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 a : acc_ngen O i, B a => f a) ==
idmap intros f.
H: Univalence
O: Modality
H0: IsAccModality O
Topological0: forall i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
f: forall a : acc_ngen O i, B a
(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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
i: lgen_indices (acc_lgen O)
B: acc_ngen O i -> Type_ (modality_subuniv O)
a: acc_ngen O i
f: forall a : acc_ngen O i, B a
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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 i : ngen_indices (acc_ngen O),
IsHProp (acc_ngen O i)
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.


Global 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 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)}
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 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)}
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 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)}
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 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)}
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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 in b1 = b2
    end
    :
    Type
|}: NullGenerators
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) *
(Nul D <=> Nul B)}
    assert (Dtrunc : forall c:C, IsTrunc n.+1 (D c)).
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
{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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) *
(Nul D <=> Nul B)}
    assert (OeqD : O <=> (Nul D)).
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
OeqD: O <=> Nul D
{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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 a : A, IsConnected O (B a)
IsConnected O
  (lgen_domain (null_to_local_generators D) (inl a))
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 in b1 = b2
    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 a : A, IsConnected O (B a)
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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 a : A, IsConnected O (B a)
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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 a : A, IsConnected O (B a)
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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 a : A, IsConnected O (B a)
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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 a : A, IsConnected O (B a)
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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 a : A, IsConnected O (B a)
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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 in b1 = b2
    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 a : A, IsConnected O (B a)
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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 in b1 = b2
    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 a : A, IsConnected O (B a)
IsConnected O (b1 = b2) rapply isconnected_paths.
      -
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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)) rapply isconnected_acc_ngen. }
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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)
          rapply (isconnected_acc_ngen (Nul D) (inr (a;(b,x)))). }
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 x : X => forall u : B a, x = 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 x : X => forall u : B a, x = 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 in b1 = b2
    end
    :
    Type
|}: NullGenerators
Dtrunc: forall c : C, IsTrunc n.+1 (D c)
OeqD: O <=> Nul D
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) *
(Nul D <=> Nul B)}
    destruct (IHn D OeqD _) as [E [HE EeqD]].
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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
{D : NullGenerators &
(forall c : ngen_indices D, IsHProp (D c)) *
(Nul D <=> Nul B)}
    exists E; split; [ exact HE | ].
H: Funext
O: Modality
Olex: Lex O
n: trunc_index
IHn: 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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 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)}
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 proj3 := proj2 in
        let b1 := fst proj3 in
        let b2 := snd proj3 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.