collapse-side move out of extrustions too

pthariensflame · May 5, 2024 · 8c73dfd · 8c73dfd
1 parent bbe3bd4
commit 8c73dfd
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 22 deletions.
diff --git a/src/Algebra/Fumula/Extrusion/Convert.agda b/src/Algebra/Fumula/Extrusion/Convert.agda
@@ -93,11 +93,6 @@ module FromModule where
         (x *ₗ 0#) + z ≈⟨ +ᴹ-congʳ (*ₗ-zeroʳ x) ⟩
         0# + z ≈⟨ +ᴹ-identityˡ z ⟩
         z ∎
-      ; ❲❳⤙⤚-●ᶠ-◆-collapse-sideˡ = λ x → begin
-        ((R.- R.1# R.* R.- R.1# R.+ (R.- R.1# R.* R.- R.1# R.+ R.- R.1#)) *ₗ x) + 0# ≈⟨ +ᴹ-congʳ (*ₗ-congʳ R.1≈-1*-1+[-1*-1+-1]) ⟨
-        (R.1# *ₗ x) + 0# ≈⟨ +ᴹ-identityʳ (R.1# *ₗ x) ⟩
-        R.1# *ₗ x ≈⟨ *ₗ-identityˡ x ⟩
-        x ∎
       ; ❲❳⤙⤚-◆ᶠ-◆-outer-associate = λ w x y _ → +ᴹ-congʳ (begin
         (w R.* x R.+ (R.- R.1# R.* R.- R.1# R.+ R.- R.1#)) *ₗ y ≈⟨ *ₗ-congʳ (R.+-congˡ R.0≈-1*-1+-1) ⟨
         (w R.* x R.+ R.0#) *ₗ y ≈⟨ *ₗ-congʳ (R.+-identityʳ (w R.* x)) ⟩
@@ -182,11 +177,6 @@ module FromModule where
         (x *ᵣ R.0#) + z ≈⟨ +ᴹ-congʳ (*ᵣ-zeroʳ x) ⟩
         0# + z ≈⟨ +ᴹ-identityˡ z ⟩
         z ∎
-      ; ⤙⤚❲❳-●ᶠ-◆-collapse-sideʳ = λ x → begin
-        (x *ᵣ (R.- R.1# R.* R.- R.1# R.+ (R.- R.1# R.* R.- R.1# R.+ R.- R.1#))) + 0# ≈⟨ +ᴹ-identityʳ (x *ᵣ (R.- R.1# R.* R.- R.1# R.+ (R.- R.1# R.* R.- R.1# R.+ R.- R.1#))) ⟩
-        x *ᵣ (R.- R.1# R.* R.- R.1# R.+ (R.- R.1# R.* R.- R.1# R.+ R.- R.1#)) ≈⟨ *ᵣ-congˡ R.1≈-1*-1+[-1*-1+-1] ⟨
-        x *ᵣ R.1# ≈⟨ *ᵣ-identityʳ x ⟩
-        x ∎
       ; ⤙⤚❲❳-◆ᶠ-◆-outer-associate = λ w x y _ → +ᴹ-congʳ (begin
         ((w *ᵣ x) + 0#) *ᵣ y ≈⟨ *ᵣ-congʳ (+ᴹ-identityʳ (w *ᵣ x)) ⟩
         ((w *ᵣ x) *ᵣ y) ≈⟨ *ᵣ-assoc w x y ⟩
@@ -255,15 +245,13 @@ module FromModule where
       ; ❲❳⤙⤚-■ᶠ-collapse-dupʳ = ❲❳⤙⤚-■ᶠ-collapse-dupʳ
       ; ❲❳⤙⤚-◆ᶠ-collapse-middleˡ = ❲❳⤙⤚-◆ᶠ-collapse-middleˡ
       ; ❲❳⤙⤚-◆-collapse-middleʳ = ❲❳⤙⤚-◆-collapse-middleʳ
-      ; ❲❳⤙⤚-●ᶠ-◆-collapse-sideˡ = ❲❳⤙⤚-●ᶠ-◆-collapse-sideˡ
       ; ❲❳⤙⤚-◆ᶠ-◆-outer-associate = ❲❳⤙⤚-◆ᶠ-◆-outer-associate
       ; ⤙⤚❲❳-●ᶠ-inner-commuteₗ = ⤙⤚❲❳-●ᶠ-inner-commuteₗ
       ; ⤙⤚❲❳-◆-pulloutₗ = ⤙⤚❲❳-◆-pulloutₗ
       ; ⤙⤚❲❳-◆ᶠ-pulloutᵣ = ⤙⤚❲❳-◆ᶠ-pulloutᵣ
       ; ⤙⤚❲❳-■ᶠ-collapse-dupˡ = ⤙⤚❲❳-■ᶠ-collapse-dupˡ
       ; ⤙⤚❲❳-◆-collapse-middleˡ = ⤙⤚❲❳-◆-collapse-middleˡ
       ; ⤙⤚❲❳-◆ᶠ-collapse-middleʳ = ⤙⤚❲❳-◆ᶠ-collapse-middleʳ
-      ; ⤙⤚❲❳-●ᶠ-◆-collapse-sideʳ = ⤙⤚❲❳-●ᶠ-◆-collapse-sideʳ
       ; ⤙⤚❲❳-◆ᶠ-◆-outer-associate = ⤙⤚❲❳-◆ᶠ-◆-outer-associate
       ; ◆-outer-associate = λ w x y z → +ᴹ-congʳ (begin
         ((w *ₗ x) + 0#) *ᵣ y ≈⟨ *ᵣ-congʳ (+ᴹ-identityʳ (w *ₗ x)) ⟩
@@ -589,17 +577,23 @@ module FromFumulaExtrusion where
       }
       where
         open IsDoubleFumulaExtrusion X
-        module L = IsLeftModule (isLeftModule Fₗ _≈_ ❲_❳⤙_⤚_ ◆ ❲❳⤙⤚-isLeftFumulaExtrusion)
-        module R = IsRightModule (isRightModule Fᵣ _≈_ _⤙_⤚❲_❳ ◆ ⤙⤚❲❳-isRightFumulaExtrusion)
+        L = isLeftModule Fₗ _≈_ ❲_❳⤙_⤚_ ◆ ❲❳⤙⤚-isLeftFumulaExtrusion
+        R = isRightModule Fᵣ _≈_ _⤙_⤚❲_❳ ◆ ⤙⤚❲❳-isRightFumulaExtrusion
+        module L where
+          open IsLeftModule L public
+          open LeftProperties Fₗ record { isLeftFumulaExtrusion = ❲❳⤙⤚-isLeftFumulaExtrusion } public
+        module R where
+          open IsRightModule R public
+          open RightProperties Fᵣ record { isRightFumulaExtrusion = ⤙⤚❲❳-isRightFumulaExtrusion } public
         open IsEquivalence isEquivalence using (refl)
         open SetoidReasoning record { isEquivalence = isEquivalence }
 
         +≈+′ : ∀ x y → (x + y) ≈ (x +′ y)
         +≈+′ x y = begin
           ❲ Fₗ.● ❳⤙ x ⤚ y ≈⟨ ❲❳⤙⤚-●ᶠ-inner-commuteᵣ x y ⟩
-          ❲ Fₗ.● ❳⤙ y ⤚ x ≈⟨ ❲❳⤙⤚-cong Fₗ.refl refl (⤙⤚❲❳-●ᶠ-◆-collapse-sideʳ x) ⟨
+          ❲ Fₗ.● ❳⤙ y ⤚ x ≈⟨ ❲❳⤙⤚-cong Fₗ.refl refl (R.⤙⤚❲❳-●ᶠ-◆-collapse-sideʳ x) ⟨
           ❲ Fₗ.● ❳⤙ y ⤚ (x ⤙ ◆ ⤚❲ Fᵣ.● ❳) ≈⟨ ◆-outer-associate Fₗ.● x Fᵣ.● y ⟨
-          (❲ Fₗ.● ❳⤙ ◆ ⤚ x) ⤙ y ⤚❲ Fᵣ.● ❳ ≈⟨ ⤙⤚❲❳-cong (❲❳⤙⤚-●ᶠ-◆-collapse-sideˡ x) refl Fᵣ.refl ⟩
+          (❲ Fₗ.● ❳⤙ ◆ ⤚ x) ⤙ y ⤚❲ Fᵣ.● ❳ ≈⟨ ⤙⤚❲❳-cong (L.❲❳⤙⤚-●ᶠ-◆-collapse-sideˡ x) refl Fᵣ.refl ⟩
           x ⤙ y ⤚❲ Fᵣ.● ❳ ∎
 
   module _ {fₗ fᵣ x fℓₗ fℓᵣ xℓ} (Fₗ : Fumula fₗ fℓₗ) (Fᵣ : Fumula fᵣ fℓᵣ) where

diff --git a/src/Algebra/Fumula/Extrusion/Properties.agda b/src/Algebra/Fumula/Extrusion/Properties.agda
@@ -20,6 +20,12 @@ module LeftProperties {f fℓ x xℓ} (F : Fumula f fℓ) (X : LeftFumulaExtrusi
   open Setoid setoid using (refl)
   open SetoidReasoning setoid
 
+  ❲❳⤙⤚-●ᶠ-◆-collapse-sideˡ : ∀ x → (❲ F.● ❳⤙ ◆ ⤚ x) ≈ x
+  ❲❳⤙⤚-●ᶠ-◆-collapse-sideˡ x = begin
+    ❲ F.● ❳⤙ ◆ ⤚ x ≈⟨ ❲❳⤙⤚-●ᶠ-inner-commuteᵣ ◆ x ⟩
+    ❲ F.● ❳⤙ x ⤚ ◆ ≈⟨ ❲❳⤙⤚-◆-collapse-middleʳ F.● x ⟩
+    x ∎
+
   ❲❳⤙⤚-●ᶠ-◆-pull-apartʳ : ∀ x y z → (❲ F.● ❳⤙ z ⤚ ❲ x ❳⤙ ◆ ⤚ y) ≈ ❲ x ❳⤙ z ⤚ y
   ❲❳⤙⤚-●ᶠ-◆-pull-apartʳ x y z = begin
     ❲ F.● ❳⤙ z ⤚ ❲ x ❳⤙ ◆ ⤚ y ≈⟨ ❲❳⤙⤚-◆ᶠ-◆-outer-associate F.● x y z ⟨
@@ -35,6 +41,12 @@ module RightProperties {f fℓ x xℓ} (F : Fumula f fℓ) (X : RightFumulaExtru
   open Setoid setoid using (refl)
   open SetoidReasoning setoid
 
+  ⤙⤚❲❳-●ᶠ-◆-collapse-sideʳ : ∀ x → (x ⤙ ◆ ⤚❲ F.● ❳) ≈ x
+  ⤙⤚❲❳-●ᶠ-◆-collapse-sideʳ x = begin
+    x ⤙ ◆ ⤚❲ F.● ❳ ≈⟨ ⤙⤚❲❳-●ᶠ-inner-commuteₗ x ◆ ⟩
+    ◆ ⤙ x ⤚❲ F.● ❳ ≈⟨ ⤙⤚❲❳-◆-collapse-middleˡ F.● x ⟩
+    x ∎
+
   ⤙⤚❲❳-●ᶠ-◆-pull-apartˡ : ∀ x y z → (x ⤙ ◆ ⤚❲ y ❳ ⤙ z ⤚❲ F.● ❳) ≈ x ⤙ z ⤚❲ y ❳
   ⤙⤚❲❳-●ᶠ-◆-pull-apartˡ x y z = begin
     x ⤙ ◆ ⤚❲ y ❳ ⤙ z ⤚❲ F.● ❳ ≈⟨ ⤙⤚❲❳-◆ᶠ-◆-outer-associate x y F.● z ⟩

diff --git a/src/Algebra/Fumula/Extrusion/Structures.agda b/src/Algebra/Fumula/Extrusion/Structures.agda
@@ -126,7 +126,6 @@ module _ (F : Fumula f ℓf) (_≈_ : Rel {x} X ℓx)
       ❲❳⤙⤚-■ᶠ-collapse-dupʳ : ∀ x → (❲ F.■ ❳⤙ x ⤚ x) ≈ ◆
       ❲❳⤙⤚-◆ᶠ-collapse-middleˡ : ∀ x z → (❲ F.◆ ❳⤙ z ⤚ x) ≈ z
       ❲❳⤙⤚-◆-collapse-middleʳ : ∀ x z → (❲ x ❳⤙ z ⤚ ◆) ≈ z
-      ❲❳⤙⤚-●ᶠ-◆-collapse-sideˡ : ∀ x → (❲ F.● ❳⤙ ◆ ⤚ x) ≈ x
       ❲❳⤙⤚-◆ᶠ-◆-outer-associate : OuterAssociativeWith F._⤙_⤚_ F.◆ ◆
 
     open IsLeftAlmostFumulaExtrusion ❲❳⤙⤚-isLeftAlmostFumulaExtrusion public
@@ -147,7 +146,6 @@ module _ (F : Fumula f ℓf) (_≈_ : Rel {x} X ℓx)
       ⤙⤚❲❳-■ᶠ-collapse-dupˡ : ∀ x → (x ⤙ x ⤚❲ F.■ ❳) ≈ ◆
       ⤙⤚❲❳-◆-collapse-middleˡ : ∀ x z → (◆ ⤙ z ⤚❲ x ❳) ≈ z
       ⤙⤚❲❳-◆ᶠ-collapse-middleʳ : ∀ x z → (x ⤙ z ⤚❲ F.◆ ❳) ≈ z
-      ⤙⤚❲❳-●ᶠ-◆-collapse-sideʳ : ∀ x → (x ⤙ ◆ ⤚❲ F.● ❳) ≈ x
       ⤙⤚❲❳-◆ᶠ-◆-outer-associate : OuterAssociativeWith F._⤙_⤚_ F.◆ ◆
 
     open IsRightAlmostFumulaExtrusion ⤙⤚❲❳-isRightAlmostFumulaExtrusion public
@@ -174,15 +172,13 @@ module _ (Fₗ : Fumula fₗ ℓfₗ) (Fᵣ : Fumula fᵣ ℓfᵣ) (_≈_ : Rel
       ❲❳⤙⤚-■ᶠ-collapse-dupʳ : ∀ x → (❲ Fₗ.■ ❳⤙ x ⤚ x) ≈ ◆
       ❲❳⤙⤚-◆ᶠ-collapse-middleˡ : ∀ x z → (❲ Fₗ.◆ ❳⤙ z ⤚ x) ≈ z
       ❲❳⤙⤚-◆-collapse-middleʳ : ∀ x z → (❲ x ❳⤙ z ⤚ ◆) ≈ z
-      ❲❳⤙⤚-●ᶠ-◆-collapse-sideˡ : ∀ x → (❲ Fₗ.● ❳⤙ ◆ ⤚ x) ≈ x
       ❲❳⤙⤚-◆ᶠ-◆-outer-associate : L.OuterAssociativeWith Fₗ._⤙_⤚_ Fₗ.◆ ◆
       ⤙⤚❲❳-●ᶠ-inner-commuteₗ : R.LeftInnerCommutativeWith Fᵣ.●
       ⤙⤚❲❳-◆-pulloutₗ : R.LeftPulloutWith ◆
       ⤙⤚❲❳-◆ᶠ-pulloutᵣ : R.RightPulloutWith Fᵣ._⤙_⤚_ Fᵣ.◆
       ⤙⤚❲❳-■ᶠ-collapse-dupˡ : ∀ x → (x ⤙ x ⤚❲ Fᵣ.■ ❳) ≈ ◆
       ⤙⤚❲❳-◆-collapse-middleˡ : ∀ x z → (◆ ⤙ z ⤚❲ x ❳) ≈ z
       ⤙⤚❲❳-◆ᶠ-collapse-middleʳ : ∀ x z → (x ⤙ z ⤚❲ Fᵣ.◆ ❳) ≈ z
-      ⤙⤚❲❳-●ᶠ-◆-collapse-sideʳ : ∀ x → (x ⤙ ◆ ⤚❲ Fᵣ.● ❳) ≈ x
       ⤙⤚❲❳-◆ᶠ-◆-outer-associate : R.OuterAssociativeWith Fᵣ._⤙_⤚_ Fᵣ.◆ ◆
       ◆-outer-associate : OuterAssociativeWith ◆
 
@@ -200,7 +196,6 @@ module _ (Fₗ : Fumula fₗ ℓfₗ) (Fᵣ : Fumula fᵣ ℓfᵣ) (_≈_ : Rel
       ; ❲❳⤙⤚-■ᶠ-collapse-dupʳ = ❲❳⤙⤚-■ᶠ-collapse-dupʳ
       ; ❲❳⤙⤚-◆ᶠ-collapse-middleˡ = ❲❳⤙⤚-◆ᶠ-collapse-middleˡ
       ; ❲❳⤙⤚-◆-collapse-middleʳ = ❲❳⤙⤚-◆-collapse-middleʳ
-      ; ❲❳⤙⤚-●ᶠ-◆-collapse-sideˡ = ❲❳⤙⤚-●ᶠ-◆-collapse-sideˡ
       ; ❲❳⤙⤚-◆ᶠ-◆-outer-associate = ❲❳⤙⤚-◆ᶠ-◆-outer-associate
       }
 
@@ -213,7 +208,6 @@ module _ (Fₗ : Fumula fₗ ℓfₗ) (Fᵣ : Fumula fᵣ ℓfᵣ) (_≈_ : Rel
       ; ⤙⤚❲❳-■ᶠ-collapse-dupˡ = ⤙⤚❲❳-■ᶠ-collapse-dupˡ
       ; ⤙⤚❲❳-◆-collapse-middleˡ = ⤙⤚❲❳-◆-collapse-middleˡ
       ; ⤙⤚❲❳-◆ᶠ-collapse-middleʳ = ⤙⤚❲❳-◆ᶠ-collapse-middleʳ
-      ; ⤙⤚❲❳-●ᶠ-◆-collapse-sideʳ = ⤙⤚❲❳-●ᶠ-◆-collapse-sideʳ
       ; ⤙⤚❲❳-◆ᶠ-◆-outer-associate = ⤙⤚❲❳-◆ᶠ-◆-outer-associate
       }