Martin Escardo, 15th April 2025

We look at convex bodies (= cancellative, iterative mindpoint objects)
in the ∞-topos of types.

NB. Here the category of sets in a universe 𝓀 can be any 𝟏-topos in models.

These are experimental thoughts while finishing the joirnal version of
the interval objects paper with Alex Simpson.

Euclidean interval objects in categories with finite products
https://arxiv.org/abs/2504.21551

\begin{code}

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

open import MLTT.Spartan hiding (_+_)
open import Naturals.Addition
open import UF.FunExt
open import UF.Sets
open import UF.Sets-Properties
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Subsingletons-Properties
open import UF.Base

module gist.IntervalObject
        (fe : Fun-Ext)
       where

convex-body-structure : 𝓀 Μ‡ β†’ 𝓀 Μ‡
convex-body-structure X = X β†’ X β†’ X

is-convex-body : (X : 𝓀 Μ‡ ) β†’ convex-body-structure X β†’ 𝓀 Μ‡
is-convex-body X _βŠ•_ = Carrier-is-set Γ— Idemp Γ— Comm Γ— Transp Γ— Cancel Γ— Iter
 where
  Carrier-is-set = is-set X
  Idemp  = (x : X) β†’ x βŠ• x ＝ x
  Comm   = (x y : X) β†’ x βŠ• y ＝ y βŠ• x
  Transp = (a b x y : X) β†’ (a βŠ• b) βŠ• (x βŠ• y) ＝ (a βŠ• x) βŠ• (b βŠ• y)
  Cancel = (a x y : X) β†’ a βŠ• x ＝ a βŠ• y β†’ x ＝ y
  Iter   = Ξ£ ⨁ κž‰ ((β„• β†’ X) β†’ X) , Unfolding ⨁ Γ— Canonicity ⨁
   where
    Unfolding =  ⨁ ↦ ((x : β„• β†’ X) β†’ ⨁ x ＝ x 0 βŠ• ⨁ (x ∘ succ))

    Canonicity = ⨁ ↦ ((x y : β„• β†’ X)
                      β†’ ((i : β„•) β†’ y i ＝ x i βŠ• y (succ i))
                      β†’ y 0 ＝ ⨁ x)
\end{code}

NB. We are adopting the formulation of iteration that uses unfolding
an canonicity, which is possible as we have a natural numbers type.

NB. The iteration axiom is property, and hence so is
is-convex-body. (TODO in due course.)

\begin{code}

Convex-Body : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
Convex-Body 𝓀 = Ξ£ A κž‰ 𝓀 Μ‡ , Ξ£ s κž‰ convex-body-structure A , is-convex-body A s

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

is-hom : (𝓐 : Convex-Body 𝓀) (𝓑 : Convex-Body π“₯)
       β†’ (⟨ 𝓐 ⟩ β†’ ⟨ 𝓑 ⟩) β†’ 𝓀 βŠ” π“₯ Μ‡
is-hom (A , _βŠ•_ , _) (_ , _⊞_ , _) f = (x y : A) β†’ f (x βŠ• y) ＝ f x ⊞ f y

is-Hom : (𝓐 : Convex-Body 𝓀) (𝓑 : Convex-Body π“₯)
       β†’ (⟨ 𝓐 ⟩ β†’ ⟨ 𝓑 ⟩) β†’ 𝓀 βŠ” π“₯ Μ‡
is-Hom (A , _ , _ , _ , _ , _ , _ , ⨁ᡃ , _)
       (_ , _ , _ , _ , _ , _ , _ , ⨁ᡇ , _) f
 = (x : β„• β†’ A) β†’ f (⨁ᡃ x) ＝ ⨁ᡇ (f ∘ x)

homs-are-Homs : (𝓐 : Convex-Body 𝓀) (𝓑 : Convex-Body π“₯)
                (f : ⟨ 𝓐 ⟩ β†’ ⟨ 𝓑 ⟩)
              β†’ is-hom 𝓐 𝓑 f
              β†’ is-Hom 𝓐 𝓑 f
homs-are-Homs (_ , _βŠ•α΅ƒ_ , _ , _ , _ , _ , _ , ⨁ᡃ , unfoldingᡃ , _)
              (_ , _βŠ•α΅‡_ , _ , _ , _ , _ , _ , ⨁ᡇ , _          , canonicityᡇ)
              f f-is-hom x
 = II
 where
  I : (i : β„•) β†’ f (⨁ᡃ (j ↦ x (j + i))) ＝ (f (x i) βŠ•α΅‡ f (⨁ᡃ (j ↦ x (j + succ i))))
  I i = f (⨁ᡃ (j ↦ x (j + i)))                       ＝⟨ ap f (unfoldingᡃ _) ⟩
        f (x (0 + i) βŠ•α΅ƒ ⨁ᡃ (j ↦ x (succ j + i)))     ＝⟨ f-is-hom _ _ ⟩
        f (x (0 + i)) βŠ•α΅‡ f (⨁ᡃ (j ↦ x (succ j + i))) ＝⟨ I₁ ⟩
        (f (x i) βŠ•α΅‡ f (⨁ᡃ (j ↦ x (j + succ i))))     ∎
    where
     Iβ‚€ = j ↦ (succ j + i   ＝⟨ addition-commutativity (succ j) i ⟩
               i + succ j   ＝⟨ refl ⟩
               succ (i + j) ＝⟨ ap succ (addition-commutativity i j) ⟩
               succ (j + i) ＝⟨ refl ⟩
               j + succ i   ∎)

     I₁ = apβ‚‚ _βŠ•α΅‡_
           (ap (f ∘ x) (addition-commutativity 0 i))
           (ap (f ∘ ⨁ᡃ) (dfunext fe (j ↦ ap x (Iβ‚€ j))))

  II : f (⨁ᡃ x) ＝ ⨁ᡇ (f ∘ x)
  II = canonicityᡇ (f ∘ x) (i ↦ f (⨁ᡃ (j ↦ x (j + i)))) I


\end{code}

TODO. Add a proof Homs-are-homs of the converse (not needed for our
current purposes).

\begin{code}

id-is-hom : (𝓐 : Convex-Body 𝓀)
          β†’ is-hom 𝓐 𝓐 id
id-is-hom 𝓐 aβ‚€ a₁ = refl

const-is-hom : (𝓐 : Convex-Body 𝓀) (𝓑 : Convex-Body π“₯)
               (b : ⟨ 𝓑 ⟩)
             β†’ is-hom 𝓐 𝓑 (_ ↦ b)
const-is-hom 𝓐 𝓑@(_ , _βŠ•_ , _ , idemp , _) b aβ‚€ a₁ = (idemp b)⁻¹

module _ (𝓐@(A , _βŠ•_ , _ , idemp , _ , transp , _) : Convex-Body 𝓀) where

 βŠ•-is-left-hom : (x : A)
               β†’ is-hom 𝓐 𝓐 (_βŠ• x)
 βŠ•-is-left-hom x y z =
  (y βŠ• z) βŠ• x       ＝⟨ ap ((y βŠ• z) βŠ•_) ((idemp x)⁻¹) ⟩
  (y βŠ• z) βŠ• (x βŠ• x) ＝⟨ transp y z x x ⟩
  (y βŠ• x) βŠ• (z βŠ• x) ∎

 βŠ•-is-right-hom : (x : A)
                β†’ is-hom 𝓐 𝓐 (x βŠ•_)
 βŠ•-is-right-hom x y z =
  x βŠ• (y βŠ• z)       ＝⟨ ap (_βŠ• (y βŠ• z)) ((idemp x)⁻¹) ⟩
  (x βŠ• x) βŠ• (y βŠ• z) ＝⟨ transp x x y z ⟩
  (x βŠ• y) βŠ• (x βŠ• z) ∎

∘-is-hom : (𝓐 : Convex-Body 𝓀) (𝓑 : Convex-Body π“₯) (𝓒 : Convex-Body 𝓦)
           (f : ⟨ 𝓐 ⟩ β†’ ⟨ 𝓑 ⟩) (g : ⟨ 𝓑 ⟩ β†’ ⟨ 𝓒 ⟩)
         β†’ is-hom 𝓐 𝓑 f
         β†’ is-hom 𝓑 𝓒 g
         β†’ is-hom 𝓐 𝓒 (g ∘ f)
∘-is-hom 𝓐@(A , _βŠ•α΅ƒ_ , _) 𝓑@(B , _βŠ•α΅‡_ , _) 𝓒@(C , _βŠ•αΆœ_ , _)
         f g f-is-hom g-is-hom aβ‚€ a₁ =
 g (f (aβ‚€ βŠ•α΅ƒ a₁))           ＝⟨ ap g (f-is-hom aβ‚€ a₁) ⟩
 g (f aβ‚€ βŠ•α΅‡ f a₁)           ＝⟨ g-is-hom (f aβ‚€) (f a₁) ⟩
 ((g ∘ f) aβ‚€ βŠ•αΆœ (g ∘ f) a₁) ∎

is-interval-object : (𝓐 : Convex-Body 𝓀) β†’ ⟨ 𝓐 ⟩ β†’ ⟨ 𝓐 ⟩ β†’ 𝓀ω
is-interval-object 𝓐 aβ‚€ a₁ =
  {π“₯ : Universe} (𝓑 : Convex-Body π“₯) (bβ‚€ b₁ : ⟨ 𝓑 ⟩)
 β†’ βˆƒ! h κž‰ (⟨ 𝓐 ⟩ β†’ ⟨ 𝓑 ⟩) , is-hom 𝓐 𝓑 h
                           Γ— (h aβ‚€ ＝ bβ‚€)
                           Γ— (h a₁ ＝ b₁)

module _ (𝓧@(X ,
             _⊞_ ,
             X-is-set ,
             ⊞-idemp ,
             ⊞-comm ,
             ⊞-transp ,
             ⊞-cancel ,
             ⊞-iter@(M , ⊞-unfolding , ⊞-canonicity))
           : Convex-Body π“₯)
       where

 append : X β†’ (β„• β†’ X) β†’ (β„• β†’ X)
 append x s 0        = x
 append x s (succ i) = s i

 constant-sequence : X β†’ (β„• β†’ X)
 constant-sequence x i = x

 ⊞-fix : (a x : X) β†’ a ＝ x ⊞ a β†’ a ＝ x
 ⊞-fix a x e = ⊞-cancel a a x
                (a ⊞ a ＝⟨ ⊞-idemp a ⟩
                 a     ＝⟨ e  ⟩
                 x ⊞ a ＝⟨ ⊞-comm x a ⟩
                 a ⊞ x ∎)

 constant-iteration : (x : X) β†’ M (constant-sequence x) ＝ x
 constant-iteration x = ⊞-fix (M (constant-sequence x)) x I
  where
   I : M (constant-sequence x) ＝ x ⊞ M (constant-sequence x)
   I = ⊞-unfolding (constant-sequence x)

 binary-from-infinitary : (x y : X) β†’ M (append x (constant-sequence y)) ＝ x ⊞ y
 binary-from-infinitary x y = I
  where
   I = M (append x (constant-sequence y)) ＝⟨ Iβ‚€ ⟩
       x ⊞ M (constant-sequence y)        ＝⟨ I₁ ⟩
       x ⊞ y                     ∎
        where
         Iβ‚€ = ⊞-unfolding (append x (constant-sequence y))
         I₁ = ap (x ⊞_) (constant-iteration y)

module _ (𝓀 : Universe)
         (π“˜@([𝟎,𝟏] ,
          _βŠ•_ ,
          [𝟎,𝟏]-is-set ,
          βŠ•-idemp ,
          βŠ•-comm ,
          βŠ•-transp ,
          βŠ•-cancel ,
          βŠ•-iter@(⨁ , βŠ•-unfolding , βŠ•-canonicity)) : Convex-Body 𝓀)
         (𝟎 𝟏 : [𝟎,𝟏])
         ([𝟎,𝟏]-is-interval-object : is-interval-object π“˜ 𝟎 𝟏)
       where

 module standard-definitions
         (𝓐@(A , _⊞_ , A-is-set , ⊞-idemp , ⊞-comm , ⊞-transp , ⊞-cancel , ⊞-iter)
           : Convex-Body π“₯)
        where

\end{code}

We think of Ξ± aβ‚€ a₁ defined below as the line from aβ‚€ to a₁ in A, or
as the unique affine function that maps 𝟎 to aβ‚€ and 𝟏 to a₁. We also
think of Ξ± aβ‚€ a₁ r as the weighted average of aβ‚€ and a₁ with left
weight r and right weight 1 - r, often termed a convex combination of
aβ‚€ and a₁.

\begin{code}

  Ξ± : A β†’ A β†’ [𝟎,𝟏] β†’ A
  Ξ± aβ‚€ a₁ = βˆƒ!-witness ([𝟎,𝟏]-is-interval-object 𝓐 aβ‚€ a₁)

  module _ (aβ‚€ a₁ : A) where

   Ξ±-property : is-hom π“˜ 𝓐 (Ξ± aβ‚€ a₁)
              Γ— (Ξ± aβ‚€ a₁ 𝟎 ＝ aβ‚€)
              Γ— (Ξ± aβ‚€ a₁ 𝟏 ＝ a₁)
   Ξ±-property = βˆƒ!-is-witness ([𝟎,𝟏]-is-interval-object 𝓐 aβ‚€ a₁)

   Ξ±-is-hom : is-hom π“˜ 𝓐 (Ξ± aβ‚€ a₁)
   Ξ±-is-hom = pr₁ Ξ±-property

   Ξ±-lawβ‚€ : Ξ± aβ‚€ a₁ 𝟎 ＝ aβ‚€
   Ξ±-lawβ‚€ = pr₁ (prβ‚‚ Ξ±-property)

   Ξ±-law₁ : Ξ± aβ‚€ a₁ 𝟏 ＝ a₁
   Ξ±-law₁ = prβ‚‚ (prβ‚‚ Ξ±-property)

   at-most-one-hom : (h k : ⟨ π“˜ ⟩ β†’ A)
                   β†’ is-hom π“˜ 𝓐 h Γ— (h 𝟎 ＝ aβ‚€) Γ— (h 𝟏 ＝ a₁)
                   β†’ is-hom π“˜ 𝓐 k Γ— (k 𝟎 ＝ aβ‚€) Γ— (k 𝟏 ＝ a₁)
                   β†’ h ∼ k
   at-most-one-hom h k u v =
    happly (witness-uniqueness _ ([𝟎,𝟏]-is-interval-object 𝓐 aβ‚€ a₁) h k u v)

   Ξ±-uniqueness : (h : [𝟎,𝟏] β†’ A)
                β†’ is-hom π“˜ 𝓐 h Γ— (h 𝟎 ＝ aβ‚€) Γ— (h 𝟏 ＝ a₁)
                β†’ h ∼ Ξ± aβ‚€ a₁
   Ξ±-uniqueness h h-property = at-most-one-hom h (Ξ± aβ‚€ a₁) h-property Ξ±-property

   Ξ±-uniqueness⁻¹ : (h : [𝟎,𝟏] β†’ A)
                  β†’ is-hom π“˜ 𝓐 h Γ— (h 𝟎 ＝ aβ‚€) Γ— (h 𝟏 ＝ a₁)
                  β†’ Ξ± aβ‚€ a₁ ∼ h
   α-uniqueness⁻¹ h h-property r = (α-uniqueness h h-property r)⁻¹

  homs-charac : (h : [𝟎,𝟏] β†’ A) β†’ is-hom π“˜ 𝓐 h β†’ h ∼ Ξ± (h 𝟎) (h 𝟏)
  homs-charac h h-is-hom = α-uniqueness (h 𝟎) (h 𝟏) h (h-is-hom , refl , refl)

  homs-charac⁻¹ : (h : [𝟎,𝟏] β†’ A) β†’ is-hom π“˜ 𝓐 h β†’ Ξ± (h 𝟎) (h 𝟏) ∼ h
  homs-charac⁻¹ h h-is-hom r = (homs-charac h h-is-hom r)⁻¹

  Ξ±-lawβ‚‚ : (r : [𝟎,𝟏]) (x : A) β†’ Ξ± x x r ＝ x
  Ξ±-lawβ‚‚ r x = homs-charac⁻¹ (_ ↦ x) (const-is-hom π“˜ 𝓐 x) r

\end{code}

End of module standard-definitions, and still in anonymous module
assumming an interval [𝟎,𝟏].

Observation (17th April 2025). If we don't assume commutativity in the
definition of interval object, but only that 𝟎 βŠ• 𝟏 ＝ 𝟏 βŠ• 𝟎, then we
get commutativity automatically. The advantage of a definition
replacing commutativity by commutativity at 𝟎 and 𝟏 only is that we
have a more general class of convex bodies in the universal
property. However, we will keep working with the less general
definition in this file, leaving the generalization to future work (of
the author or any interested reader).

\begin{code}

 module observation where

  open standard-definitions π“˜

  comm-automaticβ‚€ : (x : [𝟎,𝟏])
                  β†’ 𝟎 βŠ• 𝟏 ＝ 𝟏 βŠ• 𝟎
                  β†’ 𝟎 βŠ• x ＝ x βŠ• 𝟎
  comm-automaticβ‚€ x e = at-most-one-hom (𝟎 βŠ• 𝟎) (𝟎 βŠ• 𝟏) (𝟎 βŠ•_) (_βŠ• 𝟎)
                         (βŠ•-is-right-hom π“˜ 𝟎 , refl , refl)
                         (βŠ•-is-left-hom  π“˜ 𝟎 , refl , (e ⁻¹))
                         x

  comm-automatic₁ : (x : [𝟎,𝟏])
                  β†’ 𝟎 βŠ• 𝟏 ＝ 𝟏 βŠ• 𝟎
                  β†’ 𝟏 βŠ• x ＝ x βŠ• 𝟏
  comm-automatic₁ x e = at-most-one-hom (𝟏 βŠ• 𝟎) (𝟏 βŠ• 𝟏) (𝟏 βŠ•_) (_βŠ• 𝟏)
                         (βŠ•-is-right-hom π“˜ 𝟏 , refl , refl)
                         (βŠ•-is-left-hom  π“˜ 𝟏 , e , refl)
                         x

  comm-automatic : (x y : [𝟎,𝟏])
                 β†’ 𝟎 βŠ• 𝟏 ＝ 𝟏 βŠ• 𝟎
                 β†’ x βŠ• y ＝ y βŠ• x
  comm-automatic x y e =
   at-most-one-hom (x βŠ• 𝟎) (x βŠ• 𝟏) (x βŠ•_) (_βŠ• x)
    (βŠ•-is-right-hom π“˜ x , refl , refl)
    (βŠ•-is-left-hom π“˜ x , comm-automaticβ‚€ x e , comm-automatic₁ x e)
    y

\end{code}

End of module observation and still in the anonymous module assuming
an interval object [𝟎,𝟏].

\begin{code}

 open standard-definitions

 private
  Ξ±Μ² : [𝟎,𝟏] β†’ [𝟎,𝟏] β†’ [𝟎,𝟏] β†’ [𝟎,𝟏]
  Ξ±Μ² = Ξ± π“˜

 line-from-𝟎-to-𝟏-is-id : α̲ 𝟎 𝟏 ∼ id
 line-from-𝟎-to-𝟏-is-id = homs-charac⁻¹ π“˜ id (id-is-hom π“˜)

\end{code}

Induction on [𝟎,𝟏]. (Added 28th April 2025.)

This requires more than just a category with finite
products. Everything else in this file should work in a category with
finite products.

TODO. There should be a variation that doesn't assume that P is prop-valued.

\begin{code}

 is-closed-under-midpoint : ([𝟎,𝟏] β†’ π“₯ Μ‡ ) β†’ 𝓀 βŠ” π“₯ Μ‡
 is-closed-under-midpoint P = (r s : [𝟎,𝟏]) β†’ P r β†’ P s β†’ P (r βŠ• s)

 is-closed-under-big-midpoint : ([𝟎,𝟏] β†’ π“₯ Μ‡ ) β†’ 𝓀 βŠ” π“₯ Μ‡
 is-closed-under-big-midpoint P = (x : β„• β†’ [𝟎,𝟏]) β†’ ((i : β„•) β†’ P (x i)) β†’ P (⨁ x)

 closure-under-big-midpoint-gives-closure-under-midpoint
  : (P : [𝟎,𝟏] β†’ π“₯ Μ‡ )
  β†’ is-closed-under-big-midpoint P
  β†’ is-closed-under-midpoint P
 closure-under-big-midpoint-gives-closure-under-midpoint
  P P⨁ r s pr ps
  = transport P
     (binary-from-infinitary π“˜ r s)
     (P⨁ (append π“˜ r (constant-sequence π“˜ s)) I)
    where
     I : (i : β„•) β†’ P (append π“˜ r (constant-sequence π“˜ s) i)
     I 0        = pr
     I (succ i) = ps

 [𝟎,𝟏]-induction
  : (P : [𝟎,𝟏] β†’ π“₯ Μ‡ )
  β†’ ((r : [𝟎,𝟏]) β†’ is-prop (P r))
  β†’ P 𝟎
  β†’ P 𝟏
  β†’ is-closed-under-big-midpoint P
  β†’ (r : [𝟎,𝟏]) β†’ P r
 [𝟎,𝟏]-induction {π“₯} P P-is-prop-valued Pβ‚€ P₁ P⨁ = VI
  where
   X : 𝓀 βŠ” π“₯ Μ‡
   X = Ξ£ r κž‰ [𝟎,𝟏] , P r

   X-is-set : is-set X
   X-is-set = subtypes-of-sets-are-sets' pr₁
               (pr₁-lc (P-is-prop-valued _))
               [𝟎,𝟏]-is-set

   PβŠ• : (r s : [𝟎,𝟏]) β†’ P r β†’ P s β†’ P (r βŠ• s)
   PβŠ• = closure-under-big-midpoint-gives-closure-under-midpoint P P⨁

   _⊞_ : X β†’ X β†’ X
   (r , pr) ⊞ (s , ps) = r βŠ• s , PβŠ• r s pr ps

   ⊞-idemp : (x : X) β†’ x ⊞ x ＝ x
   ⊞-idemp (r , _) = to-subtype-＝ P-is-prop-valued (βŠ•-idemp r)

   ⊞-comm : (x y : X) β†’ x ⊞ y ＝ y ⊞ x
   ⊞-comm (r , _) (s , _) = to-subtype-＝ P-is-prop-valued (βŠ•-comm r s)

   ⊞-transp : (a b x y : X) β†’ (a ⊞ b) ⊞ (x ⊞ y) ＝ (a ⊞ x) ⊞ (b ⊞ y)
   ⊞-transp (u , _) (v , _) (r , _) (s , _) =
    to-subtype-＝ P-is-prop-valued (βŠ•-transp u v r s)

   ⊞-cancel : (a x y : X) β†’ a ⊞ x ＝ a ⊞ y β†’ x ＝ y
   ⊞-cancel (u , _) (r , _) (s , _) e =
    to-subtype-＝ P-is-prop-valued (βŠ•-cancel u r s (ap pr₁ e))

   M : (β„• β†’ X) β†’ X
   M x = (⨁ (pr₁ ∘ x)) ,
         P⨁ (pr₁ ∘ x) (prβ‚‚ ∘ x)

   ⊞-unfolding : (x : β„• β†’ X) β†’ M x ＝ x 0 ⊞ M (x ∘ succ)
   ⊞-unfolding x = to-subtype-＝ P-is-prop-valued (βŠ•-unfolding (pr₁ ∘ x))

   ⊞-canonicity : (x y : β„• β†’ X)
                β†’ ((i : β„•) β†’ y i ＝ x i ⊞ y (succ i))
                β†’ y 0 ＝ M x
   ⊞-canonicity x y a = to-subtype-＝ P-is-prop-valued
                         (βŠ•-canonicity (pr₁ ∘ x) (pr₁ ∘ y) (Ξ» i β†’ ap pr₁ (a i)))

   ⊞-iter = M , ⊞-unfolding , ⊞-canonicity

   𝓧 : Convex-Body (𝓀 βŠ” π“₯)
   𝓧 = X , _⊞_ , X-is-set , ⊞-idemp , ⊞-comm , ⊞-transp , ⊞-cancel , ⊞-iter

   xβ‚€ x₁ : X
   xβ‚€ = 𝟎 , Pβ‚€
   x₁ = 𝟏 , P₁

   h : [𝟎,𝟏] β†’ X
   h = Ξ± 𝓧 xβ‚€ x₁

   pr₁-is-hom : is-hom 𝓧 π“˜ pr₁
   pr₁-is-hom x y = refl

   I : is-hom π“˜ π“˜ (pr₁ ∘ h)
   I = ∘-is-hom π“˜ 𝓧 π“˜ h pr₁ (Ξ±-is-hom 𝓧 xβ‚€ x₁) pr₁-is-hom

   IIβ‚€ : pr₁ (h 𝟎) ＝ 𝟎
   IIβ‚€ = ap pr₁ (Ξ±-lawβ‚€ 𝓧 xβ‚€ x₁)

   II₁ : pr₁ (h 𝟏) ＝ 𝟏
   II₁ = ap pr₁ (Ξ±-law₁ 𝓧 xβ‚€ x₁)

   III : pr₁ ∘ h ∼ Ξ±Μ² 𝟎 𝟏
   III = Ξ±-uniqueness π“˜ 𝟎 𝟏 (pr₁ ∘ h) (I , IIβ‚€ , II₁)

   IV : pr₁ ∘ h ∼ id
   IV r = III r βˆ™ line-from-𝟎-to-𝟏-is-id r

   V : (r : [𝟎,𝟏]) β†’ P (pr₁ (h r))
   V r = prβ‚‚ (h r )

   VI : (r : [𝟎,𝟏]) β†’ P r
   VI r = transport P (IV r) (V r)

\end{code}

Notice, however, that a number of operations can be defined and their
properties can be easily established without induction, using only the
universal property of [𝟎,𝟏].

Complement and multiplication.

\begin{code}

 𝟏- : [𝟎,𝟏] β†’ [𝟎,𝟏]
 𝟏- r = α̲ 𝟏 𝟎 r

 𝟏-𝟎-is-𝟏 : 𝟏- 𝟎 ＝ 𝟏
 𝟏-𝟎-is-𝟏 = Ξ±-lawβ‚€ π“˜ 𝟏 𝟎

 𝟏-𝟏-is-𝟎 : 𝟏- 𝟏 ＝ 𝟎
 𝟏-𝟏-is-𝟎 = Ξ±-law₁ π“˜ 𝟏 𝟎

 𝟏-is-hom : (r s : [𝟎,𝟏]) β†’ 𝟏- (r βŠ• s) ＝ (𝟏- r) βŠ• (𝟏- s)
 𝟏-is-hom = Ξ±-is-hom π“˜ 𝟏 𝟎

 𝟏-involution : (r : [𝟎,𝟏]) β†’ 𝟏- (𝟏- r) ＝ r
 𝟏-involution =
  at-most-one-hom π“˜ 𝟎 𝟏 (𝟏- ∘ 𝟏-) id
   (∘-is-hom π“˜ π“˜ π“˜ 𝟏- 𝟏- 𝟏-is-hom 𝟏-is-hom ,
   (𝟏- (𝟏- 𝟎) ＝⟨ ap 𝟏- 𝟏-𝟎-is-𝟏 ⟩
    𝟏- 𝟏      ＝⟨ 𝟏-𝟏-is-𝟎 ⟩
    𝟎         ∎) ,
   (𝟏- (𝟏- 𝟏) ＝⟨ ap 𝟏- 𝟏-𝟏-is-𝟎 ⟩
    𝟏- 𝟎      ＝⟨ 𝟏-𝟎-is-𝟏 ⟩
    𝟏         ∎))
    (id-is-hom π“˜ , refl , refl)

 ½ : [𝟎,𝟏]
 Β½ = 𝟎 βŠ• 𝟏

 ½-is-𝟏-fix : 𝟏- ½ ＝ ½
 ½-is-𝟏-fix =
  𝟏- ½            ＝⟨ 𝟏-is-hom 𝟎 𝟏 ⟩
  (𝟏- 𝟎) βŠ• (𝟏- 𝟏) ＝⟨ apβ‚‚ _βŠ•_ 𝟏-𝟎-is-𝟏 𝟏-𝟏-is-𝟎 ⟩
  𝟏 βŠ• 𝟎           ＝⟨ βŠ•-comm 𝟏 𝟎 ⟩
  𝟎 βŠ• 𝟏           ∎

 βŠ•-𝟏-Β½-property : (r : [𝟎,𝟏]) β†’ r βŠ• (𝟏- r) ＝ Β½
 βŠ•-𝟏-Β½-property =
  at-most-one-hom π“˜ Β½ Β½ h (_ ↦ Β½)
   (h-is-hom , ap (𝟎 βŠ•_) 𝟏-𝟎-is-𝟏 , (ap (𝟏 βŠ•_) 𝟏-𝟏-is-𝟎 βˆ™ βŠ•-comm 𝟏 𝟎))
   (const-is-hom π“˜ π“˜ Β½ , refl , refl)
  where
   h : [𝟎,𝟏] β†’ [𝟎,𝟏]
   h r = r βŠ• (𝟏- r)

   h-is-hom : is-hom π“˜ π“˜ h
   h-is-hom r s =
    (r βŠ• s) βŠ• (𝟏- (r βŠ• s))      ＝⟨ ap ((r βŠ• s) βŠ•_) (𝟏-is-hom r s) ⟩
    (r βŠ• s) βŠ• ((𝟏- r) βŠ• (𝟏- s)) ＝⟨ βŠ•-transp r s (𝟏- r) (𝟏- s) ⟩
    (r βŠ• (𝟏- r)) βŠ• (s βŠ• (𝟏- s)) ∎

 _Β·_ : [𝟎,𝟏] β†’ [𝟎,𝟏] β†’ [𝟎,𝟏]
 r · s = α̲ 𝟎 s r

 𝟎-left : (s : [𝟎,𝟏]) β†’ 𝟎 Β· s ＝ 𝟎
 𝟎-left = Ξ±-lawβ‚€ π“˜ 𝟎

 𝟏-left : (s : [𝟎,𝟏]) β†’ 𝟏 Β· s ＝ s
 𝟏-left = Ξ±-law₁ π“˜ 𝟎

 mult-is-left-hom : (s : [𝟎,𝟏]) β†’ is-hom π“˜ π“˜ (_Β· s)
 mult-is-left-hom = Ξ±-is-hom π“˜ 𝟎

 mult-mid-left-distr : (r s t : [𝟎,𝟏]) β†’ (r βŠ• s) Β· t ＝ (r Β· t) βŠ• (s Β· t)
 mult-mid-left-distr r s t = mult-is-left-hom t r s

 mult-is-assoc : (r s t : [𝟎,𝟏]) β†’ r Β· (s Β· t) ＝ (r Β· s) Β· t
 mult-is-assoc r s t = Ξ³
  where
   I : is-hom π“˜ π“˜ (r ↦ (r Β· s) Β· t)
   I rβ‚€ r₁ =
    ((rβ‚€ βŠ• r₁) Β· s) Β· t             ＝⟨ ap (_Β· t) (mult-is-left-hom s rβ‚€ r₁) ⟩
    ((rβ‚€ Β· s) βŠ• (r₁ Β· s)) Β· t       ＝⟨ mult-is-left-hom t (rβ‚€ Β· s) (r₁ Β· s) ⟩
    ((rβ‚€ Β· s) Β· t) βŠ• ((r₁ Β· s) Β· t) ∎

   IIβ‚€ = (𝟎 Β· s) Β· t ＝⟨ ap (_Β· t) (𝟎-left s) ⟩
         𝟎 · t       ＝⟨ 𝟎-left t ⟩
         𝟎           ∎

   II₁ = (𝟏 Β· s) Β· t ＝⟨ ap (_Β· t) (𝟏-left s) ⟩
         s · t       ∎

   γ : r · (s · t) ＝ (r · s) · t
   Ξ³ = Ξ±-uniqueness⁻¹ π“˜ 𝟎 (s Β· t) (r ↦ (r Β· s) Β· t) (I , IIβ‚€ , II₁) r

 𝟎-right : (r : [𝟎,𝟏]) β†’ r Β· 𝟎 ＝ 𝟎
 𝟎-right r = Ξ±-lawβ‚‚ π“˜ r 𝟎

 𝟏-right : (r : [𝟎,𝟏]) β†’ r Β· 𝟏 ＝ r
 𝟏-right = line-from-𝟎-to-𝟏-is-id

 mult-is-right-hom : (r : [𝟎,𝟏]) β†’ is-hom π“˜ π“˜ (r Β·_)
 mult-is-right-hom r s t = Ξ³
  where
   f g : [𝟎,𝟏] β†’ [𝟎,𝟏]
   f r = r Β· (s βŠ• t)
   g r = (r Β· s) βŠ• (r Β· t)

   f-is-hom : is-hom π“˜ π“˜ f
   f-is-hom = mult-is-left-hom (s βŠ• t)

   g-is-hom : is-hom π“˜ π“˜ g
   g-is-hom rβ‚€ r₁ =
    ((rβ‚€ βŠ• r₁) Β· s) βŠ• ((rβ‚€ βŠ• r₁) Β· t)             ＝⟨ I ⟩
    ((rβ‚€ Β· s) βŠ• (r₁ Β· s)) βŠ• ((rβ‚€ Β· t) βŠ• (r₁ Β· t)) ＝⟨ II ⟩
    ((rβ‚€ Β· s) βŠ• (rβ‚€ Β· t)) βŠ• ((r₁ Β· s) βŠ• (r₁ Β· t)) ∎
     where
      I  = apβ‚‚ _βŠ•_ (mult-is-left-hom s rβ‚€ r₁) (mult-is-left-hom t rβ‚€ r₁)
      II = βŠ•-transp (rβ‚€ Β· s) (r₁ Β· s) (rβ‚€ Β· t) (r₁ Β· t)

   fβ‚€ : f 𝟎 ＝ 𝟎
   fβ‚€ = 𝟎-left (s βŠ• t)

   f₁ : f 𝟏 ＝ s βŠ• t
   f₁ = 𝟏-left (s βŠ• t)

   gβ‚€ : g 𝟎 ＝ 𝟎
   gβ‚€ =  (𝟎 Β· s) βŠ• (𝟎 Β· t) ＝⟨ apβ‚‚ _βŠ•_ (𝟎-left s) (𝟎-left t) ⟩
         𝟎 βŠ• 𝟎             ＝⟨ βŠ•-idemp 𝟎 ⟩
         𝟎                 ∎

   g₁ : g 𝟏 ＝ s βŠ• t
   g₁ = apβ‚‚ _βŠ•_ (𝟏-left s) (𝟏-left t)

   γ : f r ＝ g r
   Ξ³ = at-most-one-hom π“˜ 𝟎 (s βŠ• t) f g
        (f-is-hom , fβ‚€ , f₁)
        (g-is-hom , gβ‚€ , g₁)
        r

 mult-is-comm : (r s : [𝟎,𝟏]) β†’ r Β· s ＝ s Β· r
 mult-is-comm r s = Ξ±-uniqueness⁻¹ π“˜ 𝟎 s (s Β·_)
                     (mult-is-right-hom s , 𝟎-right s , 𝟏-right s)
                     r
 mult-mid-right-distr : (r s t : [𝟎,𝟏]) β†’ r Β· (s βŠ• t) ＝ (r Β· s) βŠ• (r Β· t)
 mult-mid-right-distr = mult-is-right-hom

\end{code}

TODO. r Β· s ＝ 𝟏 β†’ r ＝ 𝟏.

In an interval object [𝟎,𝟏] in a cartesian closed category, we cannot
prove that 𝟎 β‰  𝟏, because a terminal category is cartesian closed and
any of its (terminal) objects is an interval objects, but terminal
objects have only one global point by definition. But we can prove the
following in any ccc with interval object.

\begin{code}

 [𝟎,𝟏]-triviality : 𝟎 ＝ 𝟏 β†’ (r s : [𝟎,𝟏]) β†’ r ＝ s
 [𝟎,𝟏]-triviality e r s =
   r       ＝⟨ (Ξ±-lawβ‚€ π“˜ r s)⁻¹ ⟩
   α̲ r s 𝟎 ＝⟨ ap (α̲ r s) e ⟩
   Ξ±Μ² r s 𝟏 ＝⟨ Ξ±-law₁ π“˜ r s ⟩
   s       ∎

\end{code}

Homomorphisms automatically preserve convex combinations.

\begin{code}

 homs-preserve-ccs : (𝓐 : Convex-Body 𝓀) (𝓑 : Convex-Body π“₯)
                   β†’ (h : ⟨ 𝓐 ⟩ β†’ ⟨ 𝓑 ⟩)
                   β†’ is-hom 𝓐 𝓑 h
                   β†’ (xβ‚€ x₁ : ⟨ 𝓐 ⟩) (r : [𝟎,𝟏])
                   β†’ h (Ξ± 𝓐 xβ‚€ x₁ r) ＝ Ξ± 𝓑 (h xβ‚€) (h x₁) r
 homs-preserve-ccs 𝓐@(A , _βŠ•α΅ƒ_ , _) 𝓑@(_ , _βŠ•α΅‡_ , _) h h-is-hom xβ‚€ x₁ =
  f-and-g-agreement
  where
   f : [𝟎,𝟏] β†’ ⟨ 𝓑 ⟩
   f r = h (Ξ± 𝓐 xβ‚€ x₁ r)

   f-is-hom : is-hom π“˜ 𝓑 f
   f-is-hom = ∘-is-hom π“˜ 𝓐 𝓑 (Ξ± 𝓐 xβ‚€ x₁) h (Ξ±-is-hom 𝓐 xβ‚€ x₁) h-is-hom

   𝟎-agreement : f 𝟎 ＝ h xβ‚€
   𝟎-agreement = ap h (Ξ±-lawβ‚€ 𝓐 xβ‚€ x₁)

   𝟏-agreement : f 𝟏 ＝ h x₁
   𝟏-agreement = ap h (Ξ±-law₁ 𝓐 xβ‚€ x₁)

   f-and-g-agreement : f ∼ Ξ± 𝓑 (h xβ‚€) (h x₁)
   f-and-g-agreement = Ξ±-uniqueness 𝓑 (h xβ‚€) (h x₁) f
                        (f-is-hom , 𝟎-agreement , 𝟏-agreement)

 module _ (𝓧@(X , _⊞_ , X-is-set , ⊞-idemp , ⊞-comm , ⊞-transp , ⊞-cancel , ⊞-iter)
             : Convex-Body π“₯)
        where

  Ξ±Μ… : X β†’ X β†’ [𝟎,𝟏] β†’ X
  Ξ±Μ… = Ξ± 𝓧

  c : [𝟎,𝟏] β†’ X β†’ X β†’ X
  c r x y = Ξ±Μ… x y r

  cΜ… : [𝟎,𝟏] β†’ [𝟎,𝟏] β†’ [𝟎,𝟏] β†’ [𝟎,𝟏]
  cΜ… r x y = Ξ±Μ² x y r

  Β½-combination : (xβ‚€ x₁ : X) β†’ c Β½ xβ‚€ x₁ ＝ xβ‚€ ⊞ x₁
  Β½-combination xβ‚€ x₁ =
   c Β½ xβ‚€ x₁             ＝⟨ refl ⟩
   Ξ±Μ… xβ‚€ x₁ (𝟎 βŠ• 𝟏)       ＝⟨ Ξ±-is-hom 𝓧 xβ‚€ x₁ 𝟎 𝟏 ⟩
   Ξ±Μ… xβ‚€ x₁ 𝟎 ⊞ Ξ±Μ… xβ‚€ x₁ 𝟏 ＝⟨ apβ‚‚ _⊞_ (Ξ±-lawβ‚€ 𝓧 xβ‚€ x₁) (Ξ±-law₁ 𝓧 xβ‚€ x₁) ⟩
   xβ‚€ ⊞ x₁               ∎

  Ξ±-self-hom : (xβ‚€ x₁ : X) (sβ‚€ s₁ r : [𝟎,𝟏])
             β†’ Ξ±Μ… xβ‚€ x₁ (Ξ±Μ² sβ‚€ s₁ r) ＝ Ξ±Μ… (Ξ±Μ… xβ‚€ x₁ sβ‚€) (Ξ±Μ… xβ‚€ x₁ s₁) r
  Ξ±-self-hom xβ‚€ x₁ = homs-preserve-ccs π“˜ 𝓧 (Ξ±Μ… xβ‚€ x₁) (Ξ±-is-hom 𝓧 xβ‚€ x₁)

  c-self-hom : (r sβ‚€ s₁ : [𝟎,𝟏]) (xβ‚€ x₁ : X)
             β†’ c (cΜ… r sβ‚€ s₁) xβ‚€ x₁ ＝ c r (c sβ‚€ xβ‚€ x₁) (c s₁ xβ‚€ x₁)
  c-self-hom r sβ‚€ s₁ xβ‚€ x₁ = Ξ±-self-hom xβ‚€ x₁ sβ‚€ s₁ r

  c-self-hom-special : (r s : [𝟎,𝟏]) (xβ‚€ x₁ : X)
                     β†’ c (r Β· s) xβ‚€ x₁ ＝ c r xβ‚€ (c s xβ‚€ x₁)
  c-self-hom-special r s xβ‚€ x₁ =
   c (r Β· s) xβ‚€ x₁             ＝⟨ I ⟩
   c r (c 𝟎 xβ‚€ x₁) (c s xβ‚€ x₁) ＝⟨ II ⟩
   c r xβ‚€ (c s xβ‚€ x₁)          ∎
    where
     I  = c-self-hom r 𝟎 s xβ‚€ x₁
     II = ap (- ↦ c r - (c s xβ‚€ x₁)) (Ξ±-lawβ‚€ 𝓧 xβ‚€ x₁)

  Ξ±-is-hom₀₁ : (xβ‚€ x₁ yβ‚€ y₁ : X) (r : [𝟎,𝟏])
            β†’ Ξ±Μ… (xβ‚€ ⊞ x₁) (yβ‚€ ⊞ y₁) r ＝ Ξ±Μ… xβ‚€ yβ‚€ r ⊞ Ξ±Μ… x₁ y₁ r
  Ξ±-is-hom₀₁ xβ‚€ x₁ yβ‚€ y₁ =
   Ξ±-uniqueness⁻¹ 𝓧 (xβ‚€ ⊞ x₁) (yβ‚€ ⊞ y₁) f (f-is-hom , 𝟎-agreement , 𝟏-agreement)
   where
    f : [𝟎,𝟏] β†’ X
    f r = Ξ±Μ… xβ‚€ yβ‚€ r ⊞ Ξ±Μ… x₁ y₁ r

    f-is-hom : is-hom π“˜ 𝓧 f
    f-is-hom r s =
     (Ξ±Μ… xβ‚€ yβ‚€ (r βŠ• s) ⊞ Ξ±Μ… x₁ y₁ (r βŠ• s))               ＝⟨ I ⟩
     (Ξ±Μ… xβ‚€ yβ‚€ r ⊞ Ξ±Μ… xβ‚€ yβ‚€ s) ⊞ (Ξ±Μ… x₁ y₁ r ⊞ Ξ±Μ… x₁ y₁ s) ＝⟨ II ⟩
     (Ξ±Μ… xβ‚€ yβ‚€ r ⊞ Ξ±Μ… x₁ y₁ r) ⊞ (Ξ±Μ… xβ‚€ yβ‚€ s ⊞ Ξ±Μ… x₁ y₁ s) ∎
      where
       I = apβ‚‚
            _⊞_
            (Ξ±-is-hom 𝓧 xβ‚€ yβ‚€ r s)
            (Ξ±-is-hom 𝓧 x₁ y₁ r s)

       II = ⊞-transp (Ξ±Μ… xβ‚€ yβ‚€ r) (Ξ±Μ… xβ‚€ yβ‚€ s) (Ξ±Μ… x₁ y₁ r) (Ξ±Μ… x₁ y₁ s)

    𝟎-agreement : f 𝟎 ＝ xβ‚€ ⊞ x₁
    𝟎-agreement =
     f 𝟎                 ＝⟨ refl ⟩
     Ξ±Μ… xβ‚€ yβ‚€ 𝟎 ⊞ Ξ±Μ… x₁ y₁ 𝟎 ＝⟨ I ⟩
     xβ‚€ ⊞ x₁             ∎
      where
       I = apβ‚‚ _⊞_ (Ξ±-lawβ‚€ 𝓧 xβ‚€ yβ‚€) (Ξ±-lawβ‚€ 𝓧 x₁ y₁)

    𝟏-agreement : f 𝟏 ＝ yβ‚€ ⊞ y₁
    𝟏-agreement =
     f 𝟏                   ＝⟨ refl ⟩
     Ξ±Μ… xβ‚€ yβ‚€ 𝟏 ⊞ Ξ±Μ… x₁ y₁ 𝟏 ＝⟨ I ⟩
     yβ‚€ ⊞ y₁               ∎
      where
       I = apβ‚‚ _⊞_ (Ξ±-law₁ 𝓧 xβ‚€ yβ‚€) (Ξ±-law₁ 𝓧 x₁ y₁)

  Ξ±-is-homβ‚€ : (xβ‚€ x₁ y : X) (r : [𝟎,𝟏])
            β†’ Ξ±Μ… (xβ‚€ ⊞ x₁) y r ＝ Ξ±Μ… xβ‚€ y r ⊞ Ξ±Μ… x₁ y r
  Ξ±-is-homβ‚€ xβ‚€ x₁ y r =
   Ξ±Μ… (xβ‚€ ⊞ x₁) y r       ＝⟨ ap (- ↦ Ξ±Μ… (xβ‚€ ⊞ x₁) - r) ((⊞-idemp y)⁻¹) ⟩
   Ξ±Μ… (xβ‚€ ⊞ x₁) (y ⊞ y) r ＝⟨ Ξ±-is-hom₀₁ xβ‚€ x₁ y y r ⟩
   Ξ±Μ… xβ‚€ y r ⊞ Ξ±Μ… x₁ y r   ∎

  Ξ±-is-hom₁ : (x yβ‚€ y₁ : X) (r : [𝟎,𝟏])
            β†’ Ξ±Μ… x (yβ‚€ ⊞ y₁) r ＝ Ξ±Μ… x yβ‚€ r ⊞ Ξ±Μ… x y₁ r
  Ξ±-is-hom₁ x yβ‚€ y₁ r =
   Ξ±Μ… x (yβ‚€ ⊞ y₁) r       ＝⟨ ap (- ↦ Ξ±Μ… - (yβ‚€ ⊞ y₁) r) ((⊞-idemp x)⁻¹) ⟩
   Ξ±Μ… (x ⊞ x) (yβ‚€ ⊞ y₁) r ＝⟨ Ξ±-is-hom₀₁ x x yβ‚€ y₁ r ⟩
   Ξ±Μ… x yβ‚€ r ⊞ Ξ±Μ… x y₁ r   ∎

  Ξ±-law₃ : (r : [𝟎,𝟏]) (x y : X) β†’ c r x y ＝ c (𝟏- r) y x
  Ξ±-law₃ r x y = III
   where
    I : is-hom π“˜ 𝓧 (- ↦ c (𝟏- -) y x)
    I = ∘-is-hom π“˜ π“˜ 𝓧 𝟏- (- ↦ c - y x) (Ξ±-is-hom π“˜ 𝟏 𝟎) (Ξ±-is-hom 𝓧 y x)

    IIβ‚€ = c (𝟏- 𝟎) y x    ＝⟨ refl ⟩
          Ξ±Μ… y x (Ξ±Μ² 𝟏 𝟎 𝟎) ＝⟨ ap (Ξ±Μ… y x) (Ξ±-lawβ‚€ π“˜ 𝟏 𝟎) ⟩
          Ξ±Μ… y x 𝟏         ＝⟨ Ξ±-law₁ 𝓧 y x ⟩
          x               ∎

    II₁ = c (𝟏- 𝟏) y x    ＝⟨ refl ⟩
          Ξ±Μ… y x (Ξ±Μ² 𝟏 𝟎 𝟏) ＝⟨ ap (Ξ±Μ… y x) (Ξ±-law₁ π“˜ 𝟏 𝟎) ⟩
          Ξ±Μ… y x 𝟎         ＝⟨ Ξ±-lawβ‚€ 𝓧 y x ⟩
          y               ∎

    III : c r x y ＝ c (𝟏- r) y x
    III = Ξ±-uniqueness⁻¹ 𝓧 x y (Ζ› ↦ c (𝟏- Ζ›) y x) (I , IIβ‚€ , II₁) r

\end{code}