{-
    T R U N C A T I O N   L E V E L S
                 I N
H O M O T O P Y   T Y P E   T H E O R Y

======= ELECTRONIC APPENDIX =======

           NICOLAI KRAUS

           February 2015
-}

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

module INDEX where

-- Chapter 2
open import Preliminaries
-- Parts of Chapter 2 are in a separate file:
open import Pointed

{- Chapter 3,4,5,6 are joint work with
   Martin Escardo, 
   Thierry Coquand, 
   Thorsten Altenkirch -}

-- Chapter 3
open import Truncation_Level_Criteria

-- Chapter 4
open import Anonymous_Existence_CollSplit
open import Anonymous_Existence_Populatedness
open import Anonymous_Existence_Comparison

-- Chapter 5
open import Weakly_Constant_Functions

-- Chapter 6
open import Judgmental_Computation

{- Chapter 7 (joint work with Christian Sattler)
   has two parts. First, we construct homotopically
   complicated types; this development is distributed 
   beween two files. Then, we discuss connectedness,
   which turns out to be very hard to formalise;
   we use in total five files to structure that 
   discussion, see below. -}

{- First, we have an auxiliary file which makes precise 
   that the 'universe of n-types' behaves like an actual
   universe. We formalise operations for it; this is 
   very useful as it allows a more 'principled' development. -}
open import UniverseOfNTypes
{- Now: Sections 1-4 of Chapter 7, where 1,2 are "hidden". 
   They are special cases of the more general theorem that 
   we prove in 7.4; the special cases are written out only
   for pedagogical reasons and are thus omitted in this 
   formalisation. -}
open import HHHUU-ComplicatedTypes

{- Note that Chapter 7.5 is not formalised, even though it 
   could have been; we omit it because it is only an 
   alternative to the above formalisation, and actually 
   leads to a weaker result than the one in 
   'HHHUU-ComplicatedTypes'. 

   Chapter 7.6 is very hard to formalise (mostly done by 
   Christian Sattler). Caveat: The order of the statements
   in the formalisation is different from the order in
   the thesis (it sometimes is more convenient to define
   multiple notions in the same module because they share
   argument to avoid replication of code, without them 
   belonging together logically).

   First, we show (in a separate file) that the non-dependent 
   universal property and the dependent universal
   property are equivalent. 

   Contains: Definition 7.6.2, Lemma 7.6.6 -}
open import Trunc.Universal

-- Definition 7.6.4, Lemma 7.6.7, Corollary 7.6.8
open import Trunc.Basics

-- Lemma 7.6.9, Lemma 7.6.10
-- (actually even a stronger version of Lemma 7.6.10)
open import Trunc.TypeConstructors

{- main part of connectedness:
   (link to 7.6.1,)
   Definition 7.6.13, Definition 7.6.11, 
   Lemma 7.6.14, Lemma 7.6.12, Lemma 7.6.15 
   and
   Theorem 7.7.1 -}
open import Trunc.Connection

-- Remark 7.6.16
open import Trunc.ConnectednessAlt


{- The main result of Chapter 8 is, unfortunately,
   meta-theoretical. It is plausible that in an 
   implementation of a type theory with 'two levels'
   (one semi-internal 'strict' equality and the
   ordinary identity type), the complete Chapter 8
   could be formalised; but at the moment, this is
   merely speculation. -}


-- Chapter 9.2: Semi-Simplicial Types

-- Proposition 9.2.1 (Δ₊ implemented with judgmental categorical laws)
open import Deltaplus