Side collapse: move out of structure

It can be defined in terms of others, as it turns out.

src/Algebra/Fumula/Construct.agda

@@ -171,7 +171,6 @@ module Reverse where
       ; ◆-collapse-middle = F.◆-collapse-middleʳ , F.◆-collapse-middleˡ
       ; ●-outer-commute = outer-commute-with _≈_ _⤙_⤚_ F.sym (RawFumula.● F.rawFumula) F.●-outer-commute
       ; ●-inner-commute = inner-commute-with _≈_ _⤙_⤚_ (RawFumula.● F.rawFumula) F.●-inner-commute
-      ; ●-◆-collapse-side = F.●-◆-collapse-sideʳ , F.●-◆-collapse-sideˡ
       ; ◆-outer-associate = outer-associate-with _≈_ _⤙_⤚_ F.sym (RawFumula.◆ F.rawFumula) F.◆-outer-associate
       ; ◆-pullout = pullout-with _≈_ _⤙_⤚_ (RawFumula.◆ F.rawFumula) F.◆-pullout
       }
@@ -290,9 +289,6 @@ module DirectProduct {c ℓ} where
       ; ●-inner-commute =
         (λ (x₁ , x₂) (y₁ , y₂) → F₁.●-inner-commuteˡ x₁ y₁ , F₂.●-inner-commuteˡ x₂ y₂) ,
         (λ (x₁ , x₂) (y₁ , y₂) → F₁.●-inner-commuteʳ x₁ y₁ , F₂.●-inner-commuteʳ x₂ y₂)
-      ; ●-◆-collapse-side =
-        (λ (x₁ , x₂) → F₁.●-◆-collapse-sideˡ x₁ , F₂.●-◆-collapse-sideˡ x₂) ,
-        (λ (x₁ , x₂) → F₁.●-◆-collapse-sideʳ x₁ , F₂.●-◆-collapse-sideʳ x₂)
       ; ◆-outer-associate = λ (w₁ , w₂) (x₁ , x₂) (y₁ , y₂) (z₁ , z₂) →
         F₁.◆-outer-associate w₁ x₁ y₁ z₁ , F₂.◆-outer-associate w₂ x₂ y₂ z₂
       ; ◆-pullout =

src/Algebra/Fumula/Convert.agda

@@ -130,17 +130,6 @@ module FromRing where
         x + y ≈⟨ +-congʳ (sym (*-identityˡ x)) ⟩
         1# * x + y ≈⟨ +-congʳ (*-congʳ 1≈-1*-1+[-1*-1+-1]) ⟩
         (- 1# * - 1# + (- 1# * - 1# + - 1#)) * x + y ∎)
-    ; ●-◆-collapse-side =
-      (λ x →  begin
-      (- 1# * - 1# + (- 1# * - 1# + - 1#)) * x + (- 1# * - 1# + - 1#) ≈⟨ +-cong (*-congʳ (sym 1≈-1*-1+[-1*-1+-1])) (sym 0≈-1*-1+-1) ⟩
-      1# * x + 0# ≈⟨ +-identityʳ (1# * x) ⟩
-      1# * x ≈⟨ *-identityˡ x ⟩
-      x ∎) ,
-      (λ x → begin
-      x * (- 1# * - 1# + (- 1# * - 1# + - 1#)) + (- 1# * - 1# + - 1#) ≈⟨ +-cong (*-congˡ (sym 1≈-1*-1+[-1*-1+-1])) (sym 0≈-1*-1+-1) ⟩
-      x * 1# + 0# ≈⟨ +-identityʳ (x * 1#) ⟩
-      x * 1# ≈⟨ *-identityʳ x ⟩
-      x ∎)
     ; ◆-outer-associate = λ w x y z → +-congʳ (begin
       (w * x + (- 1# * - 1# + - 1#)) * y ≈⟨ *-congʳ (+-congˡ (sym 0≈-1*-1+-1)) ⟩
       (w * x + 0#) * y ≈⟨ *-congʳ (+-identityʳ (w * x)) ⟩

src/Algebra/Fumula/Properties.agda

@@ -9,7 +9,7 @@ open import Algebra.Fumula.Bundles using (Fumula)
 module Algebra.Fumula.Properties {c ℓ} (F : Fumula c ℓ) where
 
 open import Function.Definitions using (Inverseˡ; Inverseʳ; Inverseᵇ)
-open import Data.Product.Base using (_,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Data.Nat.Base using (zero; suc) renaming (_+_ to _ℕ+_)
 open import Data.Nat.Properties using (+-comm)
 open import Data.Integer.Base using (ℤ; +_; -[1+_]; -1ℤ; 0ℤ; 1ℤ; _+_; _-_)
@@ -19,14 +19,34 @@ open import Relation.Binary.PropositionalEquality using (_≡_) renaming (cong t
 open import Relation.Binary.Reasoning.Setoid setoid
 open import Algebra.Fumula.Definitions _≈_ _⤙_⤚_ using (OuterCommutativeWith)
 
+------------------------------------------------------------------------
+-- The "side collapse" property: the "missing" collapse form,
+-- derivable from the other axioms.
+------------------------------------------------------------------------
+
+●-◆-collapse-sideˡ : ∀ x → (● ⤙ ◆ ⤚ x) ≈ x
+●-◆-collapse-sideˡ x = begin
+  ● ⤙ ◆ ⤚ x ≈⟨ ●-inner-commuteʳ ◆ x ⟩
+  ● ⤙ x ⤚ ◆ ≈⟨ ◆-collapse-middleʳ ● x ⟩
+  x ∎
+
+●-◆-collapse-sideʳ : ∀ x → (x ⤙ ◆ ⤚ ●) ≈ x
+●-◆-collapse-sideʳ x = begin
+  x ⤙ ◆ ⤚ ● ≈⟨ ●-inner-commuteˡ x ◆ ⟩
+  ◆ ⤙ x ⤚ ● ≈⟨ ◆-collapse-middleˡ ● x ⟩
+  x ∎
+
+●-◆-collapse-side : (∀ x → (● ⤙ ◆ ⤚ x) ≈ x) × (∀ x → (x ⤙ ◆ ⤚ ●) ≈ x)
+●-◆-collapse-side = ●-◆-collapse-sideˡ , ●-◆-collapse-sideʳ
+
 ------------------------------------------------------------------------
 -- The "pull apart" property: a way of separating the two ring
 -- operators from within a fumula, or of melding them again.
 ------------------------------------------------------------------------
 
 ●-◆-pull-apartˡ : ∀ x y z → (x ⤙ ◆ ⤚ y) ⤙ z ⤚ ● ≈ x ⤙ z ⤚ y
 ●-◆-pull-apartˡ x y z = begin
-  (x ⤙ ◆ ⤚ y) ⤙ z ⤚ ● ≈⟨  ◆-outer-associate x y ● z  ⟩
+  (x ⤙ ◆ ⤚ y) ⤙ z ⤚ ● ≈⟨ ◆-outer-associate x y ● z ⟩
   x ⤙ z ⤚ (y ⤙ ◆ ⤚ ●) ≈⟨ ⤙⤚-cong refl refl (●-◆-collapse-sideʳ y) ⟩
   x ⤙ z ⤚ y ∎
 
@@ -36,6 +56,9 @@ open import Algebra.Fumula.Definitions _≈_ _⤙_⤚_ using (OuterCommutativeWi
   (● ⤙ ◆ ⤚ x) ⤙ z ⤚ y ≈⟨ ⤙⤚-cong (●-◆-collapse-sideˡ x) refl refl ⟩
   x ⤙ z ⤚ y ∎
 
+●-◆-pull-apart : (∀ x y z → (x ⤙ ◆ ⤚ y) ⤙ z ⤚ ● ≈ x ⤙ z ⤚ y) × (∀ x y z → ● ⤙ z ⤚ (x ⤙ ◆ ⤚ y) ≈ x ⤙ z ⤚ y)
+●-◆-pull-apart = ●-◆-pull-apartˡ , ●-◆-pull-apartʳ
+
 ------------------------------------------------------------------------
 -- Properties of the successor and predecessor operations.
 ------------------------------------------------------------------------
@@ -85,6 +108,9 @@ open import Algebra.Fumula.Definitions _≈_ _⤙_⤚_ using (OuterCommutativeWi
   x ⤙ x ⤙ z ⤚ y ⤚ ● ≈⟨ double-exchange x ● x y z ⟩
   x ⤙ x ⤙ z ⤚ ● ⤚ y ∎
 
+↑-⤙⤚-●-dup-nest : (∀ x y z → x ↑ ⤙ z ⤚ y ≈ x ⤙ ● ⤙ z ⤚ y ⤚ y) × (∀ x y z → x ⤙ z ⤚ y ↑ ≈ x ⤙ x ⤙ z ⤚ ● ⤚ y)
+↑-⤙⤚-●-dup-nest = ↑-⤙⤚-●-dup-nestˡ , ↑-⤙⤚-●-dup-nestʳ
+
 ↓-⤙⤚-■-dup-nestˡ : ∀ x y z → x ↓ ⤙ z ⤚ y ≈ x ⤙ ■ ⤙ z ⤚ y ⤚ y
 ↓-⤙⤚-■-dup-nestˡ x y z = begin
   x ↓ ⤙ z ⤚ y ≈⟨ ◆-pulloutˡ x ■ ● y z ⟩
@@ -99,6 +125,9 @@ open import Algebra.Fumula.Definitions _≈_ _⤙_⤚_ using (OuterCommutativeWi
   x ⤙ x ⤙ z ⤚ y ⤚ ■ ≈⟨ double-exchange x ■ x y z ⟩
   x ⤙ x ⤙ z ⤚ ■ ⤚ y ∎
 
+↓-⤙⤚-■-dup-nest : (∀ x y z → x ↓ ⤙ z ⤚ y ≈ x ⤙ ■ ⤙ z ⤚ y ⤚ y) × (∀ x y z → x ⤙ z ⤚ y ↓ ≈ x ⤙ x ⤙ z ⤚ ■ ⤚ y)
+↓-⤙⤚-■-dup-nest = ↓-⤙⤚-■-dup-nestˡ , ↓-⤙⤚-■-dup-nestʳ
+
 ------------------------------------------------------------------------
 -- Properties of the invert operation.
 ------------------------------------------------------------------------

src/Algebra/Fumula/Structures.agda

@@ -86,7 +86,6 @@ record IsFumula (■ : A) : Set (a ⊔ ℓ) where
     ◆-collapse-middle : (∀ x z → (◆ ⤙ z ⤚ x) ≈ z) × (∀ x z → (x ⤙ z ⤚ ◆) ≈ z)
     ●-outer-commute : OuterCommutativeWith ●
     ●-inner-commute : InnerCommutativeWith ●
-    ●-◆-collapse-side : (∀ x → (● ⤙ ◆ ⤚ x) ≈ x) × (∀ x → (x ⤙ ◆ ⤚ ●) ≈ x) -- not primitive (TODO: move)
 
   ■-collapse-dupˡ : ∀ x → (■ ⤙ x ⤚ x) ≈ ◆
   ■-collapse-dupˡ = proj₁ ■-collapse-dup
@@ -106,12 +105,6 @@ record IsFumula (■ : A) : Set (a ⊔ ℓ) where
   ●-inner-commuteʳ : RightInnerCommutativeWith ●
   ●-inner-commuteʳ = proj₂ ●-inner-commute
 
-  ●-◆-collapse-sideˡ : ∀ x → (● ⤙ ◆ ⤚ x) ≈ x
-  ●-◆-collapse-sideˡ = proj₁ ●-◆-collapse-side
-
-  ●-◆-collapse-sideʳ : ∀ x → (x ⤙ ◆ ⤚ ●) ≈ x
-  ●-◆-collapse-sideʳ = proj₂ ●-◆-collapse-side
-
   field
     ◆-outer-associate : OuterAssociativeWith ◆
     ◆-pullout : PulloutWith ◆