❲❳⤙⤚-⤙⤚❲❳-double-exchange (for real)

pthariensflame · Jun 6, 2024 · c74c607 · c74c607
1 parent 1ae11d9
commit c74c607
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 4 deletions.
diff --git a/src/Algebra/Fumula/Extrusion/Construct.agda b/src/Algebra/Fumula/Extrusion/Construct.agda
@@ -184,6 +184,7 @@ module Initial {x xℓ} where
         ; ❲❳⤙⤚-double-exchange = λ _ ()
         ; ⤙⤚❲❳-cong = ⤙⤚❲❳-cong (AlmostFumula._≈_ Fᵣ)
         ; ⤙⤚❲❳-double-exchange = λ ()
+        ; ❲❳⤙⤚-⤙⤚❲❳-double-exchange = λ _ ()
         }
       }
     open DoubleAlmostFumulaExtrusion doubleAlmostFumulaExtrusion public
@@ -285,6 +286,8 @@ module DirectProduct {x₁ xℓ₁ x₂ xℓ₂} where
         ; ⤙⤚❲❳-cong = λ (x₁≈ , x₂≈) (z₁≈ , z₂≈) s≈ → X₁.⤙⤚❲❳-cong x₁≈ z₁≈ s≈ , X₂.⤙⤚❲❳-cong x₂≈ z₂≈ s≈
         ; ⤙⤚❲❳-double-exchange = λ (v₁ , v₂) w (x₁ , x₂) y (z₁ , z₂) →
           X₁.⤙⤚❲❳-double-exchange v₁ w x₁ y z₁ , X₂.⤙⤚❲❳-double-exchange v₂ w x₂ y z₂
+        ; ❲❳⤙⤚-⤙⤚❲❳-double-exchange = λ v (w₁ , w₂) (x₁ , x₂) y (z₁ , z₂) →
+          X₁.❲❳⤙⤚-⤙⤚❲❳-double-exchange v w₁ x₁ y z₁ , X₂.❲❳⤙⤚-⤙⤚❲❳-double-exchange v w₂ x₂ y z₂
         }
       }
     open DoubleAlmostFumulaExtrusion doubleAlmostFumulaExtrusion public
@@ -479,6 +482,7 @@ module TensorUnit {f fℓ} where
         ; ❲❳⤙⤚-double-exchange = F.double-exchange
         ; ⤙⤚❲❳-cong = F.⤙⤚-cong
         ; ⤙⤚❲❳-double-exchange = F.double-exchange
+        ; ❲❳⤙⤚-⤙⤚❲❳-double-exchange = F.double-exchange
         }
       }
     open DoubleAlmostFumulaExtrusion doubleAlmostFumulaExtrusion public

diff --git a/src/Algebra/Fumula/Extrusion/Convert.agda b/src/Algebra/Fumula/Extrusion/Convert.agda
@@ -238,6 +238,11 @@ module FromModule where
         ; ❲❳⤙⤚-double-exchange = ❲❳⤙⤚-double-exchange
         ; ⤙⤚❲❳-cong = ⤙⤚❲❳-cong
         ; ⤙⤚❲❳-double-exchange = ⤙⤚❲❳-double-exchange
+        ; ❲❳⤙⤚-⤙⤚❲❳-double-exchange = λ v w x y z → begin
+          (v *ₗ w) + ((x *ᵣ y) + z) ≈⟨ +ᴹ-assoc (v *ₗ w) (x *ᵣ y) z ⟨
+          ((v *ₗ w) + (x *ᵣ y)) + z ≈⟨ +ᴹ-congʳ (+ᴹ-comm (v *ₗ w) (x *ᵣ y)) ⟩
+          ((x *ᵣ y) + (v *ₗ w)) + z ≈⟨ +ᴹ-assoc (x *ᵣ y) (v *ₗ w) z ⟩
+          (x *ᵣ y) + ((v *ₗ w) + z) ∎
         }
       ; ❲❳⤙⤚-●ᶠ-inner-commuteʳ = ❲❳⤙⤚-●ᶠ-inner-commuteʳ
       ; ❲❳⤙⤚-◆ᶠ-pulloutˡ = ❲❳⤙⤚-◆ᶠ-pulloutˡ

diff --git a/src/Algebra/Fumula/Extrusion/Definitions.agda b/src/Algebra/Fumula/Extrusion/Definitions.agda
@@ -57,7 +57,7 @@ module BiDefs {aₗ aᵣ b ℓb} {Aₗ : Set aₗ} {Aᵣ : Set aᵣ} {B : Set b}
     module R = RightDefs _⤙_⤚❲_❳ _≈ᵇ_
 
   MiddleNestedDoubleExchange : Set _
-  MiddleNestedDoubleExchange = L.MiddleNestedDoubleExchange × R.MiddleNestedDoubleExchange
+  MiddleNestedDoubleExchange = ∀ v w x y z → (❲ v ❳⤙ x ⤙ z ⤚❲ y ❳ ⤚ w) ≈ᵇ (x ⤙ ❲ v ❳⤙ z ⤚ w ⤚❲ y ❳)
 
   OuterAssociativeWith : B → Set _
   OuterAssociativeWith e = ∀ w x y z → ((❲ w ❳⤙ e ⤚ x) ⤙ z ⤚❲ y ❳) ≈ᵇ (❲ w ❳⤙ z ⤚ (x ⤙ e ⤚❲ y ❳))

diff --git a/src/Algebra/Fumula/Extrusion/Structures.agda b/src/Algebra/Fumula/Extrusion/Structures.agda
@@ -70,6 +70,7 @@ module _ (Fₗ : AlmostFumula fₗ ℓfₗ) (Fᵣ : AlmostFumula fᵣ ℓfᵣ) (
       ❲❳⤙⤚-double-exchange : L.MiddleNestedDoubleExchange
       ⤙⤚❲❳-cong : R.Congruent₃ Fᵣ._≈_
       ⤙⤚❲❳-double-exchange : R.MiddleNestedDoubleExchange
+      ❲❳⤙⤚-⤙⤚❲❳-double-exchange : MiddleNestedDoubleExchange -- ought to be provable from other axioms, but whatever
 
     ❲❳⤙⤚-isLeftAlmostFumulaExtrusion : IsLeftAlmostFumulaExtrusion Fₗ _≈_ ❲_❳⤙_⤚_
     ❲❳⤙⤚-isLeftAlmostFumulaExtrusion = record
@@ -85,9 +86,6 @@ module _ (Fₗ : AlmostFumula fₗ ℓfₗ) (Fᵣ : AlmostFumula fᵣ ℓfᵣ) (
       ; ⤙⤚❲❳-double-exchange = ⤙⤚❲❳-double-exchange
       }
 
-    double-exchange : MiddleNestedDoubleExchange
-    double-exchange = ❲❳⤙⤚-double-exchange , ⤙⤚❲❳-double-exchange
-
 module _ (F : ReversibleAlmostFumula f ℓf) (_≈_ : Rel {x} X ℓx)
          (❲_❳⤙_⤚_ : Op₃ₗ (ReversibleAlmostFumula.Carrier F) X)
          (_⤙_⤚❲_❳ : Op₃ᵣ (ReversibleAlmostFumula.Carrier F) X)