{-# OPTIONS --safe #-}
module DepthComonads.Algebra.Monus where
open import DepthComonads.Prelude
open import DepthComonads.Algebra
open import DepthComonads.Relation.Binary
open import DepthComonads.Function.Reasoning
record POM {ℓ₁} (𝑆 : Type ℓ₁) ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
field commutativeMonoid : CommutativeMonoid 𝑆
open CommutativeMonoid commutativeMonoid public
field preorder : Preorder 𝑆 ℓ₂
open Preorder preorder public renaming (refl to ≤-refl)
field
positive : ∀ x → ε ≤ x
≤-cong : ∀ x {y z} → y ≤ z → x ∙ y ≤ x ∙ z
x≤x∙y : ∀ {x y} → x ≤ x ∙ y
x≤x∙y {x} {y} = subst (_≤ x ∙ y) (∙ε x) (≤-cong x (positive y))
≤-congʳ : ∀ x {y z} → y ≤ z → y ∙ x ≤ z ∙ x
≤-congʳ x {y} {z} p = subst₂ _≤_ (comm x y) (comm x z) (≤-cong x p)
alg-≤-trans : ∀ {x y z k₁ k₂} → y ≡ x ∙ k₁ → z ≡ y ∙ k₂ → z ≡ x ∙ (k₁ ∙ k₂)
alg-≤-trans {x} {y} {z} {k₁} {k₂} y≡x∙k₁ z≡y∙k₂ =
z ≡⟨ z≡y∙k₂ ⟩
y ∙ k₂ ≡⟨ cong (_∙ k₂) y≡x∙k₁ ⟩
(x ∙ k₁) ∙ k₂ ≡⟨ assoc x k₁ k₂ ⟩
x ∙ (k₁ ∙ k₂) ∎
infix 4 _≺_
_≺_ : 𝑆 → 𝑆 → Type _
x ≺ y = ∃ k × (y ≡ x ∙ k) × (k ≢ ε)
record TAPOM {ℓ₁} (𝑆 : Type ℓ₁) ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
field pom : POM 𝑆 ℓ₂
open POM pom public using (preorder; _≤_; ≤-cong; ≤-congʳ; x≤x∙y; commutativeMonoid; positive)
open CommutativeMonoid commutativeMonoid public
field
_≤|≥_ : Total _≤_
antisym : Antisymmetric _≤_
totalOrder : TotalOrder 𝑆 ℓ₂ ℓ₂
totalOrder = fromPartialOrder (record { preorder = preorder ; antisym = antisym }) _≤|≥_
open TotalOrder totalOrder public hiding (_≤|≥_; antisym) renaming (refl to ≤-refl)
module AlgebraicPOM {ℓ} {𝑆 : Type ℓ} (mon : CommutativeMonoid 𝑆) where
commutativeMonoid = mon
open CommutativeMonoid mon
infix 4 _≤_
_≤_ : 𝑆 → 𝑆 → Type _
x ≤ y = ∃ z × (y ≡ x ∙ z)
≤-trans : Transitive _≤_
≤-trans (k₁ , _) (k₂ , _) .fst = k₁ ∙ k₂
≤-trans {x} {y} {z} (k₁ , y≡x∙k₁) (k₂ , z≡y∙k₂) .snd =
z ≡⟨ z≡y∙k₂ ⟩
y ∙ k₂ ≡⟨ cong (_∙ k₂) y≡x∙k₁ ⟩
(x ∙ k₁) ∙ k₂ ≡⟨ assoc x k₁ k₂ ⟩
x ∙ (k₁ ∙ k₂) ∎
preorder : Preorder 𝑆 ℓ
Preorder._≤_ preorder = _≤_
Preorder.refl preorder = ε , sym (∙ε _)
Preorder.trans preorder = ≤-trans
positive : ∀ x → ε ≤ x
positive x = x , sym (ε∙ x)
≤-cong : ∀ x {y z} → y ≤ z → x ∙ y ≤ x ∙ z
≤-cong x (k , z≡y∙k) = k , cong (x ∙_) z≡y∙k ; sym (assoc x _ k)
algebraic-pom : ∀ {ℓ} {𝑆 : Type ℓ} → CommutativeMonoid 𝑆 → POM 𝑆 ℓ
algebraic-pom mon = record { AlgebraicPOM mon }
record TMPOM {ℓ} (𝑆 : Type ℓ) : Type ℓ where
field ⦃ commutativeMonoid ⦄ : CommutativeMonoid 𝑆
pom : POM _ _
pom = algebraic-pom commutativeMonoid
open POM pom public
infix 4 _≤|≥_
field _≤|≥_ : Total _≤_
<⇒≺ : ∀ x y → y ≰ x → x ≺ y
<⇒≺ x y x<y with x ≤|≥ y
... | inr y≤x = ⊥-elim (x<y y≤x)
... | inl (k , y≡x∙k) = λ
where
.fst → k
.snd .fst → y≡x∙k
.snd .snd k≡ε → x<y (ε , sym (∙ε y ; y≡x∙k ; cong (x ∙_) k≡ε ; ∙ε x))
infixl 6 _∸_
_∸_ : 𝑆 → 𝑆 → 𝑆
x ∸ y = either′ (const ε) fst (x ≤|≥ y)
x∸y≤x : ∀ x y → x ∸ y ≤ x
x∸y≤x x y with x ≤|≥ y
... | inl (k , p) = positive x
... | inr (k , x≡y∙k) = y , x≡y∙k ; comm y k
record TMAPOM {ℓ} (𝑆 : Type ℓ) : Type ℓ where
field tmpom : TMPOM 𝑆
open TMPOM tmpom public using (_≤_; _≤|≥_; positive; alg-≤-trans; _≺_; <⇒≺; _∸_; x∸y≤x)
field antisym : Antisymmetric _≤_
tapom : TAPOM _ _
TAPOM.pom tapom = TMPOM.pom tmpom
TAPOM._≤|≥_ tapom = _≤|≥_
TAPOM.antisym tapom = antisym
open TAPOM tapom public hiding (antisym; _≤|≥_; _≤_; positive)
zeroSumFree : ∀ x y → x ∙ y ≡ ε → x ≡ ε
zeroSumFree x y x∙y≡ε = antisym (y , sym x∙y≡ε) (positive x)
≺-trans : Transitive _≺_
≺-trans {x} {y} {z} (i , y≡x∙i , i≢ε) (j , z≡y∙j , j≢ε) =
i ∙ j , alg-≤-trans y≡x∙i z≡y∙j , i≢ε ∘ zeroSumFree i j
≤‿∸‿cancel : ∀ x y → x ≤ y → (y ∸ x) ∙ x ≡ y
≤‿∸‿cancel x y x≤y with y ≤|≥ x
... | inl y≤x = ε∙ x ; antisym x≤y y≤x
... | inr (k , y≡x∙k) = comm k x ; sym y≡x∙k
∸‿comm : ∀ x y → x ∙ (y ∸ x) ≡ y ∙ (x ∸ y)
∸‿comm x y with y ≤|≥ x | x ≤|≥ y
... | inl y≤x | inl x≤y = cong (_∙ ε) (antisym x≤y y≤x)
... | inr (k , y≡x∙k) | inl x≤y = sym y≡x∙k ; sym (∙ε y)
... | inl y≤x | inr (k , x≥y) = ∙ε x ; x≥y
... | inr (k₁ , y≡x∙k₁) | inr (k₂ , x≡y∙k₂) =
x ∙ k₁ ≡˘⟨ y≡x∙k₁ ⟩
y ≡⟨ antisym (k₂ , x≡y∙k₂) (k₁ , y≡x∙k₁) ⟩
x ≡⟨ x≡y∙k₂ ⟩
y ∙ k₂ ∎
∸‿≺ : ∀ x y → x ≢ ε → y ≢ ε → x ∸ y ≺ x
∸‿≺ x y x≢ε y≢ε with x ≤|≥ y
... | inl _ = x , sym (ε∙ x) , x≢ε
... | inr (k , x≡y∙k) = y , x≡y∙k ; comm y k , y≢ε
record CMM {ℓ} (𝑆 : Type ℓ) : Type ℓ where
field commutativeMonoid : CommutativeMonoid 𝑆
pom : POM _ _
pom = algebraic-pom commutativeMonoid
open POM pom public
field _∸_ : 𝑆 → 𝑆 → 𝑆
infixl 6 _∸_
field
∸‿comm : ∀ x y → x ∙ (y ∸ x) ≡ y ∙ (x ∸ y)
∸‿assoc : ∀ x y z → (x ∸ y) ∸ z ≡ x ∸ (y ∙ z)
∸‿inv : ∀ x → x ∸ x ≡ ε
ε∸ : ∀ x → ε ∸ x ≡ ε
∸ε : ∀ x → x ∸ ε ≡ x
∸ε x =
x ∸ ε ≡˘⟨ ε∙ (x ∸ ε) ⟩
ε ∙ (x ∸ ε) ≡⟨ ∸‿comm ε x ⟩
x ∙ (ε ∸ x) ≡⟨ cong (x ∙_) (ε∸ x) ⟩
x ∙ ε ≡⟨ ∙ε x ⟩
x ∎
∸≤ : ∀ x y → x ≤ y → x ∸ y ≡ ε
∸≤ x y (k , y≡x∙k) =
x ∸ y ≡⟨ cong (x ∸_) y≡x∙k ⟩
x ∸ (x ∙ k) ≡˘⟨ ∸‿assoc x x k ⟩
(x ∸ x) ∸ k ≡⟨ cong (_∸ k) (∸‿inv x) ⟩
ε ∸ k ≡⟨ ε∸ k ⟩
ε ∎
∣_-_∣ : 𝑆 → 𝑆 → 𝑆
∣ x - y ∣ = (x ∸ y) ∙ (y ∸ x)
_⊔₂_ : 𝑆 → 𝑆 → 𝑆
x ⊔₂ y = x ∙ y ∙ ∣ x - y ∣
_⊓₂_ : 𝑆 → 𝑆 → 𝑆
x ⊓₂ y = (x ∙ y) ∸ ∣ x - y ∣
record CCMM {ℓ} (𝑆 : Type ℓ) : Type ℓ where
field cmm : CMM 𝑆
open CMM cmm public
field ∸‿cancel : ∀ x y → (x ∙ y) ∸ x ≡ y
cancelˡ : Cancellativeˡ _∙_
cancelˡ x y z x∙y≡x∙z =
y ≡˘⟨ ∸‿cancel x y ⟩
(x ∙ y) ∸ x ≡⟨ cong (_∸ x) x∙y≡x∙z ⟩
(x ∙ z) ∸ x ≡⟨ ∸‿cancel x z ⟩
z ∎
cancelʳ : Cancellativeʳ _∙_
cancelʳ x y z y∙x≡z∙x =
y ≡˘⟨ ∸‿cancel x y ⟩
(x ∙ y) ∸ x ≡⟨ cong (_∸ x) (comm x y) ⟩
(y ∙ x) ∸ x ≡⟨ cong (_∸ x) y∙x≡z∙x ⟩
(z ∙ x) ∸ x ≡⟨ cong (_∸ x) (comm z x) ⟩
(x ∙ z) ∸ x ≡⟨ ∸‿cancel x z ⟩
z ∎
zeroSumFree : ∀ x y → x ∙ y ≡ ε → x ≡ ε
zeroSumFree x y x∙y≡ε =
x ≡˘⟨ ∸‿cancel y x ⟩
(y ∙ x) ∸ y ≡⟨ cong (_∸ y) (comm y x) ⟩
(x ∙ y) ∸ y ≡⟨ cong (_∸ y) x∙y≡ε ⟩
ε ∸ y ≡⟨ ε∸ y ⟩
ε ∎
antisym : Antisymmetric _≤_
antisym {x} {y} (k₁ , y≡x∙k₁) (k₂ , x≡y∙k₂) =
x ≡⟨ x≡y∙k₂ ⟩
y ∙ k₂ ≡⟨ [ lemma ]⇒ y ∙ ε ≡ y ∙ (k₂ ∙ k₁)
⟨ cancelˡ y ε (k₂ ∙ k₁) ⟩⇒ ε ≡ k₂ ∙ k₁
⟨ sym ⟩⇒ k₂ ∙ k₁ ≡ ε
⟨ zeroSumFree k₂ k₁ ⟩⇒ k₂ ≡ ε
⟨ cong (y ∙_) ⟩⇒ y ∙ k₂ ≡ y ∙ ε ⇒∎ ⟩
y ∙ ε ≡⟨ ∙ε y ⟩
y ∎
where
lemma = ∙ε y ; alg-≤-trans x≡y∙k₂ y≡x∙k₁
partialOrder : PartialOrder _ _
PartialOrder.preorder partialOrder = preorder
PartialOrder.antisym partialOrder = antisym
≺⇒< : ∀ x y → x ≺ y → y ≰ x
≺⇒< x y (k₁ , y≡x∙k₁ , k₁≢ε) (k₂ , x≡y∙k₂) =
[ x ∙ ε ≡⟨ ∙ε x ⟩
x ≡⟨ x≡y∙k₂ ⟩
y ∙ k₂ ≡⟨ cong (_∙ k₂) y≡x∙k₁ ⟩
(x ∙ k₁) ∙ k₂ ≡⟨ assoc x k₁ k₂ ⟩
x ∙ (k₁ ∙ k₂) ∎ ]⇒ x ∙ ε ≡ x ∙ (k₁ ∙ k₂)
⟨ cancelˡ x ε (k₁ ∙ k₂) ⟩⇒ ε ≡ k₁ ∙ k₂
⟨ sym ⟩⇒ k₁ ∙ k₂ ≡ ε
⟨ zeroSumFree k₁ k₂ ⟩⇒ k₁ ≡ ε
⟨ k₁≢ε ⟩⇒ ⊥ ⇒∎
≤⇒<⇒≢ε : ∀ x y → (x≤y : x ≤ y) → y ≰ x → fst x≤y ≢ ε
≤⇒<⇒≢ε x y (k₁ , y≡x∙k₁) y≰x k₁≡ε = y≰x λ
where
.fst → ε
.snd → x ≡˘⟨ ∙ε x ⟩
x ∙ ε ≡˘⟨ cong (x ∙_) k₁≡ε ⟩
x ∙ k₁ ≡˘⟨ y≡x∙k₁ ⟩
y ≡˘⟨ ∙ε y ⟩
y ∙ ε ∎
≤-cancelʳ : ∀ x y z → y ∙ x ≤ z ∙ x → y ≤ z
≤-cancelʳ x y z (k , z∙x≡y∙x∙k) .fst = k
≤-cancelʳ x y z (k , z∙x≡y∙x∙k) .snd = cancelʳ x z (y ∙ k) $
z ∙ x ≡⟨ z∙x≡y∙x∙k ⟩
(y ∙ x) ∙ k ≡⟨ assoc y x k ⟩
y ∙ (x ∙ k) ≡⟨ cong (y ∙_) (comm x k) ⟩
y ∙ (k ∙ x) ≡˘⟨ assoc y k x ⟩
(y ∙ k) ∙ x ∎
≤-cancelˡ : ∀ x y z → x ∙ y ≤ x ∙ z → y ≤ z
≤-cancelˡ x y z (k , x∙z≡x∙y∙k) .fst = k
≤-cancelˡ x y z (k , x∙z≡x∙y∙k) .snd =
cancelˡ x z (y ∙ k) (x∙z≡x∙y∙k ; assoc x y k)
≺-irrefl : Irreflexive _≺_
≺-irrefl {x} (k , x≡x∙k , k≢ε) = k≢ε (sym (cancelˡ x ε k (∙ε x ; x≡x∙k)))
≤∸ : ∀ x y → (x≤y : x ≤ y) → y ∸ x ≡ fst x≤y
≤∸ x y (k , y≡x∙k) =
y ∸ x ≡⟨ cong (_∸ x) y≡x∙k ⟩
(x ∙ k) ∸ x ≡⟨ ∸‿cancel x k ⟩
k ∎
≤‿∸‿cancel : ∀ x y → x ≤ y → (y ∸ x) ∙ x ≡ y
≤‿∸‿cancel x y (k , y≡x∙k) =
(y ∸ x) ∙ x ≡⟨ cong (λ y → (y ∸ x) ∙ x) y≡x∙k ⟩
((x ∙ k) ∸ x) ∙ x ≡⟨ cong (_∙ x) (∸‿cancel x k) ⟩
k ∙ x ≡⟨ comm k x ⟩
x ∙ k ≡˘⟨ y≡x∙k ⟩
y ∎
record CTMAPOM {ℓ} (𝑆 : Type ℓ) : Type ℓ where
field tmapom : TMAPOM 𝑆
open TMAPOM tmapom public
field cancel : Cancellativeˡ _∙_
module cmm where
∸≤ : ∀ x y → x ≤ y → x ∸ y ≡ ε
∸≤ x y x≤y with x ≤|≥ y
∸≤ x y x≤y | inl _ = refl
∸≤ x y (k₁ , y≡x∙k₁) | inr (k₂ , x≡y∙k₂) =
[ lemma ]⇒ y ∙ ε ≡ y ∙ (k₂ ∙ k₁)
⟨ cancel y ε (k₂ ∙ k₁) ⟩⇒ ε ≡ k₂ ∙ k₁
⟨ sym ⟩⇒ k₂ ∙ k₁ ≡ ε
⟨ zeroSumFree k₂ k₁ ⟩⇒ k₂ ≡ ε ⇒∎
where
lemma = ∙ε y ; alg-≤-trans x≡y∙k₂ y≡x∙k₁
∸‿inv : ∀ x → x ∸ x ≡ ε
∸‿inv x = ∸≤ x x ≤-refl
ε∸ : ∀ x → ε ∸ x ≡ ε
ε∸ x = ∸≤ ε x (positive x)
∸‿assoc : ∀ x y z → (x ∸ y) ∸ z ≡ x ∸ (y ∙ z)
∸‿assoc x y z with x ≤|≥ y
∸‿assoc x y z | inl x≤y = ε∸ z ; sym (∸≤ x (y ∙ z) (≤-trans x≤y x≤x∙y))
∸‿assoc x y z | inr x≥y with x ≤|≥ y ∙ z
∸‿assoc x y z | inr (k₁ , x≡y∙k₁) | inl (k₂ , y∙z≡x∙k₂) = ∸≤ k₁ z (k₂ , lemma)
where
lemma : z ≡ k₁ ∙ k₂
lemma = cancel y z (k₁ ∙ k₂) (alg-≤-trans x≡y∙k₁ y∙z≡x∙k₂)
∸‿assoc x y z | inr (k , x≡y∙k) | inr x≥y∙z with k ≤|≥ z
∸‿assoc x y z | inr (k₁ , x≡y∙k₁) | inr (k₂ , x≡y∙z∙k₂) | inl (k₃ , z≡k₁∙k₃) =
[ lemma₁ ]⇒ ε ≡ k₂ ∙ k₃
⟨ sym ⟩⇒ k₂ ∙ k₃ ≡ ε
⟨ zeroSumFree k₂ k₃ ⟩⇒ k₂ ≡ ε
⟨ sym ⟩⇒ ε ≡ k₂ ⇒∎
where
lemma₃ =
y ∙ k₁ ≡˘⟨ x≡y∙k₁ ⟩
x ≡⟨ x≡y∙z∙k₂ ⟩
(y ∙ z) ∙ k₂ ≡⟨ assoc y z k₂ ⟩
y ∙ (z ∙ k₂) ∎
lemma₂ =
k₁ ∙ ε ≡⟨ ∙ε k₁ ⟩
k₁ ≡⟨ alg-≤-trans z≡k₁∙k₃ (cancel y k₁ (z ∙ k₂) lemma₃) ⟩
k₁ ∙ (k₃ ∙ k₂) ∎
lemma₁ =
ε ≡⟨ cancel k₁ ε (k₃ ∙ k₂) lemma₂ ⟩
k₃ ∙ k₂ ≡⟨ comm k₃ k₂ ⟩
k₂ ∙ k₃ ∎
∸‿assoc x y z | inr (k₁ , x≡y∙k₁) | inr (k₂ , x≡y∙z∙k₂) | inr (k₃ , k₁≡z∙k₃) =
cancel z k₃ k₂ lemma₂
where
lemma₁ =
y ∙ k₁ ≡˘⟨ x≡y∙k₁ ⟩
x ≡⟨ x≡y∙z∙k₂ ⟩
(y ∙ z) ∙ k₂ ≡⟨ assoc y z k₂ ⟩
y ∙ (z ∙ k₂) ∎
lemma₂ =
z ∙ k₃ ≡˘⟨ k₁≡z∙k₃ ⟩
k₁ ≡⟨ cancel y k₁ (z ∙ k₂) lemma₁ ⟩
z ∙ k₂ ∎
open cmm public
∸‿cancel : ∀ x y → (x ∙ y) ∸ x ≡ y
∸‿cancel x y with (x ∙ y) ≤|≥ x
... | inl x∙y≤x = sym (cancel x y ε (antisym x∙y≤x x≤x∙y ; sym (∙ε x)))
... | inr (k , x∙y≡x∙k) = sym (cancel x y k x∙y≡x∙k)
ccmm : CCMM _
ccmm = record { ∸‿cancel = ∸‿cancel
; cmm = record { cmm
; ∸‿comm = ∸‿comm
; commutativeMonoid = commutativeMonoid } }
open CCMM ccmm public
using (cancelʳ; cancelˡ; ∸ε; ≺⇒<; ≤⇒<⇒≢ε; _⊔₂_; _⊓₂_; ≺-irrefl; ≤∸)
∸‿< : ∀ x y → x ≢ ε → y ≢ ε → x ∸ y < x
∸‿< x y x≢ε y≢ε = ≺⇒< (x ∸ y) x (∸‿≺ x y x≢ε y≢ε)
∸‿<-< : ∀ x y → x < y → x ≢ ε → y ∸ x < y
∸‿<-< x y x<y x≢ε = ∸‿< y x (λ y≡ε → x<y (x , sym (cong (_∙ x) y≡ε ; ε∙ x))) x≢ε
2× : 𝑆 → 𝑆
2× x = x ∙ x
≤-prop : ∀ x y → isProp (x ≤ y)
≤-prop x y (k₁ , y≡x∙k₁) (k₂ , y≡x∙k₂) = Σ≡Prop (λ _ → total⇒isSet _ _) (cancelˡ x k₁ k₂ (sym y≡x∙k₁ ; y≡x∙k₂))
open import Cubical.Foundations.HLevels using (isProp×)
≺-prop : ∀ x y → isProp (x ≺ y)
≺-prop x y (k₁ , y≡x∙k₁ , k₁≢ε) (k₂ , y≡x∙k₂ , k₂≢ε) = Σ≡Prop (λ k → isProp× (total⇒isSet _ _) isProp¬) (cancelˡ x k₁ k₂ (sym y≡x∙k₁ ; y≡x∙k₂))