Right extrusion conversions complete

pthariensflame · May 5, 2024 · 55e1d9d · 55e1d9d
1 parent 420bf2a
commit 55e1d9d
Showing 1 changed file with 4 additions and 13 deletions.
diff --git a/src/Algebra/Fumula/Extrusion/Convert.agda b/src/Algebra/Fumula/Extrusion/Convert.agda
@@ -337,19 +337,10 @@ module FromFumulaExtrusion where
           ; *ᵣ-assoc = λ x s r → ⤙⤚❲❳-◆ᶠ-◆-outer-associate x s r ◆
           ; *ᵣ-zeroˡ = λ x → ⤙⤚❲❳-◆-collapse-middleˡ x ◆
           ; *ᵣ-distribʳ = λ s x y → begin
-            x ⤙ y ⤚❲ F.● ❳ ⤙ ◆ ⤚❲ s ❳ ≈⟨ {!!} ⟩
-            {!!} ≈⟨ {!!} ⟩
-            {!!} ≈⟨ {!!} ⟩
-            {!!} ≈⟨ {!!} ⟩
-            {!!} ≈⟨ {!!} ⟩
-            {!!} ≈⟨ {!!} ⟩
-            {!!} ≈⟨ {!!} ⟩
-            {!!} ≈⟨ {!!} ⟩
-            {!!} ≈⟨ {!!} ⟩
-            {!!} ≈⟨ {!!} ⟩
-            {!!} ≈⟨ {!!} ⟩
-            {!!} ≈⟨ {!!} ⟩
-            {!!} ≈⟨ {!!} ⟩
+            x ⤙ y ⤚❲ F.● ❳ ⤙ ◆ ⤚❲ s ❳ ≈⟨ ⤙⤚❲❳-◆-pulloutₗ y x F.● s ◆ ⟩
+            x ⤙ ◆ ⤚❲ F.● ❳ ⤙ y ⤙ ◆ ⤚❲ s ❳ ⤚❲ s ❳ ≈⟨ ⤙⤚❲❳-cong (⤙⤚❲❳-●ᶠ-◆-collapse-sideʳ x) (sym (⤙⤚❲❳-●ᶠ-◆-collapse-sideʳ (y ⤙ ◆ ⤚❲ s ❳))) F.refl ⟩
+            x ⤙ y ⤙ ◆ ⤚❲ s ❳ ⤙ ◆ ⤚❲ F.● ❳ ⤚❲ s ❳ ≈⟨ ⤙⤚❲❳-double-exchange x s (y ⤙ ◆ ⤚❲ s ❳) F.● ◆ ⟩
+            ((y ⤙ ◆ ⤚❲ s ❳) ⤙ x ⤙ ◆ ⤚❲ s ❳ ⤚❲ F.● ❳) ≈⟨ ⤙⤚❲❳-●ᶠ-inner-commuteₗ (y ⤙ ◆ ⤚❲ s ❳) (x ⤙ ◆ ⤚❲ s ❳) ⟩
             x ⤙ ◆ ⤚❲ s ❳ ⤙ y ⤙ ◆ ⤚❲ s ❳ ⤚❲ F.● ❳ ∎
           }
         }