Todd Waugh Ambridge, 27th April 2020.

We formalize, in univalent mathematics in Agda, some definitions in

M.H. Escardo and A. Simpson. A universal characterization of the
closed Euclidean interval (extended abstract). Proceedings of the 16th
Annual IEEE Symposium on Logic in Computer Science,
pp.115--125. Boston, Massachusetts, June 16-19, 2001.

https://www.cs.bham.ac.uk/~mhe/papers/lics2001-revised.pdf
https://www.cs.bham.ac.uk/~mhe/papers/interval.pdf
https://www.cs.bham.ac.uk/~mhe/.talks/map2011/

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import UF.FunExt

module TWA.Escardo-Simpson-LICS2001 (fe : FunExt) where

open import MLTT.Spartan
open import Naturals.Addition renaming (_+_ to _+β„•_)
open import Naturals.Sequence fe
open import UF.Sets
open import UF.Subsingletons public

\end{code}

First we give basic properties on binary functions,
as well as a specific property about equality of streams under some arithmetic.

\begin{code}

idempotent transpositional : {X : 𝓀 Μ‡ } β†’ (X β†’ X β†’ X) β†’ 𝓀 Μ‡
idempotent       _βˆ™_ = βˆ€ a       β†’ a βˆ™ a             ＝ a
transpositional  _βˆ™_ = βˆ€ a b c d β†’ (a βˆ™ b) βˆ™ (c βˆ™ d) ＝ (a βˆ™ c) βˆ™ (b βˆ™ d)

seq-add-push : {A : 𝓀 Μ‡ } (Ξ± : β„• β†’ A) (n : β„•)
             β†’ (Ξ» (i : β„•) β†’ Ξ± (succ i +β„• n)) ＝ (Ξ» (i : β„•) β†’ Ξ± (succ (i +β„• n)))
seq-add-push Ξ± 0 = refl
seq-add-push α (succ n) = seq-add-push (α ∘ succ) n

\end{code}

The initial structure we define is a Midpoint-algebra.

\begin{code}

midpoint-algebra-axioms : (A : 𝓀 Μ‡ ) β†’ (A β†’ A β†’ A) β†’ 𝓀 Μ‡
midpoint-algebra-axioms {𝓀} A _βŠ•_ = is-set A
                                  Γ— idempotent _βŠ•_ Γ— commutative _βŠ•_ Γ— transpositional _βŠ•_

Midpoint-algebra : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
Midpoint-algebra 𝓀 = Ξ£ A κž‰ 𝓀 Μ‡ , Ξ£ _βŠ•_ κž‰ (A β†’ A β†’ A) , (midpoint-algebra-axioms A _βŠ•_)

\end{code}

 We introduce two more properties on binary functions: cancellation and iteration.
 For a particular type, the iterator is unique.

\begin{code}

cancellative : {X : 𝓀 Μ‡ } β†’ (X β†’ X β†’ X) β†’ 𝓀 Μ‡
cancellative  _βˆ™_ = βˆ€ a b c β†’ a βˆ™ c ＝ b βˆ™ c β†’ a ＝ b

iterative : {A : 𝓀 Μ‡ } β†’ (A β†’ A β†’ A) β†’ 𝓀 Μ‡
iterative {𝓀} {A} _βŠ•_ = Ξ£ M κž‰ ((β„• β†’ A) β†’ A) , ((a : β„• β†’ A) β†’ M a ＝ a 0 βŠ• M (tail a))
                                            Γ— ((a x : β„• β†’ A)
                                               β†’ ((i : β„•) β†’ a i ＝ x i βŠ• a (succ i))
                                               β†’ a 0 ＝ M x)

iterative-uniquenessΒ· : {A : 𝓀 Μ‡ } β†’ (_βŠ•_ : A β†’ A β†’ A)
                      β†’ (F M : iterative _βŠ•_)
                      β†’ pr₁ F ∼ pr₁ M
iterative-uniquenessΒ· {𝓀} {𝕀} _βŠ•_ (F , p₁ , q₁) (M , pβ‚‚ , qβ‚‚) x = qβ‚‚ M' x Ξ³
  where M' : β„• β†’ 𝕀
        M' i = F (Ξ» n β†’ x (n +β„• i))
        Ξ³ : (i : β„•) β†’ M' i ＝ (x i βŠ• M' (succ i))
        Ξ³ i = p₁ (Ξ» n β†’ x (n +β„• i))
            βˆ™ ap (Ξ» - β†’ x - βŠ• F (Ξ» n β†’ x (succ n +β„• i))) (zero-left-neutral i)
            βˆ™ ap (Ξ» - β†’ x i βŠ• F -) (seq-add-push x i)

iterative-uniqueness : {A : 𝓀 Μ‡ } β†’ (_βŠ•_ : A β†’ A β†’ A)
                     β†’ (F M : iterative _βŠ•_)
                     β†’ pr₁ F ＝ pr₁ M
iterative-uniqueness {𝓀} _βŠ•_ F M = dfunext (fe 𝓀 𝓀) (iterative-uniquenessΒ· _βŠ•_ F M)

\end{code}

 A Convex-body is a cancellative, iterative Midpoint-algebra.

\begin{code}

convex-body-axioms : (A : 𝓀 Μ‡ ) β†’ (A β†’ A β†’ A) β†’ 𝓀 Μ‡
convex-body-axioms {𝓀} A _βŠ•_ = (midpoint-algebra-axioms A _βŠ•_)
                             Γ— (cancellative _βŠ•_)
                             Γ— (iterative _βŠ•_)

Convex-body : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
Convex-body 𝓀 = Ξ£ A κž‰ 𝓀 Μ‡ , Ξ£ _βŠ•_ κž‰ (A β†’ A β†’ A) , (convex-body-axioms A _βŠ•_)

⟨_⟩ : Convex-body 𝓀 β†’ 𝓀 Μ‡
⟨ A , _ ⟩ = A

midpoint-operation : (𝓐 : Convex-body 𝓀) β†’ ⟨ 𝓐 ⟩ β†’ ⟨ 𝓐 ⟩ β†’ ⟨ 𝓐 ⟩
midpoint-operation (A , _βŠ•_ , _) = _βŠ•_

syntax midpoint-operation 𝓐 x y = x βŠ•βŸ¨ 𝓐 ⟩ y

\end{code}

 Definition of a midpoint-homomorphism.
 The identity function is a midpoint-hom.
 The unary functions given by a constant midpoint are midpoint-homs.
 The composition of two midpoint-homs is a midpoint-hom.

\begin{code}

is-βŠ•-homomorphism : (𝓐 : Convex-body 𝓀) (𝓑 : Convex-body π“₯)
                β†’ (⟨ 𝓐 ⟩ β†’ ⟨ 𝓑 ⟩) β†’ 𝓀 βŠ” π“₯ Μ‡
is-βŠ•-homomorphism 𝓐 𝓑 h = (x y : ⟨ 𝓐 ⟩) β†’ h (x βŠ•βŸ¨ 𝓐 ⟩ y) ＝ h x βŠ•βŸ¨ 𝓑 ⟩ h y

id-is-βŠ•-homomorphism : (𝓐 : Convex-body 𝓀) β†’ is-βŠ•-homomorphism 𝓐 𝓐 id
id-is-βŠ•-homomorphism 𝓐 x y = refl

βŠ•-is-βŠ•-homomorphism-r : (𝓐 : Convex-body 𝓀)
                    β†’ (a : ⟨ 𝓐 ⟩) β†’ is-βŠ•-homomorphism 𝓐 𝓐 (Ξ» y β†’ a βŠ•βŸ¨ 𝓐 ⟩ y)
βŠ•-is-βŠ•-homomorphism-r (𝓐 , _βŠ•_ , (_ , βŠ•-idem , _ , βŠ•-tran) , _) a x y
 =    a    βŠ• (x βŠ• y) ＝⟨ ap (_βŠ• (x βŠ• y)) (βŠ•-idem a ⁻¹) ⟩
   (a βŠ• a) βŠ• (x βŠ• y) ＝⟨ βŠ•-tran a a x y ⟩
   (a βŠ• x) βŠ• (a βŠ• y) ∎

βŠ•-is-βŠ•-homomorphism-l : (𝓐 : Convex-body 𝓀)
                    β†’ (b : ⟨ 𝓐 ⟩) β†’ is-βŠ•-homomorphism 𝓐 𝓐 (Ξ» x β†’ x βŠ•βŸ¨ 𝓐 ⟩ b)
βŠ•-is-βŠ•-homomorphism-l (𝓐 , _βŠ•_ , (_ , βŠ•-idem , _ , βŠ•-tran) , _) b x y
 = (x βŠ• y) βŠ•    b    ＝⟨ ap ((x βŠ• y) βŠ•_) (βŠ•-idem b ⁻¹) ⟩
   (x βŠ• y) βŠ• (b βŠ• b) ＝⟨ βŠ•-tran x y b b ⟩
   (x βŠ• b) βŠ• (y βŠ• b) ∎

βŠ•-hom-composition : (𝓐 : Convex-body 𝓀) (𝓑 : Convex-body π“₯) (𝓒 : Convex-body 𝓦)
                          β†’ (h₁ : ⟨ 𝓐 ⟩ β†’ ⟨ 𝓑 ⟩) β†’ (hβ‚‚ : ⟨ 𝓑 ⟩ β†’ ⟨ 𝓒 ⟩)
                          β†’ is-βŠ•-homomorphism 𝓐 𝓑 h₁ β†’ is-βŠ•-homomorphism 𝓑 𝓒 hβ‚‚
                          β†’ is-βŠ•-homomorphism 𝓐 𝓒 (hβ‚‚ ∘ h₁)
βŠ•-hom-composition {𝓀} {π“₯} {𝓦} 𝓐 𝓑 𝓒 h₁ hβ‚‚ i₁ iβ‚‚ x y
 = (hβ‚‚ ∘ h₁) (x βŠ•βŸ¨ 𝓐 ⟩ y)                       ＝⟨ ap hβ‚‚ (i₁ x y) ⟩
         hβ‚‚  ((h₁ x) βŠ•βŸ¨ 𝓑 ⟩ (h₁ y))             ＝⟨ iβ‚‚ (h₁ x) (h₁ y) ⟩
             ((hβ‚‚ ∘ h₁) x) βŠ•βŸ¨ 𝓒 ⟩ ((hβ‚‚ ∘ h₁) y) ∎

\end{code}

 The key structure of the axiomatisation: an interval object.
 An interval object is defined by a Convex-body π“˜ and two points u,v : βŸ¨π“˜βŸ©.
 For every two points a,b : βŸ¨π“βŸ© of a Convex-body 𝓐,
   there exists a unique h : βŸ¨π“˜βŸ© β†’ βŸ¨π“βŸ© such that:
    * h u ＝ a,
    * h v ＝ b,
    * βˆ€ x,y : βŸ¨π“˜βŸ©. h (x βŠ•βŸ¨ π“˜ ⟩ y) ＝ h x βŠ•βŸ¨ 𝓐 ⟩ h y).

\begin{code}

is-interval-object : (π“˜ : Convex-body 𝓀) (π“₯ : Universe) β†’ ⟨ π“˜ ⟩ β†’ ⟨ π“˜ ⟩ β†’ 𝓀 βŠ” π“₯ ⁺ Μ‡
is-interval-object π“˜ π“₯ u v =
    (𝓐 : Convex-body π“₯) (a b : ⟨ 𝓐 ⟩) -- h = affine a b
   β†’ βˆƒ! h κž‰ (⟨ π“˜ ⟩ β†’ ⟨ 𝓐 ⟩) , (h u ＝ a)
                            Γ— (h v ＝ b)
                            Γ— ((x y : ⟨ π“˜ ⟩) β†’ h (x βŠ•βŸ¨ π“˜ ⟩ y) ＝ h x βŠ•βŸ¨ 𝓐 ⟩ h y)

\end{code}

 The type of an interval object axiomatisation as a record.

\begin{code}

record Interval-object (𝓀 : Universe) : 𝓀ω where
 field
  𝕀 : 𝓀 Μ‡
  _βŠ•_ : 𝕀 β†’ 𝕀 β†’ 𝕀
  u v : 𝕀
  mpaa : midpoint-algebra-axioms 𝕀 _βŠ•_
  ca : cancellative _βŠ•_
  ia : iterative _βŠ•_
  universal-property : is-interval-object (𝕀 , _βŠ•_ , mpaa , ca , ia) 𝓀 u v

\end{code}

 The type of a doubling function axiomatisation.

\begin{code}

has-double : (π“₯ : Universe) (io : Interval-object π“₯) β†’ π“₯ Μ‡
has-double π“₯ io = Ξ£ double κž‰ (𝕀 β†’ 𝕀)
                 , ((x : 𝕀) β†’ double (x βŠ• (u βŠ• v)) ＝ x)
                 Γ— ((x : 𝕀) β†’ double (u βŠ• (u βŠ• x)) ＝ u)
                 Γ— ((x : 𝕀) β†’ double (v βŠ• (v βŠ• x)) ＝ v)
 where
   𝕀 = Interval-object.𝕀 io
   u = Interval-object.u io
   v = Interval-object.v io
   _βŠ•_ = Interval-object._βŠ•_ io

\end{code}

 We now prove things within a universe
 with an Interval-object and a doubling function.

\begin{code}

module basic-interval-object-development {𝓀 : Universe}
 (io : Interval-object 𝓀) (hd : has-double 𝓀 io) where

\end{code}

 First we unpack all of the axioms from the Interval-object
 affine : 𝕀 β†’ 𝕀 β†’ 𝕀 β†’ 𝕀 is given by the unique map h : 𝕀 β†’ 𝕀.

\begin{code}


 open Interval-object io public

 βŠ•-idem : idempotent _βŠ•_
 βŠ•-idem = pr₁ (prβ‚‚ mpaa)

 βŠ•-comm : commutative _βŠ•_
 βŠ•-comm = pr₁ (prβ‚‚ (prβ‚‚ mpaa))

 βŠ•-tran : transpositional _βŠ•_
 βŠ•-tran = prβ‚‚ (prβ‚‚ (prβ‚‚ mpaa))

 βŠ•-canc : cancellative _βŠ•_
 βŠ•-canc = Interval-object.ca io

 π“˜ : Convex-body 𝓀
 π“˜ = 𝕀 , _βŠ•_ , mpaa , βŠ•-canc , ia

 affine : 𝕀 β†’ 𝕀 β†’ 𝕀 β†’ 𝕀
 affine x y = βˆƒ!-witness (universal-property π“˜ x y)

 affine-equation-l : (x y : 𝕀) β†’ affine x y u ＝ x
 affine-equation-l x y = pr₁ (βˆƒ!-is-witness (universal-property π“˜ x y))

 affine-equation-r : (x y : 𝕀) β†’ affine x y v ＝ y
 affine-equation-r x y = pr₁ (prβ‚‚ (βˆƒ!-is-witness (universal-property π“˜ x y)))

 affine-is-βŠ•-homomorphism : (x y : 𝕀) (a b : 𝕀)
                        β†’ affine x y (a βŠ• b) ＝ affine x y a βŠ• affine x y b
 affine-is-βŠ•-homomorphism x y = prβ‚‚ (prβ‚‚ (βˆƒ!-is-witness (universal-property π“˜ x y)))

 affine-uniqueness : (f : 𝕀 β†’ 𝕀) (a b : 𝕀)
                   β†’ f u ＝ a
                   β†’ f v ＝ b
                   β†’ is-βŠ•-homomorphism π“˜ π“˜ f
                   β†’ affine a b ＝ f
 affine-uniqueness f a b l r i
  = ap pr₁ (βˆƒ!-uniqueness' (universal-property π“˜ a b) (f , l , r , i))

 affine-uniquenessΒ· : (f : 𝕀 β†’ 𝕀) (a b : 𝕀)
                   β†’ f u ＝ a
                   β†’ f v ＝ b
                   β†’ is-βŠ•-homomorphism π“˜ π“˜ f
                   β†’ affine a b ∼ f
 affine-uniquenessΒ· f a b l r i x = ap (Ξ» - β†’ - x) (affine-uniqueness f a b l r i)

\end{code}

 Many of the following proofs follow from the uniqueness of affine.
 For example, affine u v is point-wise equivalent to the identity function.

\begin{code}

 affine-uv-involutive : affine u v ∼ id
 affine-uv-involutive = affine-uniquenessΒ· id u v refl refl (id-is-βŠ•-homomorphism π“˜)

 affine-constant : (a : 𝕀) (x : 𝕀) β†’ affine a a x ＝ a
 affine-constant a = affine-uniquenessΒ· (Ξ» _ β†’ a) a a refl refl (Ξ» _ _ β†’ βŠ•-idem a ⁻¹)

\end{code}

 The iterator is called M.
 We prove that it is idempotent, symmetric and is a midpoint-hom.

\begin{code}

 M : (β„• β†’ 𝕀) β†’ 𝕀
 M = pr₁ ia

 M-prop₁ : (a : β„• β†’ 𝕀) β†’ M a ＝ a 0 βŠ• (M (a ∘ succ))
 M-prop₁ = pr₁ (prβ‚‚ ia)

 M-propβ‚‚ : (a x : β„• β†’ 𝕀) β†’ ((i : β„•) β†’ a i ＝ x i βŠ• a (succ i)) β†’ a 0 ＝ M x
 M-propβ‚‚ = prβ‚‚ (prβ‚‚ ia)

 M-idem : (x : 𝕀) β†’ M (Ξ» _ β†’ x) ＝ x
 M-idem x = M-propβ‚‚ (Ξ» _ β†’ x) (Ξ» _ β†’ x) (Ξ» _ β†’ βŠ•-idem x ⁻¹) ⁻¹

 M-hom : (x y : β„• β†’ 𝕀) β†’ (M x βŠ• M y) ＝ M (Ξ» i β†’ x i βŠ• y i)
 M-hom x y = M-propβ‚‚ M' (Ξ» i β†’ x i βŠ• y i) Ξ³ where
   M' : β„• β†’ 𝕀
   M' i = M (Ξ» n β†’ x (n +β„• i)) βŠ• M (Ξ» n β†’ y (n +β„• i))
   Ξ³ : (i : β„•) β†’ M' i ＝ ((x i βŠ• y i) βŠ• M' (succ i))
   Ξ³ i = M (Ξ» n β†’ x (n +β„• i)) βŠ• M (Ξ» n β†’ y (n +β„• i))
             ＝⟨ ap (_βŠ• M (Ξ» n β†’ y (n +β„• i)))
                   (M-prop₁ (Ξ» n β†’ x (n +β„• i))) ⟩
         (x (0 +β„• i) βŠ• M (Ξ» n β†’ x (succ n +β„• i))) βŠ• M (Ξ» n β†’ y (n +β„• i))
             ＝⟨ ap ((x (0 +β„• i) βŠ• M (Ξ» n β†’ x (succ n +β„• i))) βŠ•_)
                   (M-prop₁ (Ξ» n β†’ y (n +β„• i))) ⟩
         (x (0 +β„• i) βŠ• M (Ξ» n β†’ x (succ n +β„• i))) βŠ• (y (0 +β„• i) βŠ• M (Ξ» n β†’ y (succ n +β„• i)))
             ＝⟨ βŠ•-tran
                   (x (0 +β„• i)) (M (Ξ» n β†’ x (succ n +β„• i)))
                   (y (0 +β„• i)) (M (Ξ» n β†’ y (succ n +β„• i))) ⟩
         ((x (0 +β„• i) βŠ• y (0 +β„• i)) βŠ• (M (Ξ» n β†’ x (succ n +β„• i)) βŠ• M (Ξ» n β†’ y (succ n +β„• i))))
             ＝⟨ ap (Ξ» - β†’ (x - βŠ• y -)
                        βŠ• (M (Ξ» n β†’ x (succ n +β„• i)) βŠ• M (Ξ» n β†’ y (succ n +β„• i))))
                   (zero-left-neutral i) ⟩
         ((x i βŠ• y i) βŠ• (M (Ξ» n β†’ x (succ n +β„• i)) βŠ• M (Ξ» n β†’ y (succ n +β„• i))))
             ＝⟨ ap (Ξ» - β†’ (x i βŠ• y i) βŠ• (M - βŠ• M (Ξ» n β†’ y (succ n +β„• i))))
                   (seq-add-push x i) ⟩
         ((x i βŠ• y i) βŠ• (M (Ξ» n β†’ x (succ (n +β„• i))) βŠ• M (Ξ» n β†’ y (succ n +β„• i))))
             ＝⟨ ap (Ξ» - β†’ (x i βŠ• y i) βŠ• (M (Ξ» n β†’ x (succ (n +β„• i))) βŠ• M -))
                   (seq-add-push y i) ⟩
         (x i βŠ• y i) βŠ• M' (succ i) ∎

 M-prop₁-inner : (x : β„• β†’ β„• β†’ 𝕀) β†’ M (Ξ» i β†’ M (Ξ» j β†’ x i j))
                                 ＝ M (Ξ» i β†’ x i 0 βŠ• M (Ξ» j β†’ x i (succ j)))
 M-prop₁-inner x = ap M (dfunext (fe 𝓀₀ 𝓀) (Ξ» i β†’ M-prop₁ (x i)))

 M-symm : (x : β„• β†’ β„• β†’ 𝕀) β†’ M (Ξ» i β†’ M (Ξ» j β†’ x i j)) ＝ M (Ξ» i β†’ (M Ξ» j β†’ x j i))
 M-symm x = M-propβ‚‚ M' (Ξ» i β†’ M (Ξ» j β†’ x j i)) Ξ³ where
   M' : β„• β†’ 𝕀
   M' n = M (Ξ» i β†’ M (Ξ» j β†’ x i (j +β„• n)))
   Ξ³ : (i : β„•) β†’ M' i ＝ (pr₁ ia (Ξ» j β†’ x j i) βŠ• M' (succ i))
   Ξ³ n = M (Ξ» i β†’ M (Ξ» j β†’ x i (j +β„• n)))
             ＝⟨ M-prop₁-inner (Ξ» i j β†’ x i (j +β„• n)) ⟩
         M (Ξ» i β†’ x i (0 +β„• n) βŠ• M (Ξ» j β†’ x i (succ j +β„• n)))
             ＝⟨ M-hom (Ξ» i β†’ x i (0 +β„• n))
                      (Ξ» i β†’ M (Ξ» j β†’ x i (succ j +β„• n))) ⁻¹ ⟩
         M (Ξ» i β†’ x i (0 +β„• n)) βŠ• M (Ξ» i β†’ M (Ξ» j β†’ x i (succ j +β„• n)))
             ＝⟨ ap (Ξ» - β†’ M (Ξ» i β†’ x i -)
                    βŠ• M (Ξ» i β†’ M (Ξ» j β†’ x i (succ j +β„• n))))
                   (zero-left-neutral n) ⟩
         M (Ξ» i β†’ x i n) βŠ• M (Ξ» i β†’ M (Ξ» j β†’ x i (succ j +β„• n)))
             ＝⟨ ap (M (Ξ» j β†’ x j n) βŠ•_) (seq-seq-add-push x n) ⟩
         M (Ξ» j β†’ x j n) βŠ• M' (succ n) ∎
     where
       seq-seq-add-push : (x : β„• β†’ β„• β†’ 𝕀) (n : β„•)
                        β†’ M (Ξ» i β†’ M (Ξ» j β†’ x i (succ j +β„• n)))
                        ＝ M (Ξ» i β†’ M (Ξ» j β†’ x i (succ (j +β„• n))))
       seq-seq-add-push x 0 = refl
       seq-seq-add-push x (succ n) = seq-seq-add-push (Ξ» i j β†’ x i (succ j)) n

\end{code}

 Any midpoint-hom is automatically an M-hom.
 Thus, M is an M-hom.

\begin{code}

 βŠ•-homs-are-M-homs : (h : 𝕀 β†’ 𝕀) β†’ is-βŠ•-homomorphism π“˜ π“˜ h
           β†’ (z : β„• β†’ 𝕀) β†’ h (M z) ＝ M (Ξ» n β†’ h (z n))
 βŠ•-homs-are-M-homs h hom z = M-propβ‚‚ M' (Ξ» n β†’ h (z n)) Ξ³ where
   M' : β„• β†’ 𝕀
   M' i = h (M (Ξ» n β†’ z (n +β„• i)))
   Ξ³ : (i : β„•) β†’ M' i ＝ (h (z i) βŠ• M' (succ i))
   Ξ³ i = h (M (Ξ» n β†’ z (n +β„• i)))
            ＝⟨ ap h (M-prop₁ (Ξ» n β†’ z (n +β„• i))) ⟩
         h (z (0 +β„• i) βŠ• M (Ξ» n β†’ z (succ n +β„• i)))
            ＝⟨ hom (z (0 +β„• i)) (M (Ξ» n β†’ z (succ n +β„• i))) ⟩
         h (z (0 +β„• i)) βŠ• h (M (Ξ» n β†’ z (succ n +β„• i)))
            ＝⟨ ap (Ξ» - β†’ h (z -) βŠ• h (M (Ξ» n β†’ z (succ n +β„• i))))
                  (zero-left-neutral i) ⟩
         h (z i) βŠ• h (M (Ξ» n β†’ z (succ n +β„• i)))
            ＝⟨ ap (Ξ» - β†’ h (z i) βŠ• h (M -))
                  (seq-add-push z i) ⟩
         h (z i) βŠ• M' (succ i)
            ∎

 affine-M-hom : (x y : 𝕀) (z : β„• β†’ 𝕀) β†’ affine x y (M z) ＝ M (Ξ» n β†’ affine x y (z n))
 affine-M-hom x y z = βŠ•-homs-are-M-homs (affine x y) (affine-is-βŠ•-homomorphism x y) z

\end{code}

 We adopt the convention u = βˆ’1 and v = +1 for the following.

\begin{code}

 βˆ’1 O +1 : 𝕀
 βˆ’1 = u
 +1 = v
 O  = βˆ’1 βŠ• +1

\end{code}

 The negation function and related properties,
 culminating in proving negation is involutive.

\begin{code}

 βˆ’_ : 𝕀 β†’ 𝕀
 βˆ’_ = affine +1 βˆ’1

 infixl 100 βˆ’_

 βˆ’-is-βŠ•-homomorphism : (a b : 𝕀) β†’ βˆ’ (a βŠ• b) ＝ βˆ’ a βŠ• βˆ’ b
 βˆ’-is-βŠ•-homomorphism = affine-is-βŠ•-homomorphism +1 βˆ’1

 βˆ’1-inverse : βˆ’ βˆ’1 ＝ +1
 βˆ’1-inverse = affine-equation-l +1 βˆ’1

 +1-inverse : βˆ’ +1 ＝ βˆ’1
 +1-inverse = affine-equation-r +1 βˆ’1

 O-inverse : βˆ’ O ＝ O
 O-inverse =    βˆ’ O      ＝⟨ βˆ’-is-βŠ•-homomorphism βˆ’1 +1 ⟩
             βˆ’ βˆ’1 βŠ• βˆ’ +1 ＝⟨ ap (_βŠ• βˆ’ +1) βˆ’1-inverse ⟩
               +1 βŠ• βˆ’ +1 ＝⟨ ap (+1 βŠ•_)   +1-inverse ⟩
               +1 βŠ• βˆ’1   ＝⟨ βŠ•-comm +1 βˆ’1 ⟩
                  O      ∎

 βˆ’1-neg-inv : βˆ’ βˆ’ βˆ’1 ＝ βˆ’1
 βˆ’1-neg-inv = βˆ’ βˆ’ βˆ’1 ＝⟨ ap βˆ’_ βˆ’1-inverse ⟩
                βˆ’ +1 ＝⟨ +1-inverse ⟩
                  βˆ’1 ∎

 +1-neg-inv : βˆ’ βˆ’ +1 ＝ +1
 +1-neg-inv = βˆ’ βˆ’ +1 ＝⟨ ap βˆ’_ +1-inverse ⟩
                βˆ’ βˆ’1 ＝⟨ βˆ’1-inverse ⟩
                  +1 ∎

 βˆ’-involutive : (x : 𝕀) β†’ βˆ’ βˆ’ x ＝ x
 βˆ’-involutive x =         βˆ’ βˆ’ x ＝⟨ negation-involutive' x ⁻¹ ⟩
                 affine βˆ’1 +1 x ＝⟨ affine-uv-involutive x ⟩
                              x  ∎
  where
   βˆ’βˆ’-is-βŠ•-homomorphism : is-βŠ•-homomorphism π“˜ π“˜ (Ξ» x β†’ βˆ’ (βˆ’ x))
   βˆ’βˆ’-is-βŠ•-homomorphism = βŠ•-hom-composition π“˜ π“˜ π“˜ βˆ’_ βˆ’_
                          βˆ’-is-βŠ•-homomorphism βˆ’-is-βŠ•-homomorphism
   negation-involutive' : (x : 𝕀) β†’ affine βˆ’1 +1 x ＝ βˆ’ (βˆ’ x)
   negation-involutive' = affine-uniquenessΒ· (Ξ» x β†’ βˆ’ (βˆ’ x))
                          βˆ’1 +1 βˆ’1-neg-inv +1-neg-inv
                          βˆ’βˆ’-is-βŠ•-homomorphism

 fact : (x y : 𝕀) β†’ x βŠ• βˆ’ y ＝ βˆ’ (βˆ’ x βŠ• y)
 fact x y =     x βŠ• βˆ’ y ＝⟨ ap (_βŠ• (βˆ’ y)) (βˆ’-involutive x ⁻¹) ⟩
            βˆ’ βˆ’ x βŠ• βˆ’ y ＝⟨ βˆ’-is-βŠ•-homomorphism (βˆ’ x) y ⁻¹ ⟩
            βˆ’ (βˆ’ x βŠ• y) ∎

\end{code}

 The "midpoint subtraction" function from midpoint and negation.
 The midpoint subtraction of any x with itself is O.

\begin{code}

 _βŠ–_ : 𝕀 β†’ 𝕀 β†’ 𝕀
 x βŠ– y = x βŠ• (βˆ’ y)

 βŠ–-zero : (x : 𝕀) β†’ x βŠ– x ＝ O
 βŠ–-zero x = x βŠ– x        ＝⟨ βŠ–-fact' ⁻¹ ⟩
            affine O O x ＝⟨ affine-constant O x ⟩
            O            ∎
   where
    βŠ–-fact' : affine O O x ＝ x βŠ– x
    βŠ–-fact' = affine-uniquenessΒ· (Ξ» x β†’ x βŠ– x) O O
              (ap (βˆ’1 βŠ•_) βˆ’1-inverse)
              (ap (+1 βŠ•_) +1-inverse βˆ™ βŠ•-comm +1 βˆ’1)
              (Ξ» x y β†’ ap ((x βŠ• y) βŠ•_)
                          (βˆ’-is-βŠ•-homomorphism x y)
                     βˆ™ βŠ•-tran x y (βˆ’ x) (βˆ’ y))
              x

\end{code}

 The multiplication function and related properties,
 culminating in proving multiplication is
 commutative and associative'.

\begin{code}

 _*_ : 𝕀 β†’ 𝕀 β†’ 𝕀
 x * y = affine (βˆ’ x) x y

 infixl 99 _*_

 *-gives-negation-l : (x : 𝕀) β†’ x * βˆ’1 ＝ βˆ’ x
 *-gives-negation-l x = affine-equation-l (βˆ’ x) x

 *-gives-negation-r : (y : 𝕀) β†’ βˆ’1 * y ＝ βˆ’ y
 *-gives-negation-r y = ap (Ξ» - β†’ affine - βˆ’1 y) βˆ’1-inverse

 *-gives-id-l : (x : 𝕀) β†’ x * +1 ＝ x
 *-gives-id-l x = affine-equation-r (βˆ’ x) x

 *-gives-id-r : (y : 𝕀) β†’ +1 * y ＝ y
 *-gives-id-r y = ap (Ξ» - β†’ affine - +1 y) +1-inverse βˆ™ affine-uv-involutive y

 *-is-βŠ•-homomorphism-l : (a : 𝕀) β†’ is-βŠ•-homomorphism π“˜ π“˜ (a *_)
 *-is-βŠ•-homomorphism-l a x y = affine-is-βŠ•-homomorphism (βˆ’ a) a x y

 *-commutative : commutative _*_
 *-commutative x y = Ξ³ y
  where
   j : (a b : 𝕀) β†’ is-βŠ•-homomorphism π“˜ π“˜ (Ξ» x β†’ a * x βŠ• b * x)
   j a b x y
       = ap (_βŠ• b * (x βŠ• y)) (*-is-βŠ•-homomorphism-l a x y)
       βˆ™ ap ((a * x βŠ• a * y) βŠ•_) (*-is-βŠ•-homomorphism-l b x y)
       βˆ™ βŠ•-tran (a * x) (a * y) (affine (βˆ’ b) b x) (affine (βˆ’ b) b y)
   i : is-βŠ•-homomorphism π“˜ π“˜ (Ξ» y β†’ y * x)
   i y z = p
    where
     p : (y βŠ• z) * x ＝ (y * x βŠ• z * x)
     p = affine-uniquenessΒ· (Ξ» x β†’ y * x βŠ• z * x) (βˆ’ (y βŠ• z)) (y βŠ• z)
         (ap (_βŠ• z * u) (*-gives-negation-l y)
         βˆ™ ap ((βˆ’ y) βŠ•_) (*-gives-negation-l z)
         βˆ™ affine-is-βŠ•-homomorphism +1 βˆ’1 y z ⁻¹)
         (ap (_βŠ• z * v) (*-gives-id-l y)
         βˆ™ ap (y βŠ•_) (*-gives-id-l z))
         (j y z) x
   Ξ³ : (Ξ» y β†’ x * y) ∼ (Ξ» y β†’ y * x)
   Ξ³ = affine-uniquenessΒ· (Ξ» y β†’ y * x)
       (βˆ’ x) x (*-gives-negation-r x) (*-gives-id-r x)
       i

 *-is-βŠ•-homomorphism-r : (b : 𝕀) β†’ is-βŠ•-homomorphism π“˜ π“˜ (_* b)
 *-is-βŠ•-homomorphism-r b x y =
      (x βŠ• y) * b       ＝⟨ *-commutative (x βŠ• y) b ⟩
      b * (x βŠ• y)       ＝⟨ *-is-βŠ•-homomorphism-l b x y ⟩
      (b * x) βŠ• (b * y) ＝⟨ ap ((b * x) βŠ•_) (*-commutative b y) ⟩
      (b * x) βŠ• (y * b) ＝⟨ ap (_βŠ• (y * b)) (*-commutative b x) ⟩
      (x * b) βŠ• (y * b) ∎

 *-prop : (x y : 𝕀) β†’ x * y ＝ βˆ’ (x * βˆ’ y)
 *-prop x y = affine-uniquenessΒ· (Ξ» - β†’ βˆ’ (x * (βˆ’ -))) (βˆ’ x) x l r i y
  where
   l = βˆ’ (x * (βˆ’ βˆ’1)) ＝⟨ ap (Ξ» - β†’ βˆ’ (x * -)) βˆ’1-inverse ⟩
       βˆ’ (x *    +1 ) ＝⟨ ap βˆ’_ (*-gives-id-l x) ⟩
       βˆ’  x           ∎
   r = βˆ’ (x * (βˆ’ +1)) ＝⟨ ap (Ξ» - β†’ βˆ’ (x * -)) +1-inverse ⟩
       βˆ’ (x *    βˆ’1 ) ＝⟨ ap βˆ’_ (*-gives-negation-l x) ⟩
       βˆ’  (βˆ’ x)       ＝⟨ βˆ’-involutive x ⟩
             x        ∎
   i : is-βŠ•-homomorphism π“˜ π“˜ (Ξ» - β†’ βˆ’ (x * (βˆ’ -)))
   i a b = βˆ’  (x * (βˆ’ (a βŠ• b)))
                ＝⟨ ap (Ξ» - β†’ βˆ’ (x * -)) (βˆ’-is-βŠ•-homomorphism a b) ⟩
           βˆ’  (x * (βˆ’ a βŠ• βˆ’ b))
                ＝⟨ ap βˆ’_ (affine-is-βŠ•-homomorphism (βˆ’ x) x (βˆ’ a) (βˆ’ b)) ⟩
           βˆ’ ((x * βˆ’ a) βŠ• (x * βˆ’ b))
                ＝⟨ affine-is-βŠ•-homomorphism +1 βˆ’1 (x * (βˆ’ a)) (x * (βˆ’ b)) ⟩
           βˆ’ (x * βˆ’ a) βŠ• βˆ’ (x * βˆ’ b) ∎

 *-assoc : (x y z : 𝕀) β†’ x * (y * z) ＝ (x * y) * z
 *-assoc x y z = γ z ⁻¹
  where
   l =      x * (y * βˆ’1) ＝⟨ ap (x *_) (*-gives-negation-l y) ⟩
            x *  (βˆ’ y)   ＝⟨ βˆ’-involutive (x * (βˆ’ y)) ⁻¹ ⟩
     (βˆ’ (βˆ’ (x * βˆ’ y)))   ＝⟨ ap βˆ’_ (*-prop x y ⁻¹) ⟩
         βˆ’ (x * y)       ∎
   r = x * (y * +1) ＝⟨ ap (x *_) (*-gives-id-l y) ⟩
       x * y        ∎
   i : is-βŠ•-homomorphism π“˜ π“˜ (Ξ» z β†’ x * (y * z))
   i a b = x * (y * (a βŠ• b))
                ＝⟨ ap (x *_) (*-is-βŠ•-homomorphism-l y a b) ⟩
           x * (y * a βŠ• y * b)
                ＝⟨ affine-is-βŠ•-homomorphism (βˆ’ x) x (y * a) (y * b) ⟩
           x * (y * a) βŠ• x * (y * b) ∎
   Ξ³ : (Ξ» z β†’ (x * y) * z) ∼ (Ξ» z β†’ x * (y * z))
   Ξ³ = affine-uniquenessΒ· (Ξ» z β†’ x * (y * z)) (βˆ’ (x * y)) (x * y) l r i

\end{code}

 Power series can be implemented from multiplication.
 We also define a halving function from the midpoint.

\begin{code}

 _**_ : 𝕀 β†’ β„• β†’ 𝕀
 a ** 0      = +1
 a ** succ n = a * (a ** n)

 powerseries : (β„• β†’ 𝕀) β†’ (𝕀 β†’ 𝕀)
 powerseries a = Ξ» x β†’ M (Ξ» n β†’ (a n) * (x ** n))

 _/2 : 𝕀 β†’ 𝕀
 _/2 = _βŠ• O
 +1/2 = +1 /2
 βˆ’1/2 = βˆ’1 /2

 infixl 99 _/2

 βˆ’-half : (x : 𝕀) β†’ βˆ’ (x /2) ＝ βˆ’ x /2
 βˆ’-half x = βˆ’-is-βŠ•-homomorphism x O βˆ™ ap (βˆ’ x βŠ•_) O-inverse

 O-half : O /2 ＝ O
 O-half = βŠ•-idem O

 βˆ’1-half : βˆ’ +1/2 ＝ βˆ’1/2
 βˆ’1-half = βˆ’-half +1 βˆ™ ap _/2 +1-inverse

 +1-half : βˆ’ βˆ’1/2 ＝ +1/2
 +1-half = βˆ’-half βˆ’1 βˆ™ ap _/2 βˆ’1-inverse

 half-is-βŠ•-homomorphism : is-βŠ•-homomorphism π“˜ π“˜ _/2
 half-is-βŠ•-homomorphism = βŠ•-is-βŠ•-homomorphism-l π“˜ O

 half-same : (x : 𝕀) β†’ +1/2 * x ＝ x /2
 half-same x = ap (Ξ» - β†’ affine - +1/2 x) βˆ’1-half
             βˆ™ affine-uniquenessΒ· _/2 βˆ’1/2 +1/2
               refl refl half-is-βŠ•-homomorphism x

\end{code}

 Now we assume that we have a doubling function.
 This allows the definition
 of truncated addition and subtraction.

\begin{code}

 double : 𝕀 β†’ 𝕀
 double = pr₁ hd

 double-mid : (x : 𝕀) β†’ double (x /2) ＝ x
 double-mid = pr₁ (prβ‚‚ hd)

 double-left : (x : 𝕀) β†’ double (βˆ’1 βŠ• (βˆ’1 βŠ• x)) ＝ βˆ’1
 double-left = pr₁ (prβ‚‚ (prβ‚‚ hd))

 double-right : (x : 𝕀) β†’ double (+1 βŠ• (+1 βŠ• x)) ＝ +1
 double-right = prβ‚‚ (prβ‚‚ (prβ‚‚ hd))

 _+𝕀_ _βˆ’π•€_ : 𝕀 β†’ 𝕀 β†’ 𝕀
 x +𝕀 y = double (x βŠ• y)
 x βˆ’π•€ y = double (x βŠ– y)

 +𝕀-comm : commutative _+𝕀_
 +𝕀-comm x y = ap double (βŠ•-comm x y)

 +𝕀-itself : (x : 𝕀) β†’ x +𝕀 x ＝ double x
 +𝕀-itself x = ap double (βŠ•-idem x)

 +𝕀-tran : (x y s t : 𝕀) β†’ (x βŠ• y) +𝕀 (s βŠ• t) ＝ (x βŠ• s) +𝕀 (y βŠ• t)
 +𝕀-tran x y s t = ap double (βŠ•-tran x y s t)

 +𝕀-fact : (x y : 𝕀) β†’ x +𝕀 βˆ’ y ＝ double (βˆ’ (y βŠ– x))
 +𝕀-fact x y = ap double (fact x y βˆ™ ap βˆ’_ (βŠ•-comm (βˆ’ x) y))

\end{code}

 Double and half allows it to define a max operation.
 First, there is an operation for maxO,
 this is then used to define max itself.

 We wish to prove that max is a semi-lattice
 (idempotent, commutative and associative').

\begin{code}

 maxO : 𝕀 β†’ 𝕀
 maxO x = double (βˆ’1/2 +𝕀 x) /2 +𝕀 +1/2

 O-midpoint-of-halves : βˆ’1/2 βŠ• +1/2 ＝ O
 O-midpoint-of-halves = βˆ’1/2 βŠ• +1/2     ＝⟨ ap (βˆ’1/2 βŠ•_) (+1-half ⁻¹) ⟩
                        βˆ’1/2 βŠ• (βˆ’ βˆ’1/2) ＝⟨ βŠ–-zero βˆ’1/2 ⟩
                        O ∎

 double-O-is-O : double O ＝ O
 double-O-is-O = double O       ＝⟨ ap double (βŠ•-idem O ⁻¹) ⟩
                 double (O βŠ• O) ＝⟨ double-mid O ⟩
                 O ∎

 double-βˆ’1/2-is-βˆ’1 : double βˆ’1/2 ＝ βˆ’1
 double-βˆ’1/2-is-βˆ’1 = double-mid βˆ’1

 double-+1/2-is-+1 : double +1/2 ＝ +1
 double-+1/2-is-+1 = double-mid +1

 double-βˆ’1-is-βˆ’1 : double βˆ’1 ＝ βˆ’1
 double-βˆ’1-is-βˆ’1 = ap double (βŠ•-idem βˆ’1 ⁻¹ βˆ™ ap (βˆ’1 βŠ•_) (βŠ•-idem βˆ’1 ⁻¹)) βˆ™ double-left βˆ’1

 double-+1-is-+1 : double +1 ＝ +1
 double-+1-is-+1 = ap double (βŠ•-idem +1 ⁻¹ βˆ™ ap (+1 βŠ•_) (βŠ•-idem +1 ⁻¹)) βˆ™ double-right +1

 maxO-O-is-O : maxO O ＝ O
 maxO-O-is-O = maxO O
                 ＝⟨ ap (Ξ» - β†’ (double - /2) +𝕀 +1/2) (double-mid βˆ’1/2) ⟩
               (double βˆ’1/2 /2) +𝕀 +1/2
                 ＝⟨ ap (Ξ» - β†’ - /2 +𝕀 +1/2) (double-left +1) ⟩
               βˆ’1/2 +𝕀 +1/2
                 ＝⟨ ap double O-midpoint-of-halves βˆ™ double-O-is-O ⟩
               O ∎

 max _∨_ : 𝕀 β†’ 𝕀 β†’ 𝕀
 max x y = double (x /2 +𝕀 maxO (y βŠ– x))
 _∨_ = max

 max-idem : idempotent _∨_
 max-idem a = a ∨ a
                ＝⟨ ap (Ξ» - β†’ double ((a /2) +𝕀 maxO -))
                      (βŠ–-zero a) ⟩
              double (double (a /2 βŠ• maxO O))
                ＝⟨ ap (Ξ» - β†’ double ((a /2) +𝕀 -))
                      maxO-O-is-O ⟩
              double (a /2 +𝕀 O)
                ＝⟨ ap double (double-mid (a /2)) ⟩
              double (a /2)
                ＝⟨ double-mid a ⟩
              a ∎

 -- max-comm : commutative _∨_
 -- max-comm x y = {!!}

 -- max-assoc : associative' _∨_
 -- max-assoc = {!!}


\end{code}

 Other functions can be derived from max.

\begin{code}

 min : 𝕀 β†’ 𝕀 β†’ 𝕀
 min x y = βˆ’ (max (βˆ’ x) (βˆ’ y))

 abs : 𝕀 β†’ 𝕀
 abs x = max (βˆ’ x) x


\end{code}

 TODO list:
  * max (_∨_) is a semilattice -- assoc, comm (done idem)
    - derive order from this semilattice.

  * Page 42. - Prove the limit *is* the limit, as above.

  * Binary expansions
           (β„•      β†’      β„•          β†’           𝕀)
           numerator     denominator   numer/denom
           (binary expansion stream applied to M).