----------------------------------------------------------------------------------------------------
-- Arithmetic of Extensional Wellfounded orders
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical #-}

module ExtensionalWellfoundedOrder.Arithmetic where

open import Cubical.Foundations.Prelude

open import Cubical.Relation.Binary
open BinaryRelation renaming (isTrans to isTransitive)
open import Cubical.Induction.WellFounded
  renaming (WellFounded to isWellFounded)

open import Cubical.Data.Sum.Base
open import Cubical.Data.Unit
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Unit.Properties
open import Cubical.Data.Empty.Properties

open import General-Properties

open import ExtensionalWellfoundedOrder.Base

open Ord

{- # Addition -}

_+_ : Ord → Ord → Ord
Carrier (A + B) = Carrier A ⊎ Carrier B

_≺_ (A + B) (inl x) (inl y) = _≺_ A x y
_≺_ (A + B) (inl x) (inr y) = Unit
_≺_ (A + B) (inr x) (inl y) = ⊥
_≺_ (A + B) (inr x) (inr y) = _≺_ B x y

truncated (A + B) (inl x) (inl y) = truncated A x y
truncated (A + B) (inl x) (inr y) = isPropUnit
truncated (A + B) (inr x) (inl y) = isProp⊥
truncated (A + B) (inr x) (inr y) = truncated B x y

wellfounded (A + B) (inl x) = helper x (wellfounded A x) where
  helper : ∀ y → Acc (_≺_ A) y → Acc (_≺_ (A + B)) (inl y)
  helper y (acc p) = acc λ { (inl z) z<y → helper z (p z z<y) }
wellfounded (A + B) (inr x) = helper x (wellfounded B x) where
  helper-inl : ∀ y → Acc (_≺_ A) y → Acc (_≺_ (A + B)) (inl y)
  helper-inl y (acc p) = acc λ { (inl z) z<y → helper-inl z (p z z<y) }

  helper : ∀ y → Acc (_≺_ B) y → Acc (_≺_ (A + B)) (inr y)
  helper y (acc p) = acc λ { (inl z) _ → helper-inl z (wellfounded A z)
                           ; (inr z) z<y → helper z (p z z<y) }

extensional (A + B) (inl a) (inl a') ext =
   cong inl (extensional A a a' λ c → (λ c<a  → fst (ext (inl c)) c<a) ,
                                      (λ c<a' → snd (ext (inl c)) c<a'))
extensional (A + B) (inl a) (inr b') ext =
   ⊥.rec (wellfounded→irreflexive (wellfounded A) _ (snd (ext (inl a)) tt))
extensional (A + B) (inr b) (inl a') ext =
   ⊥.rec (wellfounded→irreflexive (wellfounded A) _ (fst (ext (inl a')) tt))
extensional (A + B) (inr b) (inr b') ext =
   cong inr (extensional B b b' λ c → (λ c<b  → fst (ext (inr c)) c<b) ,
                                      (λ c<b' → snd (ext (inr c)) c<b'))

transitive (A + B) (inl x) (inl x₁) (inl x₂) p q = transitive A _ _ _ p q
transitive (A + B) (inl x) (inl x₁) (inr x₂) p q = tt
transitive (A + B) (inl x) (inr x₁) (inr x₂) p q = tt
transitive (A + B) (inr x) (inr x₁) (inr x₂) p q = transitive B _ _ _ p q