Martin Escardo 1st May 2020.

This is ported from the Midlands Graduate School 2019 lecture notes

 https://www.cs.bham.ac.uk/~mhe/HoTT-UF.in-Agda-Lecture-Notes/HoTT-UF-Agda.html
 https://github.com/martinescardo/HoTT-UF.Agda-Lecture-Notes

\begin{code}

{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}

module MGS.MLTT where

open import MLTT.Universes public

open import MLTT.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 MLTT.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 MLTT.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 MLTT.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 MLTT.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 MLTT.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 -ฮ 

\end{code}