type-theory.lagda.md

agda

workbook for TypeTheory course (Maietti, Sambin)

module TypeTheory where

-- import natural to have a better rappresentation inside the script
open import Data.Nat using (ℕ; zero; suc)

some enviroment setups

the syntax is almost the same as the Maietti's course book

-- Martin Lof propositional equality
data Id_,_ {A : Set} : A → A → Set where -- the sign is the formation rules
  id : (x : A) → Id x , x -- the constructors are the introduction elements of a type

-- elimination and conversion rule for ML equality
El-Id : ∀ -- the type specify the elimination rule
  {A : Set}
  {C : (x : A) → (y : A) → (z : Id x , y)  → Set}
  {a b : A}
  → (p : Id a , b)
  → ((x : A) → C x x (id x))
  → C a b p
El-Id (id a) c = c a -- the body specify the conversion rule

-- elimination and conversion rule for ℕ induction
El-ℕ : ∀ {D : ℕ → Set} → (m : ℕ) → (d : D 0) → (e : (x : ℕ) → D x → D (suc x)) → D m
El-ℕ zero d e = d
El-ℕ (suc m) d e = e m (El-ℕ m d e)

-- sum definition
_+_ : ℕ → ℕ → ℕ
x + y = El-ℕ x y (λ _ z → suc z)

-- definition of Product Type with dependence
data Σ {A : Set} (B : A → Set) : Set where
  ⟨_,_⟩ : (x : A) → B x → Σ λ(x' : A) → B x'

-- the function type is already defined but we can define the Π to obtain a notation
-- closer to ML
-- definition of Function type(Abstraction)
Π : {X : Set} → (Y : X → Set) → Set
Π {X} Y = (x : X) → Y x

-- left projection
proj₁ : {A : Set} {B : A → Set} → (Σ λ(x : A) → B x) → A
proj₁ ⟨ a , b ⟩ = a

-- right proj₁rojection
proj₂ : {A : Set} {B : A → Set} → (c : Σ λ(x : A) → B x) → B (proj₁ c)
proj₂ ⟨ a , b ⟩ = b

ES equality preservation among programs

eq-pres : ∀ {A B : Set} {a b : A} → (f : (x : A) → B) → Id a , b → Id (f a) , (f b)
eq-pres f w = El-Id w λ x → id (f x)

ES equality is symmetric

symmetric : ∀ {A : Set} {x y : A}
  → Id x , y → Id y , x
symmetric w = El-Id w id

ES transitivity

transitivity : ∀ {A : Set} {a b c : A}
  → Id a , b → Id b , c → Id a , c
transitivity w₁ w₂ =
  El-Id
    -- {A} -- type of Identity
    {C = λ x → λ y → λ _ → (Id _ , x → Id _ , y)} -- type of C, has to be explicit
    -- {b} -- a
    -- {c} -- b
    w₂ -- "base proof" p
    (λ _ → λ w → w) -- proof c, where the first x ∈ A is avoided
  w₁ -- El-Id applied to w₁

ES propositional equality among sum operator

-- lemma₁, x + 0 equal x
lemma₁ : (x : ℕ) → Id x , (x + 0)
lemma₁ x′ = El-ℕ x′ (id 0) k
  where
    k : (x : ℕ) → Id x , (x + 0) → Id (suc x) , ((suc x) + 0)
    k x z = El-Id {C = λ x → λ y → λ _ → Id (suc x) , (suc y)} z λ x → id (suc x)

-- lemma₂, x + suc(y) equal suc(x + y)
lemma₂ : (x y : ℕ) → Id (x + (suc y)) , (suc (x + y))
lemma₂ x′ y′ = El-ℕ {D = λ x → Id (x + (suc y′)) , (suc (x + y′))}
  x′
  (id (suc y′))
  λ _ → eq-pres suc -- note that z implict param

-- note that
-- El-ℕ x y λ x₂ → suc x₂ ≡ x + y, this holds for definition
-- El-ℕ y x λ x₂ → suc x₂ ≡ y + x, this holds for definition
-- then to proof x +₁ y ≡ x +₂ y you can proof x + y ≡ y + x (e.g. commutative)
eq-sum : (x y : ℕ) → Id (x + y) , (y + x)
eq-sum x′ y′ = El-ℕ {D = λ y → Id (x′ + y) , (y + x′)}
  y′
  (symmetric (lemma₁ x′))
  λ y z → transitivity {b = suc (x′ + y)} (lemma₂ x′ y) (eq-pres suc z)

ES axiom of choice

axiom-of-choice : {A : Set} {B : A → Set} {C : (x : A) → B x → Set}
  → Π λ(z : Π λ(x : A) → (Σ λ(y : B x) → C x y))
  → Σ λ(f : Π λ(x : A) → B x) → Π λ(x : A) → C x (f x)
axiom-of-choice = λ z → ⟨ (λ x → proj₁ (z x)) , (λ x → proj₂ (z x)) ⟩