Type theory chapter of the HoTT book in Agda

tt.agda

open import Agda.Builtin.Equality
open import Agda.Primitive

Π : ∀{a b} → (A : Set a) → (B : A → Set b) → Set (a ⊔ b)
Π A B = (x : A) → B x

syntax Π A (λ x → B) = Π[ x ∶ A ] B


record _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    pr₁ : A
    pr₂ : B
open _×_ public

rec[_×_] : ∀{a b c} → (A : Set a) → (B : Set b)
           → Π[ C ∶ Set c ] ((A → B → C) → A × B → C)
rec[ A × B ] C g (a , b) = g a b

pr₁′ : ∀{a b} {A : Set a} {B : Set b} → A × B → A
pr₁′ {a} {b} {A} {B} = rec[ A × B ] A λ a b → a

pr₂′ : ∀{a b} {A : Set a} {B : Set b} → A × B → B
pr₂′ {a} {b} {A} {B} = rec[ A × B ] B λ a b → b

_ : ∀{a b} {A : Set a} {B : Set b} → (x : A × B) → pr₁ x ≡ pr₁′ x
_ = λ _ → refl

_ : ∀{a b} {A : Set a} {B : Set b} → (x : A × B) → pr₂ x ≡ pr₂′ x
_ = λ _ → refl

uniq[_×_] : ∀{a b} → (A : Set a) → (B : Set b)
            → Π[ x ∶ A × B ] ((pr₁ x , pr₂ x) ≡ x)
uniq[ A × B ] (a , b) = refl

ind[_×_] : ∀{a b c} → (A : Set a) → (B : Set b)
           → Π[ C ∶ (A × B → Set c) ]
             (Π[ x ∶ A ] Π[ y ∶ B ] C (x , y) → Π[ x ∶ A × B ] C x)
ind[ A × B ] C g (a , b) = g a b


data 𝟙 : Set where
  ★ : 𝟙

rec[𝟙] : ∀{a} → Π[ C ∶ Set a ] (C → 𝟙 → C)
rec[𝟙] C c ★ = c

ind[𝟙] : ∀{c} → Π[ C ∶ (𝟙 → Set c) ] (C ★ → Π[ x ∶ 𝟙 ] C x)
ind[𝟙] C c ★ = c

uniq[𝟙] : Π[ x ∶ 𝟙 ] (★ ≡ x)
uniq[𝟙] = ind[𝟙] (★ ≡_) refl