{- 

This is the Agda formalization of

      NOTIONS OF ANONYMOUS EXISTENCE IN MARTIN-LOF TYPE THEORY

                              by

Nicolai Kraus, Martin Escardo, Thierry Coquand, Thorsten Altenkirch

This file stays very close to the article. Because of this, not all 
proofs are given in the way that is most elegant for a formalization. 
In fact, often re-ordering statements would lead to a shorter 
presentation. The order that we have chosen in the article makes our 
results, as we hope, understandable and gives sufficient motivation.

This file type check with Agda 2.3.3 (and is expected to type check
with later versions).
-}

module INDEX_NotionsOfAnonymousExistence where

-- We use the following library files (some of them slightly modified 
-- by Christian Sattler in order to be useable with the current Agda 
-- version 2.3.3):

open import library.Basics hiding (Type ; Σ)
open import library.types.Sigma
open import library.types.Pi
open import library.types.Bool
open import library.NType2
open import library.types.Paths

-- OUR FORMALIZATION

-- Section 1: Introduction
-- (no formalization)

-- Section 2: Preliminaries
open import Sec2preliminaries

-- Section 3: Hedberg's Theorem
open import Sec3hedberg

-- Section 4: Collapsibility implies H-Stability
open import Sec4collapsibility

-- Section 5: Factorizing Weakly Constant Functions
open import Sec5factorConst

-- Section 6: Global Collapsibility implies Decidable Equality
open import Sec6collImplDecEq

-- Section 7: Populatedness
open import Sec7populatedness

-- Section 8: Taboos and Counter-Models
open import Sec8taboos

-- Section 9: Propositional Truncation with Judgmental Computation Rule
open import Sec9judgmentalBeta

-- Section 10: Conclusion and Open Problems
-- (no formalization)