{-# OPTIONS --without-K #-}

{- INDEX: Some constructions with non-recursive HITs,
   and related results.

   This formalization covers the hardest results of my
   paper titled "Constructions with non-recursive HITs".
   To be precise: I have formalized the result that all 
   functions in the sequence of approximations (see Section 6)
   are weakly constant, and that the colimit is thus 
   propositional. This requires a lot of lemmas. Some of 
   these lemmas are trivial on paper and only tedious in Agda,
   but many lemmas are (at least for me) even on paper far 
   from trivial. 

   Formalized are Section 2, Section 3 (without the example
   applications), especially the first main result; all of 
   Section 4 except Lemma 4.9, the definitions and principles 
   of Section 5, all of Section 6 expect the last corollaries.

   The parts of the paper that are not formalized are
   (A) the examples in Section 3
   (B) the statements of remarks
   (C) Lemma 4.9, 5.4, 5.5, and 5.6 
   (D) Theorem 5.7, Corollary 5.8, Theorem 6.2
   (E) the discussions and results in the concluding Section 7

   All of these are relatively easy compared with the results
   that are formalized. The items in (C) could be implemented
   easily, but are not very interesting on their own.
   The same is true for the second and third item in (D),
   which however depend on Theorem 5.7.
   Theorem 5.7 itself could be interesting to formalize. 
   However, it relies on the main result of 
       Capriotti, Kraus, Vezzosi,
       "Functions out of Higher Truncations".
   This result is formalized, but unfortunately in another
   library; thus, we omit Theorem 5.7 (for now) in the current 
   formalization. (E) would require (D) first.
   
   This development type-checks with Agda 2.4.2.5 and similar 
   versions (I assume with 2.4.2.x in general; same as the 
   HoTT library).
-}

module nicolai.pseudotruncations.NONRECURSIVE-INDEX where

{- Some preliminary definitions/lemmas, and an explanation
   why we need to work with the spheres defined by suspension-
   iteration of the form
   Σ¹⁺ⁿ :≡ Σⁿ ∘ Σ -}
open import nicolai.pseudotruncations.Preliminary-definitions
open import nicolai.pseudotruncations.Liblemmas

{- SECTION 2
   The Sequential colimit. I am aware that there is some
   overlap with lib/types/NatColim.agda -}
open import nicolai.pseudotruncations.SeqColim

{- Here is some prepartion for Section 3 -}
open import nicolai.pseudotruncations.wconst-preparation

{- The rather lengthy argument that some heptagon commutes;
   very tedious; this is still preparation for Section 3 -}
open import nicolai.pseudotruncations.heptagon

{- SECTION 3 (without the sample applications)
   One result of the paper: If we have a sequence of weakly 
   constant functions, then the colimit is propositional -}
open import nicolai.pseudotruncations.wconstSequence

{- SECTION 4
   The correspondance between loops and maps from spheres:
   a lot of tedious technical content. This was hard work for me!
   The results are in two files; first, essentially the fact that
   the 'pointed' 0-sphere [i.e. (bool, true)] is "as good as"
   the unit type if we consider pointed maps out of it.
   Second, the main lemmas. -}
open import nicolai.pseudotruncations.pointed-O-Sphere
open import nicolai.pseudotruncations.LoopsAndSpheres

{- SECTION 5 (mainly the definition and some auxiliary lemmas)
   Definition of pseudo-truncations -}
open import nicolai.pseudotruncations.PseudoTruncs

{- SECTION 6
   The sequence of approximations with increasing "connectedness-
   level", and the proof that every map is weakly constant,
   and the corollary that its colimit is propositional. -}
open import nicolai.pseudotruncations.PseudoTruncs-wconst-seq