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     β‰‘βŸ¨ refl _ ⟩
               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 _βˆ™_
infixr  0 _β‰‘βŸ¨_⟩_
infix   1 _∎
infix  40 _⁻¹
infixr -1 -Ξ£
infixr -1 -Ξ