{- 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)