Begin by downloading the file FunExtPostulate.agda and put it in your working folder.

Create a file named HLevels.agda and make it begin with

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

open import Prelude
open import Path
open import FunExtPostulate

private variable
  ℓ ℓ' : Level

1 Contractibility

Define the predicate of being contractible by

isContr : Type ℓ → Type ℓ
isContr A = Σ A (λ x → (y : A) → x ≡ y)

1.1 The terminal type is contractible

Show that the terminal type ⊤ is contractible

isContr⊤ : isContr ⊤

1.2 Bool is not contractible

Show that booleans are not contractible

¬isContrBool : ¬ (isContr Bool)

1.3 Products are contractible

Show that the product of contractible types is contractible

isContr× : {A : Type ℓ} {B : Type ℓ'} → isContr A → isContr B → isContr (A × B)

1.4 Path types

Show that contractible types have contractible path types

isContr→isContrPath : {A : Type ℓ} → isContr A → (x y : A) → isContr (x ≡ y)

1.5 Singleton types

We define singleton types as

singl : {A : Type ℓ} → A → Type ℓ
singl {A = A} a = Σ A λ x → a ≡ x

Show that singleton types are contractible

isContrSingl : {A : Type ℓ} (a : A) → isContr (singl a)
isContrSingl a = (a , refl) , λ { (x , p) → Σ≡ p (substInPathsL refl p ∙ sym (lUnit _)) }

2 Propositions

TODO: propositional truncation