Todd Waugh Ambridge, January 2024

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://doi.org/10.1109/LICS.2001.932488

# Formalisation of the Escardo-Simpson interval object

\begin{code}
{-# OPTIONS --without-K --safe #-}

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

module TWA.Thesis.Chapter5.IntervalObject (fe : FunExt) where

open import Naturals.Sequence fe
\end{code}

## Midpoint algebras

\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

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 _βŠ•_)

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

## Iteration property

\begin{code}
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}

## Convex bodies

\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
\end{code}

## Midpoint homomorphisms

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

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

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}

## Interval objects

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

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

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

 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
\end{code}

## Affine map

\begin{code}
 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)

 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}

## M properties

\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

 βŠ•-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}

## Representing [-1,1]

\begin{code}
 βˆ’1 +1 : 𝕀
 βˆ’1 = u
 +1 = v

 O : 𝕀
 O  = βˆ’1 βŠ• +1
\end{code}

## Negation

\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

 _βŠ–_ : 𝕀 β†’ 𝕀 β†’ 𝕀
 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}

## Multiplication

\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-id-l : (x : 𝕀) β†’ x * +1 ＝ x
 *-gives-id-l x = affine-equation-r (βˆ’ x) x

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

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

 *-gives-id-r : (y : 𝕀) β†’ +1 * y ＝ y
 *-gives-id-r y
  = ap (Ξ» - β†’ affine - +1 y) +1-inverse βˆ™ affine-uv-involutive 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

 *-gives-zero-l : (x : 𝕀) β†’ x * O ＝ O
 *-gives-zero-l x = *-is-βŠ•-homomorphism-l x u v
                  βˆ™ ap (_βŠ• (x * v)) (*-gives-negation-l x)
                  βˆ™ ap (βˆ’ x βŠ•_) (*-gives-id-l x)
                  βˆ™ βŠ•-comm (βˆ’ x) x
                  βˆ™ βŠ–-zero x

 *-gives-zero-r : (x : 𝕀) β†’ O * x ＝ O
 *-gives-zero-r x = *-commutative O x βˆ™ *-gives-zero-l x

 *-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}

## Halving

\begin{code}
 _/2 : 𝕀 β†’ 𝕀
 _/2 = _βŠ• O
 +1/2 = +1 /2
 βˆ’1/2 = βˆ’1 /2
\end{code}