`{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) }. Proof. destruct n. { exists (Build_NullGenerators Empty (fun _ => Unit)). split; [ exact _ | split; intros X _; [ | intros [] ] ]. intros i. apply ooextendable_equiv, isequiv_contr_contr. } pose (O := Nul B). pose (OeqB := reflexive_O_eq O : O <=> (Nul B)). change (Nul B) with O in Olex. clearbody O OeqB. revert B OeqB gtr. induction n; intros B OeqB gtr. { exists B; split; [ assumption | reflexivity ]. } pose (A := ngen_indices B). pose (C := A + { a:A & B(a) * B(a) }). pose (D := Build_NullGenerators C (fun c:C => match c with | inl a => merely (B a) | inr (a ; (b1, b2)) => (b1 = b2) end : Type)). assert (Dtrunc : forall c:C, IsTrunc n.+1 (D c)). { intros [a | [a [b1 b2]]]; [ cbn | exact _ ]. destruct n; exact _. } assert (OeqD : O <=> (Nul D)). { split; intros X. - intros X_inO c. assert (Bc : forall a:A, IsConnected O (B a)). { intros a. rapply (@isconnected_O_leq O (Nul B)). exact (isconnected_acc_ngen (Nul B) a). } apply (ooextendable_const_isconnected_inO O); [ destruct c as [a | [a [b1 b2]]] | exact X_inO ]. + apply isconnected_from_elim_to_O. destruct (isconnected_elim O (O (merely (B a))) (fun b => to O _ (tr b))) as [x h]. exists x; intros y; cbn in y. strip_truncations. exact (h y). + cbn. rapply isconnected_paths. - intros Dnull; rapply (@inO_leq (Nul B) O). intros a; cbn in a; cbn. apply ((equiv_ooextendable_isequiv (unit_name X) (fun _:B a => tt))^-1). apply isequiv_contr_map; intros f; cbn in f. refine (contr_equiv' { x:X & forall u:B a, x = f u } _). { refine (equiv_functor_sigma' (equiv_unit_rec X) _). intros x; unfold composeD; cbn. apply equiv_path_arrow. } refine ((isconnected_elim (Nul D) (A := D (inl a)) _ _).1). { rapply isconnected_acc_ngen. } intros b; cbn in b. strip_truncations. assert (bc : IsConnMap (Nul D) (unit_name b)). { intros x; unfold hfiber. apply (isconnected_equiv (Nul D) (b = x) (equiv_contr_sigma _)^-1). rapply (isconnected_acc_ngen (Nul D) (inr (a;(b,x)))). } pose (p := conn_map_elim (Nul D) (unit_name b) (fun u => f b = f u) (fun _ => 1)). apply (Build_Contr _ (f b ; p)); intros [x q]. refine (path_sigma' _ (q b)^ _); apply path_forall. refine (conn_map_elim (Nul D) (unit_name b) _ _); intros []. rewrite transport_forall_constant, transport_paths_l, inv_V. rewrite (conn_map_comp (Nul D) (unit_name b) (fun u:B a => f b = f u) (fun _ => 1) tt : p b = 1). apply concat_p1. } destruct (IHn D OeqD _) as [E [HE EeqD]]. exists E; split; [ exact HE | ]. refine (transitivity EeqD _). refine (transitivity _ OeqB). symmetry; assumption. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HoTT.Truncations. Require Import Accessible Lex Nullification.