Skip to content

Instantly share code, notes, and snippets.

@louisswarren louisswarren/tt.agda
Last active Sep 6, 2019

Embed
What would you like to do?
Type theory chapter of the HoTT book in 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.