Back to index

Chapter 1. Type Theory

We begin with importing the Agda primitives and renaming them to match the notation of book.

module Chapter1.Book where

open import Agda.Primitive public
  renaming ( Set to Universe
           ; lsuc to infix 1 _⁺
           ; SetΟ‰ to 𝓀ω)

variable
  𝒾 𝒿 𝓀 𝓁 : Level

𝒰 : (β„“ : Level) β†’ Universe (β„“ ⁺)
𝒰 β„“ = Universe β„“

𝒰₀ = Universe lzero

_⁺⁺ : (β„“ : Level) β†’ Level
β„“ ⁺⁺ = (β„“ ⁺) ⁺

universe-of : {β„“ : Level} (A : 𝒰 β„“) β†’ Level
universe-of {β„“} A = β„“

Section 1.3 Universes and families

-- Workaround to have cumulativity
data Raised (𝒿 : Level) (A : 𝒰 𝒾) : 𝒰 (𝒾 βŠ” 𝒿) where
  raise : A β†’ Raised 𝒿 A

Section 1.4 Dependent function types

Ξ  : {A : 𝒰 𝒾} (B : A β†’ 𝒰 𝒿) β†’ 𝒰 (𝒾 βŠ” 𝒿)
Ξ  {𝒾} {𝒿} {A} B = (x : A) β†’ B x

-Ξ  : (A : 𝒰 𝒾) (B : A β†’ 𝒰 𝒿) β†’ 𝒰 (𝒾 βŠ” 𝒿)
-Ξ  A B = Ξ  B
infixr -1 -Ξ 

syntax -Ξ  A (Ξ» x β†’ b) = Ξ  x κž‰ A , b

id : {A : 𝒰 𝒾} β†’ A β†’ A
id a = a

𝑖𝑑 : (A : 𝒰 𝒾) β†’ A β†’ A
𝑖𝑑 A = id

swap : Ξ  A κž‰ 𝒰 𝒾 , Ξ  B κž‰ 𝒰 𝒿 , Ξ  C κž‰ 𝒰 𝓀 , ((A β†’ B β†’ C) β†’ (B β†’ A β†’ C))
swap A B C g b a = g a b

-- Helpers
domain : {A : 𝒰 𝒾} {B : 𝒰 𝒿} β†’ (A β†’ B) β†’ 𝒰 𝒾
domain {𝒾} {𝒿} {A} {B} f = A

codomain : {A : 𝒰 𝒾} {B : 𝒰 𝒿} β†’ (A β†’ B) β†’ 𝒰 𝒿
codomain {𝒾} {𝒿} {A} {B} f = B

Section 1.5 Product types

We define the product type as a particular case of the dependent pair type, see the next section.

data πŸ™ : 𝒰₀ where
  ⋆ : πŸ™

ind-πŸ™ : (A : πŸ™ β†’ 𝒰 𝒾) β†’ A ⋆ β†’ (x : πŸ™) β†’ A x
ind-πŸ™ A a ⋆ = a

Section 1.6 Dependent pairs types

record Ξ£ {A : 𝒰 𝒾} (B : A β†’ 𝒰 𝒿) : 𝒰 (𝒾 βŠ” 𝒿) where
  constructor
    _,_
  field
    x : A
    y : B x
infixr 50 _,_

-Ξ£ : (A : 𝒰 𝒾) (B : A β†’ 𝒰 𝒿) β†’ 𝒰 (𝒾 βŠ” 𝒿)
-Ξ£ A B = Ξ£ B
infixr -1 -Ξ£

syntax -Ξ£ A (Ξ» x β†’ y) = Ξ£ x κž‰ A , y

_Γ—_ : (A : 𝒰 𝒾) (B : 𝒰 𝒿) β†’ 𝒰 (𝒾 βŠ” 𝒿)
A Γ— B = Ξ£ x κž‰ A , B
infixr 30 _Γ—_

rec-Ξ£ : {A : 𝒰 𝒾} {B : A β†’ 𝒰 𝒿} {C : 𝒰 𝓀}
      β†’ ((x : A) (y : B x) β†’ C)
      β†’ Ξ£ B β†’ C
rec-Ξ£ g (x , y) = g x y

ind-Ξ£ : {A : 𝒰 𝒾} {B : A β†’ 𝒰 𝒿} {C : Ξ£ B β†’ 𝒰 𝓀}
      β†’ ((x : A) (y : B x) β†’ C (x , y))
      β†’ ((x , y) : Ξ£ B) β†’ C (x , y)
ind-Ξ£ g (x , y) = g x y

pr₁ : {A : 𝒰 𝒾} {B : A β†’ 𝒰 𝒿} β†’ Ξ£ B β†’ A
pr₁ (x , y) = x

prβ‚‚ : {A : 𝒰 𝒾} {B : A β†’ 𝒰 𝒿} β†’ (z : Ξ£ B) β†’ B (pr₁ z)
prβ‚‚ (x , y) = y

-- The type-theoretic axiom of choice
ac : {A : 𝒰 𝒾} {B : 𝒰 𝒿} {R : A β†’ B β†’ 𝒰 𝓀}
   β†’ (Ξ  x κž‰ A , Ξ£ y κž‰ B , R x y)
   β†’ (Ξ£ f κž‰ (A β†’ B) , Ξ  x κž‰ A , R x (f x))
ac g = ((Ξ» x β†’ pr₁ (g x)) , (Ξ» x β†’ prβ‚‚ (g x)))

-- The magma examples
Magma : {𝒾 : Level} β†’ 𝒰 (𝒾 ⁺)
Magma {𝒾} = Ξ£ A κž‰ 𝒰 𝒾 , (A β†’ A β†’ A)

PointedMagma : {𝒾 : Level} β†’ 𝒰 (𝒾 ⁺)
PointedMagma {𝒾} = Ξ£ A κž‰ 𝒰 𝒾 , ((A β†’ A β†’ A) Γ— A)

Section 1.7 Coproduct types

data _⊎_ (A : 𝒰 𝒾) (B : 𝒰 𝒿) : 𝒰 (𝒾 βŠ” 𝒿) where
 inl : A β†’ A ⊎ B
 inr : B β†’ A ⊎ B
infixr 20 _⊎_

⊎-rec : {A : 𝒰 𝒾} {B : 𝒰 𝒿} (C : 𝒰 𝓀)
      β†’ ((x : A) β†’ C)
      β†’ ((y : B) β†’ C)
      β†’ (A ⊎ B β†’ C)
⊎-rec C f g (inl x) = f x
⊎-rec C f g (inr y) = g y

⊎-ind : {A : 𝒰 𝒾} {B : 𝒰 𝒿} (C : A ⊎ B β†’ 𝒰 𝓀)
      β†’ ((x : A) β†’ C (inl x))
      β†’ ((y : B) β†’ C (inr y))
      β†’ (z : A ⊎ B) β†’ C z
⊎-ind C f g (inl x) = f x
⊎-ind C f g (inr y) = g y

data 𝟘 : 𝒰₀ where

ind-𝟘 : (A : 𝟘 β†’ 𝒰 𝒾) β†’ (x : 𝟘) β†’ A x
ind-𝟘 A ()

-- Simple helper
!𝟘 : (A : 𝒰 𝒾) β†’ 𝟘 β†’ A
!𝟘 A = ind-𝟘 (Ξ» _ β†’ A)

Section 1.8 The type of booleans

𝟚 : 𝒰₀
𝟚 = πŸ™ ⊎ πŸ™

pattern β‚€ = inl ⋆
pattern ₁ = inr ⋆

𝟚-rec : (C : 𝒰 𝒾) β†’ C β†’ C β†’ 𝟚 β†’ C
𝟚-rec C cβ‚€ c₁ β‚€ = cβ‚€
𝟚-rec C cβ‚€ c₁ ₁ = c₁

ind-𝟚 : (A : 𝟚 β†’ 𝒰 𝒾) β†’ A β‚€ β†’ A ₁ β†’ (n : 𝟚) β†’ A n
ind-𝟚 A aβ‚€ a₁ β‚€ = aβ‚€
ind-𝟚 A aβ‚€ a₁ ₁ = a₁

Section 1.9 The natural numbers

data β„• : 𝒰₀ where
  zero : β„•
  succ : β„• β†’ β„•
{-# BUILTIN NATURAL β„• #-}

double : β„• β†’ β„•
double 0 = 0
double (succ n) = succ (succ n)

add-β„• : β„• β†’ β„• β†’ β„•
add-β„• 0 n = n
add-β„• (succ m) n = succ (add-β„• m n)

rec-β„• : (C : 𝒰 𝒾)
      β†’ C β†’ (β„• β†’ C β†’ C)
      β†’ β„• β†’ C
rec-β„• C cβ‚€ cβ‚› zero = cβ‚€
rec-β„• C cβ‚€ cβ‚› (succ n) = cβ‚› n (rec-β„• C cβ‚€ cβ‚› n)

ind-β„• : (C : β„• β†’ 𝒰 𝒾)
      β†’ C 0
      β†’ ((n : β„•) β†’ C n β†’ C (succ n))
      β†’ (n : β„•) β†’ C n
ind-β„• C cβ‚€ cβ‚› 0 = cβ‚€
ind-β„• C cβ‚€ cβ‚› (succ n) = cβ‚› n (ind-β„• C cβ‚€ cβ‚› n)

Section 1.11 Propositions as types

Β¬ : 𝒰 𝒾 β†’ 𝒰 𝒾
Β¬ A = A β†’ 𝟘

-- Helpers
¬¬ ¬¬¬ : 𝒰 𝒾 β†’ 𝒰 𝒾
¬¬ A = ¬ (¬ A)
¬¬¬ A = ¬ (¬¬ A)

de-Morgan : {A : 𝒰 𝒾} {B : 𝒰 𝒿}
          β†’ (Β¬ A Γ— Β¬ B)
          β†’ (Β¬ (A ⊎ B))
de-Morgan (f , g) (inl a) = f a
de-Morgan (f , g) (inr b) = g b

Ξ -of-Γ— : {A : 𝒰 𝒾} {P : A β†’ 𝒰 𝒿} {Q : A β†’ 𝒰 𝒿} β†’
         (Ξ  x κž‰ A , P x Γ— Q x) β†’
         ((Ξ  x κž‰ A , P x) Γ— (Ξ  x κž‰ A , Q x))
Ξ -of-Γ— f = ((Ξ» x β†’ pr₁ (f x)) , (Ξ» x β†’ prβ‚‚ (f x)))

Section 1.12 Identity types

data Id (A : 𝒰 𝒾) : A β†’ A β†’ 𝒰 𝒾 where
  refl : (x : A) β†’ Id A x x
infix   0 Id

_≑_ : {A : 𝒰 𝒾} β†’ A β†’ A β†’ 𝒰 𝒾
x ≑ y = Id _ x y
infix   0 _≑_
{-# BUILTIN EQUALITY _≑_ #-}
{-# BUILTIN REWRITE _≑_ #-}

ind-≑ :
    (A : 𝒰 𝒾) (C : (x y : A) β†’ x ≑ y β†’ 𝒰 𝒿)
  β†’ ((x : A) β†’ C x x (refl x))
  β†’ (x y : A) (p : x ≑ y) β†’ C x y p
ind-≑ A C c x x (refl x) = c x

based-ind-≑ :
    (A : 𝒰 𝒾) (a : A)
    (C : (x : A) β†’ a ≑ x β†’ 𝒰 𝒿)
    (c : C a (refl a))
  β†’ (x : A) (p : a ≑ x) β†’ C x p
based-ind-≑ A a C c .a (refl .a) = c

--- Equivalence of path induction and based path induction
based-ind-≑⇒ind-≑ :
    (A : 𝒰 𝒾) (C : (x y : A) β†’ x ≑ y β†’ 𝒰 𝒿)
  β†’ ((x : A) β†’ C x x (refl x))
  β†’ (x y : A) (p : x ≑ y) β†’ C x y p
based-ind-≑⇒ind-≑ A C c x y p =
  based-ind-≑ A x (C x) (c x) y p

ind-≑⇒based-ind-≑ :
    (A : 𝒰 𝒾) (a : A)
    (C : (x : A) β†’ a ≑ x β†’ 𝒰 𝒿)
    (c : C a (refl a))
  β†’ (x : A) (p : a ≑ x) β†’ C x p
ind-≑⇒based-ind-≑ {𝒾} {𝒿} A a C c x p =
 ind-≑ A
   (Ξ» x y p β†’ (C : ((z : A) β†’ (x ≑ z) β†’ 𝒰 𝒿)) β†’ C x (refl x) β†’ C y p)
   (Ξ» x C d β†’ d) a x p C c

--- Disequality
_β‰’_ : {A : 𝒰 𝒾} β†’ A β†’ A β†’ 𝒰 𝒾
x β‰’ y = Β¬ (x ≑ y)