Agda UALib β

MartΓ­n EscardΓ³ 1st May 2020.

This is ported from the Midlands Graduate School 2019 lecture notes, which are available online from the following links.

html lecture notes

Source code repository

```
{-# OPTIONS --without-K --exact-split --safe #-}

module MGS-MLTT where

open import Universes public

open import Unit-Type renaming (π to π') public

π : π€β Μ
π = π' {π€β}

π-induction : (A : π β π€βΜ ) β A β β (x : π) β A x
π-induction A a β = a

π-recursion : (B : π€βΜ ) β B β (π β B)
π-recursion B b x = π-induction (Ξ» _ β B) b x

!π' : (X : π€βΜ ) β X β π
!π' X x = β

!π : {X : π€βΜ } β X β π
!π x = β

open import Empty-Type renaming (π to π') public

π : π€β Μ
π = π' {π€β}

π-induction : (A : π β π€ Μ ) β (x : π) β A x
π-induction A ()

π-recursion : (A : π€ Μ ) β π β A
π-recursion A a = π-induction (Ξ» _ β A) a

!π : (A : π€ Μ ) β π β A
!π = π-recursion

is-empty : π€ Μ β π€ Μ
is-empty X = X β π

Β¬ : π€ Μ β π€ Μ
Β¬ X = X β π

open import Natural-Numbers-Type public

β-induction : (A : β β π€ Μ )
β A 0
β ((n : β) β A n β A (succ n))
β (n : β) β A n

β-induction A aβ f = h
where
h : (n : β) β A n
h 0        = aβ
h (succ n) = f n (h n)

β-recursion : (X : π€ Μ )
β X
β (β β X β X)
β β β X

β-recursion X = β-induction (Ξ» _ β X)

β-iteration : (X : π€ Μ )
β X
β (X β X)
β β β X

β-iteration X x f = β-recursion X x (Ξ» _ x β f x)

module Arithmetic where

_+_  _Γ_ : β β β β β

x + 0      = x
x + succ y = succ (x + y)

x Γ 0      = 0
x Γ succ y = x + x Γ y

infixl 20 _+_
infixl 21 _Γ_

module Arithmetic' where

_+_  _Γ_ : β β β β β

x + y = h y
where
h : β β β
h = β-iteration β x succ

x Γ y = h y
where
h : β β β
h = β-iteration β 0 (x +_)

infixl 20 _+_
infixl 21 _Γ_

module β-order where

_β€_ _β₯_ : β β β β π€β Μ
0      β€ y      = π
succ x β€ 0      = π
succ x β€ succ y = x β€ y

x β₯ y = y β€ x

infix 10 _β€_
infix 10 _β₯_

open import Plus-Type renaming (_+_ to infixr 20 _+_) public

+-induction : {X : π€ Μ } {Y : π₯ Μ } (A : X + Y β π¦ Μ )
β ((x : X) β A (inl x))
β ((y : Y) β A (inr y))
β (z : X + Y) β A z

+-induction A f g (inl x) = f x
+-induction A f g (inr y) = g y

+-recursion : {X : π€ Μ } {Y : π₯ Μ } {A : π¦ Μ } β (X β A) β (Y β A) β X + Y β A
+-recursion {π€} {π₯} {π¦} {X} {Y} {A} = +-induction (Ξ» _ β A)

π : π€β Μ
π = π + π

pattern β = inl β
pattern β = inr β

π-induction : (A : π β π€ Μ ) β A β β A β β (n : π) β A n
π-induction A aβ aβ β = aβ
π-induction A aβ aβ β = aβ

π-induction' : (A : π β π€ Μ ) β A β β A β β (n : π) β A n
π-induction' A aβ aβ = +-induction A
(π-induction (Ξ» (x : π) β A (inl x)) aβ)
(π-induction (Ξ» (y : π) β A (inr y)) aβ)

open import Sigma-Type renaming (_,_ to infixr 50 _,_) public

prβ : {X : π€ Μ } {Y : X β π₯ Μ } β Ξ£ Y β X
prβ (x , y) = x

prβ : {X : π€ Μ } {Y : X β π₯ Μ } β (z : Ξ£ Y) β Y (prβ z)
prβ (x , y) = y

-Ξ£ : {π€ π₯ : Universe} (X : π€ Μ ) (Y : X β π₯ Μ ) β π€ β π₯ Μ
-Ξ£ X Y = Ξ£ Y

syntax -Ξ£ X (Ξ» x β Y) = Ξ£ x κ X , Y

Ξ£-induction : {X : π€ Μ } {Y : X β π₯ Μ } {A : Ξ£ Y β π¦ Μ }
β ((x : X) (y : Y x) β A (x , y))
β ((x , y) : Ξ£ Y) β A (x , y)

Ξ£-induction g (x , y) = g x y

curry : {X : π€ Μ } {Y : X β π₯ Μ } {A : Ξ£ Y β π¦ Μ }
β (((x , y) : Ξ£ Y) β A (x , y))
β ((x : X) (y : Y x) β A (x , y))

curry f x y = f (x , y)

_Γ_ : π€ Μ β π₯ Μ β π€ β π₯ Μ
X Γ Y = Ξ£ x κ X , Y

Ξ  : {X : π€ Μ } (A : X β π₯ Μ ) β π€ β π₯ Μ
Ξ  {π€} {π₯} {X} A = (x : X) β A x

-Ξ  : {π€ π₯ : Universe} (X : π€ Μ ) (Y : X β π₯ Μ ) β π€ β π₯ Μ
-Ξ  X Y = Ξ  Y

syntax -Ξ  A (Ξ» x β b) = Ξ  x κ A , b

id : {X : π€ Μ } β X β X
id x = x

ππ : (X : π€ Μ ) β X β X
ππ X = id

_β_ : {X : π€ Μ } {Y : π₯ Μ } {Z : Y β π¦ Μ }
β ((y : Y) β Z y)
β (f : X β Y)
β (x : X) β Z (f x)

g β f = Ξ» x β g (f x)

domain : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β π€ Μ
domain {π€} {π₯} {X} {Y} f = X

codomain : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β π₯ Μ
codomain {π€} {π₯} {X} {Y} f = Y

type-of : {X : π€ Μ } β X β π€ Μ
type-of {π€} {X} x = X

open import Identity-Type renaming (_β‘_ to infix 0 _β‘_ ; refl to π»β―π―π΅) public
pattern refl x = π»β―π―π΅ {x = x}

Id : (X : π€ Μ ) β X β X β π€ Μ
Id _ x y = x β‘ y

π : (X : π€ Μ ) (A : (x y : X) β x β‘ y β π₯ Μ )
β ((x : X) β A x x (refl x))
β (x y : X) (p : x β‘ y) β A x y p

π X A f x x (refl x) = f x

β : {X : π€ Μ } (x : X) (B : (y : X) β x β‘ y β π₯ Μ )
β B x (refl x)
β (y : X) (p : x β‘ y) β B y p

β x B b x (refl x) = b

π' : (X : π€ Μ ) (A : (x y : X) β x β‘ y β π₯ Μ )
β ((x : X) β A x x (refl x))
β (x y : X) (p : x β‘ y) β A x y p

π' X A f x = β x (A x) (f x)

πs-agreement : (X : π€ Μ ) (A : (x y : X) β x β‘ y β π₯ Μ )
(f : (x : X) β A x x (refl x)) (x y : X) (p : x β‘ y)
β π X A f x y p β‘ π' X A f x y p

πs-agreement X A f x x (refl x) = refl (f x)

transport : {X : π€ Μ } (A : X β π₯ Μ ) {x y : X}
β x β‘ y β A x β A y

transport A (refl x) = ππ (A x)

transportπ : {X : π€ Μ } (A : X β π₯ Μ ) {x y : X}
β x β‘ y β A x β A y

transportπ {π€} {π₯} {X} A {x} {y} = π X (Ξ» x y _ β A x β A y) (Ξ» x β ππ (A x)) x y

nondep-β : {X : π€ Μ } (x : X) (A : X β π₯ Μ )
β A x β (y : X) β x β‘ y β A y
nondep-β x A = β x (Ξ» y _ β A y)

transportβ : {X : π€ Μ } (A : X β π₯ Μ ) {x y : X}
β x β‘ y β A x β A y
transportβ A {x} {y} p a = nondep-β x A a y p

transports-agreement : {X : π€ Μ } (A : X β π₯ Μ ) {x y : X} (p : x β‘ y)
β (transportβ A p β‘ transport A p)
Γ (transportπ A p β‘ transport A p)

transports-agreement A (refl x) = refl (transport A (refl x)) ,
refl (transport A (refl x))

lhs : {X : π€ Μ } {x y : X} β x β‘ y β X
lhs {π€} {X} {x} {y} p = x

rhs : {X : π€ Μ } {x y : X} β x β‘ y β X
rhs {π€} {X} {x} {y} p = y

_β_ : {X : π€ Μ } {x y z : X} β x β‘ y β y β‘ z β x β‘ z
p β q = transport (lhs p β‘_) q p

_β‘β¨_β©_ : {X : π€ Μ } (x : X) {y z : X} β x β‘ y β y β‘ z β x β‘ z
x β‘β¨ p β© q = p β q

_β : {X : π€ Μ } (x : X) β x β‘ x
x β = refl x

_β»ΒΉ : {X : π€ Μ } β {x y : X} β x β‘ y β y β‘ x
p β»ΒΉ = transport (_β‘ lhs p) p (refl (lhs p))

_β'_ : {X : π€ Μ } {x y z : X} β x β‘ y β y β‘ z β x β‘ z
p β' q = transport (_β‘ rhs q) (p β»ΒΉ) q

βagreement : {X : π€ Μ } {x y z : X} (p : x β‘ y) (q : y β‘ z)
β p β' q β‘ p β q

βagreement (refl x) (refl x) = refl (refl x)

rdnel : {X : π€ Μ } {x y : X} (p : x β‘ y)
β p β refl y β‘ p

rdnel p = refl p

rdner : {X : π€ Μ } {y z : X} (q : y β‘ z)
β refl y  β' q β‘ q

rdner q = refl q

ap : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) {x x' : X} β x β‘ x' β f x β‘ f x'
ap f {x} {x'} p = transport (Ξ» - β f x β‘ f -) p (refl (f x))

_βΌ_ : {X : π€ Μ } {A : X β π₯ Μ } β Ξ  A β Ξ  A β π€ β π₯ Μ
f βΌ g = β x β f x β‘ g x

Β¬Β¬ Β¬Β¬Β¬ : π€ Μ β π€ Μ
Β¬Β¬  A = Β¬(Β¬ A)
Β¬Β¬Β¬ A = Β¬(Β¬Β¬ A)

dni : (A : π€ Μ ) β A β Β¬Β¬ A
dni A a u = u a

contrapositive : {A : π€ Μ } {B : π₯ Μ } β (A β B) β (Β¬ B β Β¬ A)
contrapositive f v a = v (f a)

tno : (A : π€ Μ ) β Β¬Β¬Β¬ A β Β¬ A
tno A = contrapositive (dni A)

_β_ : π€ Μ β π₯ Μ β π€ β π₯ Μ
X β Y = (X β Y) Γ (Y β X)

lr-implication : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β (X β Y)
lr-implication = prβ

rl-implication : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β (Y β X)
rl-implication = prβ

absurdityΒ³-is-absurdity : {A : π€ Μ } β Β¬Β¬Β¬ A β Β¬ A
absurdityΒ³-is-absurdity {π€} {A} = firstly , secondly
where
firstly : Β¬Β¬Β¬ A β Β¬ A
firstly = contrapositive (dni A)

secondly : Β¬ A β Β¬Β¬Β¬ A
secondly = dni (Β¬ A)

_β’_ : {X : π€ Μ } β X β X β π€ Μ
x β’ y = Β¬(x β‘ y)

β’-sym : {X : π€ Μ } {x y : X} β x β’ y β y β’ x
β’-sym {π€} {X} {x} {y} u = Ξ» (p : y β‘ x) β u (p β»ΒΉ)

IdβFun : {X Y : π€ Μ } β X β‘ Y β X β Y
IdβFun {π€} = transport (ππ (π€ Μ ))

IdβFun' : {X Y : π€ Μ } β X β‘ Y β X β Y
IdβFun' (refl X) = ππ X

IdβFuns-agree : {X Y : π€ Μ } (p : X β‘ Y)
β IdβFun p β‘ IdβFun' p

IdβFuns-agree (refl X) = refl (ππ X)

π-is-not-π : π β’ π
π-is-not-π p = IdβFun p β

β-is-not-β : β β’ β
β-is-not-β p = π-is-not-π q
where
f : π β π€β Μ
f β = π
f β = π

q : π β‘ π
q = ap f p

decidable : π€ Μ β π€ Μ
decidable A = A + Β¬ A

has-decidable-equality : (X : π€ Μ ) β π€ Μ
has-decidable-equality X = (x y : X) β decidable (x β‘ y)

π-has-decidable-equality : has-decidable-equality π
π-has-decidable-equality β β = inl (refl β)
π-has-decidable-equality β β = inr (β’-sym β-is-not-β)
π-has-decidable-equality β β = inr β-is-not-β
π-has-decidable-equality β β = inl (refl β)

not-zero-is-one : (n : π) β n β’ β β n β‘ β
not-zero-is-one β f = !π (β β‘ β) (f (refl β))
not-zero-is-one β f = refl β

inl-inr-disjoint-images : {X : π€ Μ } {Y : π₯ Μ } {x : X} {y : Y} β inl x β’ inr y
inl-inr-disjoint-images {π€} {π₯} {X} {Y} p = π-is-not-π q
where
f : X + Y β π€β Μ
f (inl x) = π
f (inr y) = π

q : π β‘ π
q = ap f p

right-fails-gives-left-holds : {P : π€ Μ } {Q : π₯ Μ } β P + Q β Β¬ Q β P
right-fails-gives-left-holds (inl p) u = p
right-fails-gives-left-holds (inr q) u = !π _ (u q)

module twin-primes where

open Arithmetic renaming (_Γ_ to _*_ ; _+_ to _β_)
open β-order

is-prime : β β π€β Μ
is-prime n = (n β₯ 2) Γ ((x y : β) β x * y β‘ n β (x β‘ 1) + (x β‘ n))

twin-prime-conjecture : π€β Μ
twin-prime-conjecture = (n : β) β Ξ£ p κ β , (p β₯ n)
Γ is-prime p
Γ is-prime (p β 2)

positive-not-zero : (x : β) β succ x β’ 0
positive-not-zero x p = π-is-not-π (g p)
where
f : β β π€β Μ
f 0        = π
f (succ x) = π

g : succ x β‘ 0 β π β‘ π
g = ap f

pred : β β β
pred 0 = 0
pred (succ n) = n

succ-lc : {x y : β} β succ x β‘ succ y β x β‘ y
succ-lc = ap pred

β-has-decidable-equality : has-decidable-equality β
β-has-decidable-equality 0 0               = inl (refl 0)
β-has-decidable-equality 0 (succ y)        = inr (β’-sym (positive-not-zero y))
β-has-decidable-equality (succ x) 0        = inr (positive-not-zero x)
β-has-decidable-equality (succ x) (succ y) = f (β-has-decidable-equality x y)
where
f : decidable (x β‘ y) β decidable (succ x β‘ succ y)
f (inl p) = inl (ap succ p)
f (inr k) = inr (Ξ» (s : succ x β‘ succ y) β k (succ-lc s))

module basic-arithmetic-and-order where

open β-order public
open Arithmetic renaming (_+_ to _β_) hiding (_Γ_)

+-assoc : (x y z : β) β (x β y) β z β‘ x β (y β z)

+-assoc x y zero     = (x β y) β 0 β‘β¨ refl _ β©
x β (y β 0) β

+-assoc x y (succ z) = (x β y) β succ z   β‘β¨ refl _     β©
succ ((x β y) β z) β‘β¨ ap succ IH β©
succ (x β (y β z)) β‘β¨ refl _     β©
x β (y β succ z)   β
where
IH : (x β y) β z β‘ x β (y β z)
IH = +-assoc x y z

+-assoc' : (x y z : β) β (x β y) β z β‘ x β (y β z)
+-assoc' x y zero     = refl _
+-assoc' x y (succ z) = ap succ (+-assoc' x y z)

+-base-on-first : (x : β) β 0 β x β‘ x

+-base-on-first 0        = refl 0

+-base-on-first (succ x) = 0 β succ x   β‘β¨ refl _     β©
succ (0 β x) β‘β¨ ap succ IH β©
succ x       β
where
IH : 0 β x β‘ x
IH = +-base-on-first x

+-step-on-first : (x y : β) β succ x β y β‘ succ (x β y)

+-step-on-first x zero     = refl (succ x)

+-step-on-first x (succ y) = succ x β succ y   β‘β¨ refl _     β©
succ (succ x β y) β‘β¨ ap succ IH β©
succ (x β succ y) β
where
IH : succ x β y β‘ succ (x β y)
IH = +-step-on-first x y

+-comm : (x y : β) β x β y β‘ y β x

+-comm 0 y = 0 β y β‘β¨ +-base-on-first y β©
y β 0 β

+-comm (succ x) y = succ x β y  β‘β¨ +-step-on-first x y β©
succ(x β y) β‘β¨ ap succ IH          β©
succ(y β x) β‘β¨ refl _              β©
y β succ x  β
where
IH : x β y β‘ y β x
IH = +-comm x y

+-lc : (x y z : β) β x β y β‘ x β z β y β‘ z

+-lc 0        y z p = y     β‘β¨ (+-base-on-first y)β»ΒΉ β©
0 β y β‘β¨ p                     β©
0 β z β‘β¨ +-base-on-first z     β©
z     β

+-lc (succ x) y z p = IH
where
q = succ (x β y) β‘β¨ (+-step-on-first x y)β»ΒΉ β©
succ x β y   β‘β¨ p                       β©
succ x β z   β‘β¨ +-step-on-first x z     β©
succ (x β z) β

IH : y β‘ z
IH = +-lc x y z (succ-lc q)

_βΌ_ : β β β β π€β Μ
x βΌ y = Ξ£ z κ β , x β z β‘ y

β€-gives-βΌ : (x y : β) β x β€ y β x βΌ y
β€-gives-βΌ 0 0               l = 0 , refl 0
β€-gives-βΌ 0 (succ y)        l = succ y , +-base-on-first (succ y)
β€-gives-βΌ (succ x) 0        l = !π (succ x βΌ zero) l
β€-gives-βΌ (succ x) (succ y) l = Ξ³
where
IH : x βΌ y
IH = β€-gives-βΌ x y l

z : β
z = prβ IH

p : x β z β‘ y
p = prβ IH

Ξ³ : succ x βΌ succ y
Ξ³ = z , (succ x β z   β‘β¨ +-step-on-first x z β©
succ (x β z) β‘β¨ ap succ p           β©
succ y       β)

βΌ-gives-β€ : (x y : β) β x βΌ y β x β€ y

βΌ-gives-β€ 0 0               (z , p) = β

βΌ-gives-β€ 0 (succ y)        (z , p) = β

βΌ-gives-β€ (succ x) 0        (z , p) = positive-not-zero (x β z) q
where
q = succ (x β z) β‘β¨ (+-step-on-first x z)β»ΒΉ β©
succ x β z   β‘β¨ p                       β©
zero         β

βΌ-gives-β€ (succ x) (succ y) (z , p) = IH
where
q = succ (x β z) β‘β¨ (+-step-on-first x z)β»ΒΉ β©
succ x β z   β‘β¨ p                       β©
succ y       β

IH : x β€ y
IH = βΌ-gives-β€ x y (z , succ-lc q)

β€-refl : (n : β) β n β€ n
β€-refl zero     = β
β€-refl (succ n) = β€-refl n

β€-trans : (l m n : β) β l β€ m β m β€ n β l β€ n
β€-trans zero m n p q = β
β€-trans (succ l) zero n p q = !π (succ l β€ n) p
β€-trans (succ l) (succ m) zero p q = q
β€-trans (succ l) (succ m) (succ n) p q = β€-trans l m n p q

β€-anti : (m n : β) β m β€ n β n β€ m β m β‘ n
β€-anti zero zero p q = refl zero
β€-anti zero (succ n) p q = !π (zero β‘ succ n) q
β€-anti (succ m) zero p q = !π (succ m β‘ zero) p
β€-anti (succ m) (succ n) p q = ap succ (β€-anti m n p q)

β€-succ : (n : β) β n β€ succ n
β€-succ zero     = β
β€-succ (succ n) = β€-succ n

zero-minimal : (n : β) β zero β€ n
zero-minimal n = β

unique-minimal : (n : β) β n β€ zero β n β‘ zero
unique-minimal zero p = refl zero
unique-minimal (succ n) p = !π (succ n β‘ zero) p

β€-split : (m n : β) β m β€ succ n β (m β€ n) + (m β‘ succ n)
β€-split zero n l = inl l
β€-split (succ m) zero l = inr (ap succ (unique-minimal m l))
β€-split (succ m) (succ n) l = +-recursion inl (inr β ap succ) (β€-split m n l)

_<_ : β β β β π€β Μ
x < y = succ x β€ y

infix 10 _<_

not-<-gives-β₯ : (m n : β) β Β¬(n < m) β m β€ n
not-<-gives-β₯ zero n u = zero-minimal n
not-<-gives-β₯ (succ m) zero = dni (zero < succ m) (zero-minimal m)
not-<-gives-β₯ (succ m) (succ n) = not-<-gives-β₯ m n

bounded-β-next : (A : β β π€ Μ ) (k : β)
β A k
β ((n : β) β n < k β A n)
β (n : β) β n < succ k β A n
bounded-β-next A k a Ο n l = +-recursion f g s
where
s : (n < k) + (succ n β‘ succ k)
s = β€-split (succ n) k l

f : n < k β A n
f = Ο n

g : succ n β‘ succ k β A n
g p = transport A ((succ-lc p)β»ΒΉ) a

root : (β β β) β π€β Μ
root f = Ξ£ n κ β , f n β‘ 0

_has-no-root<_ : (β β β) β β β π€β Μ
f has-no-root< k = (n : β) β n < k β f n β’ 0

is-minimal-root : (β β β) β β β π€β Μ
is-minimal-root f m = (f m β‘ 0) Γ (f has-no-root< m)

at-most-one-minimal-root : (f : β β β) (m n : β)
β is-minimal-root f m β is-minimal-root f n β m β‘ n

at-most-one-minimal-root f m n (p , Ο) (q , Ο) = c m n a b
where
a : Β¬(m < n)
a u = Ο m u p

b : Β¬(n < m)
b v = Ο n v q

c : (m n : β) β Β¬(m < n) β Β¬(n < m) β m β‘ n
c m n u v = β€-anti m n (not-<-gives-β₯ m n v) (not-<-gives-β₯ n m u)

minimal-root : (β β β) β π€β Μ
minimal-root f = Ξ£ m κ β , is-minimal-root f m

minimal-root-is-root : β f β minimal-root f β root f
minimal-root-is-root f (m , p , _) = m , p

bounded-β-search : β k f β (minimal-root f) + (f has-no-root< k)
bounded-β-search zero f = inr (Ξ» n β !π (f n β’ 0))
bounded-β-search (succ k) f = +-recursion Ο Ξ³ (bounded-β-search k f)
where
A : β β (β β β) β π€β Μ
A k f = (minimal-root f) + (f has-no-root< k)

Ο : minimal-root f β A (succ k) f
Ο = inl

Ξ³ : f has-no-root< k β A (succ k) f
Ξ³ u = +-recursion Ξ³β Ξ³β (β-has-decidable-equality (f k) 0)
where
Ξ³β : f k β‘ 0 β A (succ k) f
Ξ³β p = inl (k , p , u)

Ξ³β : f k β’ 0 β A (succ k) f
Ξ³β v = inr (bounded-β-next (Ξ» n β f n β’ 0) k v u)

root-gives-minimal-root : β f β root f β minimal-root f
root-gives-minimal-root f (n , p) = Ξ³
where
g : Β¬(f has-no-root< (succ n))
g Ο = Ο n (β€-refl n) p

Ξ³ : minimal-root f
Ξ³ = right-fails-gives-left-holds (bounded-β-search (succ n) f) g

infixr 30 _Γ_
infix   0 _βΌ_
infixl 70 _β_
infix   0 Id
infix  10 _β_
infixl 30 _β_