Martin Escardo, 6th May 2022

Arithmetic for trichotomous ordinals.

\begin{code}

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

open import UF.FunExt

module Ordinals.TrichotomousArithmetic
        (fe : FunExt)
       where

open import UF.Subsingletons

open import MLTT.Spartan
open import Notation.CanonicalMap
open import Ordinals.Type
open import Ordinals.Notions
open import Ordinals.Arithmetic fe
open import Ordinals.WellOrderArithmetic
open import Ordinals.TrichotomousType fe
open import Ordinals.Underlying

_+₃_ : Ordinal₃ 𝓀 β†’ Ordinal₃ 𝓀 β†’ Ordinal₃ 𝓀
Ο„ +₃ Ο… = ([ Ο„ ] +β‚’ [ Ο… ]) , +β‚’-is-trichotomous [ Ο„ ] [ Ο… ]
                              (3is-trichotomous Ο„)
                              (3is-trichotomous Ο…)

πŸ˜β‚ƒ πŸ™β‚ƒ πŸšβ‚ƒ : Ordinal₃ 𝓀
πŸ˜β‚ƒ = πŸ˜β‚’ , πŸ˜β‚’-is-trichotomous
πŸ™β‚ƒ = πŸ™β‚’ , πŸ™β‚’-is-trichotomous
πŸšβ‚ƒ = πŸ™β‚ƒ +₃ πŸ™β‚ƒ

ω₃ : Ordinal₃ 𝓀₀
ω₃ = Ο‰ , Ο‰-is-trichotomous

βˆ‘Β³ : (Ο„ : Ordinal₃ 𝓀) β†’ (⟨ Ο„ ⟩ β†’ Ordinal₃ 𝓀) β†’ Ordinal₃ 𝓀
βˆ‘Β³ {𝓀} (Ξ±@(X , _<_ , o) , t) Ο… = ((Ξ£ x κž‰ X , ⟨ Ο… x ⟩) ,
                                 Sum.order ,
                                 Sum.well-order o (Ξ» x β†’ 3is-well-ordered (Ο… x))) ,
                                sum.trichotomy-preservation _ _ t (Ξ» x β†’ 3is-trichotomous (Ο… x))
 where
  _β‰Ί_ : {x : X} β†’ ⟨ Ο… x ⟩ β†’ ⟨ Ο… x ⟩ β†’ 𝓀 Μ‡
  y β‰Ί z = y β‰ΊβŸ¨ Ο… _ ⟩ z

  module Sum = sum-cotransitive fe _<_ _β‰Ί_ (tricho-gives-cotrans _<_ (Transitivity Ξ±) t)

_×₃_ : Ordinal₃ 𝓀 β†’ Ordinal₃ 𝓀 β†’ Ordinal₃ 𝓀
Ο„ ×₃ Ο… = βˆ‘Β³ Ο„  (Ξ» (_ : ⟨ Ο„ ⟩) β†’ Ο…)

\end{code}