----------------------------------------------------------------------------------------------------
-- Cantor Normal Forms as subset of unlabeled binary trees
----------------------------------------------------------------------------------------------------

{- We work with the mutual definition of Cantor Normal Forms and its
   ordering, which has been developed in

     Fredrik Nordvall Forsberg, Chuangjie Xu, and Neil Ghani.
     Threee quivalent ordinal notation systems in cubical agda.
     In Proceedings of the 9th ACM SIGPLAN International Conference
     on Certified Programs and Proofs, CPP 2020, page 172โ€“185.
     Association for Computing Machinery, 2020.
-}

{-# OPTIONS --cubical --safe #-}

module CantorNormalForm.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Everything
open import Cubical.Data.Sum
open import Cubical.Data.Sigma
open import Cubical.Data.Empty
  renaming (rec to โŠฅ-rec)
open import Cubical.Relation.Nullary
open import Cubical.Data.Nat
  using (โ„• ; zero ; suc)

open import General-Properties


{- Cantor Normal Forms -}

mutual

 data Cnf : Set where
  ๐ŸŽ : Cnf
  ฯ‰^_+_[_] : (a b : Cnf) โ†’ (a โ‰ฅ left b) โ†’ Cnf

 data _<_ : Cnf โ†’ Cnf โ†’ Set where
  <โ‚ : โˆ€ {a b r}                       โ†’ ๐ŸŽ              < ฯ‰^ a + b [ r ]
  <โ‚‚ : โˆ€ {a b c d r s} โ†’ a < b         โ†’ ฯ‰^ a + c [ r ] < ฯ‰^ b + d [ s ]
  <โ‚ƒ : โˆ€ {a b c d r s} โ†’ a โ‰ก b โ†’ c < d โ†’ ฯ‰^ a + c [ r ] < ฯ‰^ b + d [ s ]

 left : Cnf โ†’ Cnf
 left  ๐ŸŽ               = ๐ŸŽ
 left (ฯ‰^ a + _ [ _ ]) = a

 _>_ _โ‰ฅ_ _โ‰ค_ : Cnf โ†’ Cnf โ†’ Set
 a > b =  b < a
 a โ‰ฅ b = (a > b) โŠŽ (a โ‰ก b)
 a โ‰ค b =  b โ‰ฅ a


{- Basic properties of CNF -}

<โ‚‚' : โˆ€ {a b} โ†’ left a < left b โ†’ a < b
<โ‚‚' {๐ŸŽ} {ฯ‰^ _ + _ [ x ]} _ = <โ‚
<โ‚‚' {ฯ‰^ _ + _ [ _ ]} {ฯ‰^ _ + _ [ _ ]} a<b = <โ‚‚ a<b

<โ‚‚'' : โˆ€ {a b d s} โ†’ left a < b โ†’ a < ฯ‰^ b + d [ s ]
<โ‚‚'' {๐ŸŽ} _ = <โ‚
<โ‚‚'' {ฯ‰^ _ + _ [ _ ]} a<b = <โ‚‚ a<b

right : Cnf โ†’ Cnf
right  ๐ŸŽ               = ๐ŸŽ
right (ฯ‰^ _ + b [ _ ]) = b

caseCnf : โˆ€ {โ„“} {A : Type โ„“} (x y : A) โ†’ Cnf โ†’ A
caseCnf x y  ๐ŸŽ               = x
caseCnf x y (ฯ‰^ _ + _ [ _ ]) = y

๐ŸŽโ‰ขฯ‰ : โˆ€ {a b} {r : a โ‰ฅ left b} โ†’ ยฌ (๐ŸŽ โ‰ก ฯ‰^ a + b [ r ])
๐ŸŽโ‰ขฯ‰ e = subst (caseCnf Cnf โŠฅ) e ๐ŸŽ

ฯ‰โ‰ข๐ŸŽ : โˆ€ {a b} {r : a โ‰ฅ left b} โ†’ ยฌ (ฯ‰^ a + b [ r ] โ‰ก ๐ŸŽ)
ฯ‰โ‰ข๐ŸŽ e = subst (caseCnf โŠฅ Cnf) e ๐ŸŽ

๐ŸŽโ‰ค : {a : Cnf} โ†’ ๐ŸŽ โ‰ค a
๐ŸŽโ‰ค {๐ŸŽ} = inr (refl)
๐ŸŽโ‰ค {ฯ‰^ a + b [ r ]} = inl <โ‚

โ‰ฎ๐ŸŽ : โˆ€ {a} โ†’ ยฌ (a < ๐ŸŽ)
โ‰ฎ๐ŸŽ ()

ฯ‰^โ‰ฐ๐ŸŽ : โˆ€ {a b r} โ†’ ยฌ (ฯ‰^ a + b [ r ] โ‰ค ๐ŸŽ)
ฯ‰^โ‰ฐ๐ŸŽ (inr e) = ๐ŸŽโ‰ขฯ‰ e

โ‰ค๐ŸŽโ†’โ‰ก๐ŸŽ : โˆ€ {a} โ†’ a โ‰ค ๐ŸŽ โ†’ a โ‰ก ๐ŸŽ
โ‰ค๐ŸŽโ†’โ‰ก๐ŸŽ (inr e) = sym e

left-is-โ‰ค-monotone : {a b : Cnf} โ†’ a โ‰ค b โ†’ left a โ‰ค left b
left-is-โ‰ค-monotone (inl <โ‚) = ๐ŸŽโ‰ค
left-is-โ‰ค-monotone (inl (<โ‚‚ r)) = inl r
left-is-โ‰ค-monotone (inl (<โ‚ƒ e r)) = inr (sym e)
left-is-โ‰ค-monotone (inr e) = inr (cong left e)

left-is-<-โ‰ค-monotone : {a b : Cnf} โ†’ a < b โ†’ left a โ‰ค left b
left-is-<-โ‰ค-monotone r = left-is-โ‰ค-monotone (inl r)

<-irrefl : โˆ€ {a} โ†’ ยฌ a < a
<-irrefl (<โ‚‚ r)     = <-irrefl r
<-irrefl (<โ‚ƒ a=a r) = <-irrefl r

<-irreflexive : โˆ€ {a b} โ†’ a โ‰ก b โ†’ ยฌ a < b
<-irreflexive e = subst (ฮป x โ†’ ยฌ _ < x) e <-irrefl

<-trans : โˆ€ {a b c} โ†’ a < b โ†’ b < c โ†’ a < c
<-trans  <โ‚      (<โ‚‚ _)   = <โ‚
<-trans  <โ‚      (<โ‚ƒ _ _) = <โ‚
<-trans (<โ‚‚ r)   (<โ‚‚ s)   = <โ‚‚ (<-trans r s)
<-trans (<โ‚‚ r)   (<โ‚ƒ p _) = <โ‚‚ (subst (ฮป x โ†’ _ < x) p r)
<-trans (<โ‚ƒ p _) (<โ‚‚ s)   = <โ‚‚ (subst (ฮป x โ†’ x < _) (sym p) s)
<-trans (<โ‚ƒ p r) (<โ‚ƒ q s) = <โ‚ƒ (p โˆ™ q) (<-trans r s)

left< : {a b : Cnf} {r : a โ‰ฅ left b} โ†’ a < ฯ‰^ a + b [ r ]
left< {๐ŸŽ} = <โ‚
left< {ฯ‰^ a + c [ s ]} = <โ‚‚ left<

leftโ‰ค : {a : Cnf} โ†’ left a โ‰ค a
leftโ‰ค {๐ŸŽ} = inr refl
leftโ‰ค {ฯ‰^ a + b [ r ]} = inl left<

right< : (a b : Cnf) (r : a โ‰ฅ left b) โ†’ b < ฯ‰^ a + b [ r ]
right< a  ๐ŸŽ                _      = <โ‚
right< a (ฯ‰^ b + c [ s ]) (inl r) = <โ‚‚ r
right< a (ฯ‰^ b + c [ s ]) (inr e) = <โ‚ƒ (sym e) (right< b c s)

rightโ‰ค : (a : Cnf) โ†’ right a โ‰ค a
rightโ‰ค ๐ŸŽ = inr refl
rightโ‰ค (ฯ‰^ a + b [ r ]) = inl (right< a b r)

ฯ‰^<-cases : โˆ€ {a b c d r s}
          โ†’ ฯ‰^ a + c [ r ] < ฯ‰^ b + d [ s ]
          โ†’ (a < b) โŠŽ ((a โ‰ก b) ร— (c < d))
ฯ‰^<-cases (<โ‚‚ a<b)     = inl a<b
ฯ‰^<-cases (<โ‚ƒ aโ‰กb c<d) = inr (aโ‰กb , c<d)

<โ†’โ‰ฏ : {a b : Cnf} โ†’ a < b โ†’ ยฌ (a > b)
<โ†’โ‰ฏ (<โ‚‚ r)   (<โ‚‚ s)   = <โ†’โ‰ฏ r s
<โ†’โ‰ฏ (<โ‚‚ r)   (<โ‚ƒ e s) = <-irreflexive (sym e) r
<โ†’โ‰ฏ (<โ‚ƒ e r) (<โ‚‚ s)   = <-irreflexive (sym e) s
<โ†’โ‰ฏ (<โ‚ƒ e r) (<โ‚ƒ _ s) = <โ†’โ‰ฏ r s

<โ†’โ‰ฑ : {a b : Cnf} โ†’ a < b โ†’ ยฌ (a โ‰ฅ b)
<โ†’โ‰ฑ a<b (inl a>b) = <โ†’โ‰ฏ a<b a>b
<โ†’โ‰ฑ a<b (inr aโ‰กb) = <-irreflexive aโ‰กb a<b

โ‰คโ†’โ‰ฏ : {a b : Cnf} โ†’ a โ‰ค b โ†’ ยฌ (a > b)
โ‰คโ†’โ‰ฏ (inl a<b) = <โ†’โ‰ฏ a<b
โ‰คโ†’โ‰ฏ (inr bโ‰กa) = <-irreflexive bโ‰กa

โ‰คโˆงโ‰ฎโ†’โ‰ก : {a b : Cnf} โ†’ a โ‰ค b โ†’ ยฌ (a < b) โ†’ a โ‰ก b
โ‰คโˆงโ‰ฎโ†’โ‰ก (inl a<b) aโ‰ฎb = โŠฅ-rec (aโ‰ฎb a<b)
โ‰คโˆงโ‰ฎโ†’โ‰ก (inr bโ‰กa) _ = sym bโ‰กa

โ‰คโˆงโ‰ฅโ†’โ‰ก : {a b : Cnf} โ†’ a โ‰ค b โ†’ a โ‰ฅ b โ†’ a โ‰ก b
โ‰คโˆงโ‰ฅโ†’โ‰ก aโ‰คb aโ‰ฅb = โ‰คโˆงโ‰ฎโ†’โ‰ก aโ‰คb (โ‰คโ†’โ‰ฏ aโ‰ฅb)

โ‰ค-refl : โˆ€ {a} โ†’ a โ‰ค a
โ‰ค-refl = inr refl

โ‰ค-trans : {a b c : Cnf} โ†’ a โ‰ค b โ†’ b โ‰ค c โ†’ a โ‰ค c
โ‰ค-trans (inl a<b) (inl b<c) = inl (<-trans a<b b<c)
โ‰ค-trans (inl a<b) (inr cโ‰กb) = inl (subst (_ <_) (sym cโ‰กb) a<b)
โ‰ค-trans (inr bโ‰กa) (inl b<c) = inl (subst (_< _) bโ‰กa b<c)
โ‰ค-trans (inr bโ‰กa) (inr cโ‰กb) = inr (cโ‰กb โˆ™ bโ‰กa)

โ‰ค-antisym : {a b : Cnf} โ†’ a โ‰ค b โ†’ b โ‰ค a โ†’ a โ‰ก b
โ‰ค-antisym (inl a<b) (inl a>b) = โŠฅ-rec (<โ†’โ‰ฏ a<b a>b)
โ‰ค-antisym (inl a<b) (inr aโ‰กb) = โŠฅ-rec (<-irreflexive aโ‰กb a<b)
โ‰ค-antisym (inr bโ‰กa) (inl a>b) = โŠฅ-rec (<-irreflexive bโ‰กa a>b)
โ‰ค-antisym (inr bโ‰กa) (inr aโ‰กb) = aโ‰กb

<-in-โ‰ค : {a b : Cnf} โ†’ a < b โ†’ a โ‰ค b
<-in-โ‰ค = inl

<โˆ˜โ‰ค-in-< : {a b c : Cnf} โ†’ a < b โ†’ b โ‰ค c โ†’ a < c
<โˆ˜โ‰ค-in-< a<b (inl b<c) = <-trans a<b b<c
<โˆ˜โ‰ค-in-< a<b (inr cโ‰กb) = subst (_ <_) (sym cโ‰กb) a<b

โ‰คโˆ˜<-in-< : {a b c : Cnf} โ†’ a โ‰ค b โ†’ b < c โ†’ a < c
โ‰คโˆ˜<-in-< (inl a<b) b<c = <-trans a<b b<c
โ‰คโˆ˜<-in-< (inr bโ‰กa) b<c = subst (_< _) bโ‰กa b<c


{- Convert paths to propositional equality to help Agda's termination checker. -}
import Agda.Builtin.Equality as P

PropEqfromPath : โˆ€ {โ„“} {A : Set โ„“} {x y : A} โ†’ x โ‰ก y โ†’ x P.โ‰ก y
PropEqfromPath {x = x} p = subst (x P.โ‰ก_) p P.refl

mutual

 Cnf-is-discrete : Discrete Cnf
 Cnf-is-discrete  ๐ŸŽ                ๐ŸŽ               = yes refl
 Cnf-is-discrete  ๐ŸŽ               (ฯ‰^ b + d [ s ]) = no ๐ŸŽโ‰ขฯ‰
 Cnf-is-discrete (ฯ‰^ a + c [ r ])  ๐ŸŽ               = no ฯ‰โ‰ข๐ŸŽ
 Cnf-is-discrete (ฯ‰^ a + c [ r ]) (ฯ‰^ b + d [ s ])
     with Cnf-is-discrete a b with Cnf-is-discrete c d
 {---- Pattern match on c, to please Agda's termination checker ----}
 Cnf-is-discrete (ฯ‰^ a + ๐ŸŽ [ r ]) (ฯ‰^ b + d [ s ]) | yes aโ‰กb | yes ๐ŸŽโ‰กd
     with PropEqfromPath aโ‰กb | PropEqfromPath ๐ŸŽโ‰กd
 Cnf-is-discrete (ฯ‰^ a + ๐ŸŽ [ r ]) (ฯ‰^ b + d [ s ]) | yes aโ‰กb | yes ๐ŸŽโ‰กd
     | P.refl | P.refl = yes (cong (ฯ‰^ a + ๐ŸŽ [_]) (isPropโŸจโ‰คโŸฉ r s))
 Cnf-is-discrete (ฯ‰^ a + c@(ฯ‰^ _ + _ [ _ ]) [ r ]) (ฯ‰^ b + d [ s ]) | yes aโ‰กb | yes cโ‰กd
     with PropEqfromPath aโ‰กb | PropEqfromPath cโ‰กd
 Cnf-is-discrete (ฯ‰^ a + c@(ฯ‰^ _ + _ [ _ ]) [ r ]) (ฯ‰^ b + d [ s ]) | yes aโ‰กb | yes cโ‰กd
     | P.refl | P.refl = yes (cong (ฯ‰^ a + c [_]) (isPropโŸจโ‰คโŸฉ r s))
 {---------------- End of the pattern matching on c ----------------}
 Cnf-is-discrete (ฯ‰^ a + c [ r ]) (ฯ‰^ b + d [ s ]) | yes aโ‰กb | no cโ‰ขd =
   no (ฮป e โ†’ cโ‰ขd (cong right e))
 Cnf-is-discrete (ฯ‰^ a + c [ r ]) (ฯ‰^ b + d [ s ]) | no aโ‰ขb | v =
   no (ฮป e โ†’ aโ‰ขb (cong left e))

 {----- Inlining the proof of "Discreteโ†’isSet Cnf-is-discrete" -----}
 โ‰ก-normalise : โˆ€ {a b} โ†’ a โ‰ก b โ†’ a โ‰ก b
 โ‰ก-normalise {a} {b} aโ‰กb with Cnf-is-discrete a b
 ... | yes p = p
 ... | no ยฌp = โŠฅ-rec (ยฌp aโ‰กb)

 โ‰ก-normalise-constant : โˆ€ {a b} (p q : a โ‰ก b) โ†’ โ‰ก-normalise p โ‰ก โ‰ก-normalise q
 โ‰ก-normalise-constant {a} {b} p q with Cnf-is-discrete a b
 ... | yes _ = refl
 ... | no ยฌp = โŠฅ-rec (ยฌp p)

 โ‰ก-canonical : โˆ€ {a b} (p : a โ‰ก b)
            โ†’ (sym (โ‰ก-normalise refl)) โˆ™ (โ‰ก-normalise p) โ‰ก p
 โ‰ก-canonical = J (ฮป y p โ†’ sym (โ‰ก-normalise refl) โˆ™ (โ‰ก-normalise p) โ‰ก p)
                (lCancel (โ‰ก-normalise refl))

 Cnf-is-set : isSet Cnf
 Cnf-is-set _ _ p q = (sym (โ‰ก-canonical p)) โˆ™
  cong (sym (โ‰ก-normalise refl) โˆ™_) (โ‰ก-normalise-constant p q) โˆ™
  โ‰ก-canonical q
 {---------  Cnf-is-set = Discreteโ†’isSet Cnf-is-discrete  ----------}
 {---------------------- End of the inlining -----------------------}

 isPropโŸจ<โŸฉ : โˆ€ {a b} โ†’ isProp (a < b)
 isPropโŸจ<โŸฉ  <โ‚       <โ‚      = refl
 isPropโŸจ<โŸฉ (<โ‚‚ r)   (<โ‚‚ s)   = cong <โ‚‚ (isPropโŸจ<โŸฉ r s)
 isPropโŸจ<โŸฉ (<โ‚‚ r)   (<โ‚ƒ q s) = โŠฅ-rec (<-irreflexive q r)
 isPropโŸจ<โŸฉ (<โ‚ƒ p r) (<โ‚‚ s)   = โŠฅ-rec (<-irreflexive p s)
 isPropโŸจ<โŸฉ (<โ‚ƒ p r) (<โ‚ƒ q s) = congโ‚‚ <โ‚ƒ (Cnf-is-set _ _ p q) (isPropโŸจ<โŸฉ r s)

 isPropโŸจโ‰คโŸฉ : โˆ€ {a b} โ†’ isProp (a โ‰ค b)
 isPropโŸจโ‰คโŸฉ (inl r) (inl s) = cong inl (isPropโŸจ<โŸฉ r s)
 isPropโŸจโ‰คโŸฉ (inl r) (inr q) = โŠฅ-rec (<-irreflexive (sym q) r)
 isPropโŸจโ‰คโŸฉ (inr p) (inl s) = โŠฅ-rec (<-irreflexive (sym p) s)
 isPropโŸจโ‰คโŸฉ (inr p) (inr q) = cong inr (Cnf-is-set _ _ p q)

Cnfโผ : โˆ€ {a b c d r s} โ†’ a โ‰ก c โ†’ b โ‰ก d โ†’ ฯ‰^ a + b [ r ] โ‰ก ฯ‰^ c + d [ s ]
Cnfโผ {a} {b} {c} {d} {r} {s} aโ‰กc bโ‰กd = claimโ‚ r r' โˆ™ claimโ‚ƒ r' s
 where
  r' : c โ‰ฅ left b
  r' = subst _ aโ‰กc r
  claimโ‚€ : โˆ€ r r' โ†’ ฯ‰^ a + b [ r ] โ‰ก ฯ‰^ a + b [ r' ]
  claimโ‚€ r r' = cong (ฯ‰^ a + b [_]) (isPropโŸจโ‰คโŸฉ r r')
  claimโ‚ : (r : a โ‰ฅ left b) (r' : c โ‰ฅ left b) โ†’ ฯ‰^ a + b [ r ] โ‰ก ฯ‰^ c + b [ r' ]
  claimโ‚ = subst _ aโ‰กc claimโ‚€
  claimโ‚‚ : โˆ€ r' s โ†’ ฯ‰^ c + d [ r' ] โ‰ก ฯ‰^ c + d [ s ]
  claimโ‚‚ r' s = cong (ฯ‰^ c + d [_]) (isPropโŸจโ‰คโŸฉ r' s)
  claimโ‚ƒ : (r' : c โ‰ฅ left b) (s : c โ‰ฅ left d) โ†’ ฯ‰^ c + b [ r' ] โ‰ก ฯ‰^ c + d [ s ]
  claimโ‚ƒ = subst _ (sym bโ‰กd) claimโ‚‚

<-tri : (a b : Cnf) โ†’ (a < b) โŠŽ (a โ‰ฅ b)
<-tri  ๐ŸŽ                ๐ŸŽ               = inr (inr refl)
<-tri  ๐ŸŽ               (ฯ‰^ b + d [ _ ]) = inl <โ‚
<-tri (ฯ‰^ a + c [ _ ])  ๐ŸŽ               = inr (inl <โ‚)
<-tri (ฯ‰^ a + c [ _ ]) (ฯ‰^ b + d [ _ ]) with <-tri a b with <-tri c d
... | inl      a<b  | _             = inl (<โ‚‚ a<b)
... | inr (inl a>b) | _             = inr (inl (<โ‚‚ a>b))
... | inr (inr aโ‰กb) | inl      c<d  = inl (<โ‚ƒ aโ‰กb c<d)
... | inr (inr aโ‰กb) | inr (inl c>d) = inr (inl (<โ‚ƒ (sym aโ‰กb) c>d))
... | inr (inr aโ‰กb) | inr (inr cโ‰กd) = inr (inr (Cnfโผ aโ‰กb cโ‰กd))

โ‰ค-connex : (a b : Cnf) โ†’ (a โ‰ค b) โŠŽ (a โ‰ฅ b)
โ‰ค-connex a b with <-tri a b
... | inl a<b = inl (inl a<b)
... | inr aโ‰ฅb = inr aโ‰ฅb

<-extensional : isExtensional _<_
<-extensional a b h with <-tri a b
... | inl      a<b  = โŠฅ-rec (<-irrefl (snd (h a) a<b))
... | inr (inl a>b) = โŠฅ-rec (<-irrefl (fst (h b) a>b))
... | inr (inr aโ‰กb) = aโ‰กb

โ‰ค-extensional : isExtensional _โ‰ค_
โ‰ค-extensional a b h = โ‰ค-antisym (fst (h a) โ‰ค-refl) (snd (h b) โ‰ค-refl)

โ‰คโ‚‚ : โˆ€ {a b c r s} โ†’ a โ‰ค b โ†’ ฯ‰^ a + c [ r ] โ‰ค ฯ‰^ b + c [ s ]
โ‰คโ‚‚ (inl a<b) = inl (<โ‚‚ a<b)
โ‰คโ‚‚ (inr bโ‰กa) = inr (Cnfโผ bโ‰กa refl)

โ‰คโ‚ƒ : โˆ€ {a b c d r s} โ†’ a โ‰ก b โ†’ c โ‰ค d โ†’ ฯ‰^ a + c [ r ] โ‰ค ฯ‰^ b + d [ s ]
โ‰คโ‚ƒ aโ‰กb (inl c<d) = inl (<โ‚ƒ aโ‰กb c<d)
โ‰คโ‚ƒ aโ‰กb (inr dโ‰กc) = inr (Cnfโผ (sym aโ‰กb) dโ‰กc)

<โ‚ƒโปยน : โˆ€ {a b c d r s} โ†’ a โ‰ก b โ†’ ฯ‰^ a + c [ r ] < ฯ‰^ b + d [ s ] โ†’ c < d
<โ‚ƒโปยน aโ‰กb (<โ‚‚ a<b) = โŠฅ-rec (<-irreflexive aโ‰กb a<b)
<โ‚ƒโปยน aโ‰กb (<โ‚ƒ _ c<d) = c<d

โ‰คโ‚ƒโปยน : โˆ€ {a b c d r s} โ†’ a โ‰ก b โ†’ ฯ‰^ a + c [ r ] โ‰ค ฯ‰^ b + d [ s ] โ†’ c โ‰ค d
โ‰คโ‚ƒโปยน aโ‰กb (inl r) = inl (<โ‚ƒโปยน aโ‰กb r)
โ‰คโ‚ƒโปยน aโ‰กb (inr e) = inr (cong right e)

โ‰ฎโ†’โ‰ฅ : {a b : Cnf} โ†’ ยฌ (a < b) โ†’ a โ‰ฅ b
โ‰ฎโ†’โ‰ฅ {a} {b} ยฌa<b with <-tri a b
... | inl a<b = โŠฅ-rec (ยฌa<b a<b)
... | inr aโ‰ฅb = aโ‰ฅb

โ‰ฐโ†’> : {a b : Cnf} โ†’ ยฌ (a โ‰ค b) โ†’ a > b
โ‰ฐโ†’> {a} {b} ยฌaโ‰คb with <-tri b a
... | inl a>b = a>b
... | inr aโ‰คb = โŠฅ-rec (ยฌaโ‰คb aโ‰คb)


{- Exponentiation with base ฯ‰ -}

ฯ‰^โŸจ_โŸฉ : Cnf โ†’ Cnf
ฯ‰^โŸจ a โŸฉ = ฯ‰^ a + ๐ŸŽ [ ๐ŸŽโ‰ค ]

๐Ÿ : Cnf
๐Ÿ = ฯ‰^โŸจ ๐ŸŽ โŸฉ

ฯ‰ : Cnf
ฯ‰ = ฯ‰^โŸจ ๐Ÿ โŸฉ

๐Ÿโ‰คฯ‰^ : โˆ€ {a b r} โ†’ ๐Ÿ โ‰ค ฯ‰^ a + b [ r ]
๐Ÿโ‰คฯ‰^ {๐ŸŽ} = โ‰คโ‚ƒ refl ๐ŸŽโ‰ค
๐Ÿโ‰คฯ‰^ {ฯ‰^ a + c [ s ]} = inl (<โ‚‚ <โ‚)

ฯ‰^โ‰ฎ๐Ÿ : โˆ€ {a b r} โ†’ ยฌ (ฯ‰^ a + b [ r ] < ๐Ÿ)
ฯ‰^โ‰ฎ๐Ÿ = โ‰คโ†’โ‰ฏ ๐Ÿโ‰คฯ‰^

<๐Ÿโ†’โ‰ก๐ŸŽ : โˆ€ {a} โ†’ a < ๐Ÿ โ†’ a โ‰ก ๐ŸŽ
<๐Ÿโ†’โ‰ก๐ŸŽ <โ‚ = refl


{- Embedding natural numbers into CNF -}
mutual

 NtoC : โ„• โ†’ Cnf
 NtoC  0      = ๐ŸŽ
 NtoC (suc n) = ฯ‰^ ๐ŸŽ + NtoC n [ inr (sym (left-NtoC-is-๐ŸŽ n)) ]

 left-NtoC-is-๐ŸŽ : โˆ€ n โ†’ left (NtoC n) โ‰ก ๐ŸŽ
 left-NtoC-is-๐ŸŽ  0      = refl
 left-NtoC-is-๐ŸŽ (suc n) = refl

leftโ‰ก๐ŸŽ-is-nat : โˆ€ a โ†’ left a โ‰ก ๐ŸŽ โ†’ ฮฃ[ n โˆˆ โ„• ] a โ‰ก NtoC n
leftโ‰ก๐ŸŽ-is-nat ๐ŸŽ e = 0 , refl
leftโ‰ก๐ŸŽ-is-nat (ฯ‰^ a + b [ r ]) aโ‰ก๐ŸŽ = suc n , claim
 where
  lbโ‰ก๐ŸŽ : left b โ‰ก ๐ŸŽ
  lbโ‰ก๐ŸŽ = โ‰ค๐ŸŽโ†’โ‰ก๐ŸŽ (subst (left b โ‰ค_) aโ‰ก๐ŸŽ r)
  IH : ฮฃ[ n โˆˆ โ„• ] b โ‰ก NtoC n
  IH = leftโ‰ก๐ŸŽ-is-nat b lbโ‰ก๐ŸŽ
  n : โ„•
  n = fst IH
  claim : ฯ‰^ a + b [ r ] โ‰ก NtoC (suc n)
  claim = Cnfโผ aโ‰ก๐ŸŽ (snd IH)