diff --git a/src/Algebra/Fumula/Extrusion/Bundles.agda b/src/Algebra/Fumula/Extrusion/Bundles.agda
index 847cbed..366b248 100644
--- a/src/Algebra/Fumula/Extrusion/Bundles.agda
+++ b/src/Algebra/Fumula/Extrusion/Bundles.agda
@@ -53,7 +53,7 @@ module _ (Fₗ : AlmostFumula fₗ ℓfₗ) (Fᵣ : AlmostFumula fᵣ ℓfᵣ) w
     module Fₗ = AlmostFumula Fₗ
     module Fᵣ = AlmostFumula Fᵣ
 
-  record BiAlmostFumulaExtrusion (x ℓx : Level) : Set (fₗ ⊔ fᵣ ⊔ suc x ⊔ ℓfₗ ⊔ ℓfᵣ ⊔ suc ℓx) where
+  record DoubleAlmostFumulaExtrusion (x ℓx : Level) : Set (fₗ ⊔ fᵣ ⊔ suc x ⊔ ℓfₗ ⊔ ℓfᵣ ⊔ suc ℓx) where
     infix 7 ❲_❳⤙_⤚_
     infix 7 _⤙_⤚❲_❳
     infix 4 _≈_
@@ -62,8 +62,8 @@ module _ (Fₗ : AlmostFumula fₗ ℓfₗ) (Fᵣ : AlmostFumula fᵣ ℓfᵣ) w
       _≈_ : Rel Carrier ℓx
       ❲_❳⤙_⤚_ : Op₃ₗ Fₗ.Carrier Carrier
       _⤙_⤚❲_❳ : Op₃ᵣ Fᵣ.Carrier Carrier
-      isBiAlmostFumulaExtrusion : IsBiAlmostFumulaExtrusion Fₗ Fᵣ _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳
-    open IsBiAlmostFumulaExtrusion isBiAlmostFumulaExtrusion public
+      isDoubleAlmostFumulaExtrusion : IsDoubleAlmostFumulaExtrusion Fₗ Fᵣ _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳
+    open IsDoubleAlmostFumulaExtrusion isDoubleAlmostFumulaExtrusion public
 
     ❲❳⤙⤚-leftAlmostFumulaExtrusion : LeftAlmostFumulaExtrusion Fₗ x ℓx
     ❲❳⤙⤚-leftAlmostFumulaExtrusion = record { isLeftAlmostFumulaExtrusion = ❲❳⤙⤚-isLeftAlmostFumulaExtrusion }
@@ -89,9 +89,9 @@ module _ (F : ReversibleAlmostFumula f ℓf) where
       isAlmostFumulaExtrusion : IsAlmostFumulaExtrusion F _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳
     open IsAlmostFumulaExtrusion isAlmostFumulaExtrusion public
 
-    biAlmostFumulaExtrusion : BiAlmostFumulaExtrusion F.almostFumula F.almostFumula x ℓx
-    biAlmostFumulaExtrusion = record { isBiAlmostFumulaExtrusion = isBiAlmostFumulaExtrusion }
-    open BiAlmostFumulaExtrusion biAlmostFumulaExtrusion public
+    doubleAlmostFumulaExtrusion : DoubleAlmostFumulaExtrusion F.almostFumula F.almostFumula x ℓx
+    doubleAlmostFumulaExtrusion = record { isDoubleAlmostFumulaExtrusion = isDoubleAlmostFumulaExtrusion }
+    open DoubleAlmostFumulaExtrusion doubleAlmostFumulaExtrusion public
       using (❲❳⤙⤚-leftAlmostFumulaExtrusion; ⤙⤚❲❳-rightAlmostFumulaExtrusion; setoid)
 
   record ReversibleAlmostFumulaExtrusion (x ℓx : Level) : Set (f ⊔ suc x ⊔ ℓf ⊔ suc ℓx) where
@@ -110,7 +110,7 @@ module _ (F : ReversibleAlmostFumula f ℓf) where
     almostFumulaExtrusion = record { isAlmostFumulaExtrusion = isAlmostFumulaExtrusion }
     open AlmostFumulaExtrusion almostFumulaExtrusion public
       using (❲❳⤙⤚-leftAlmostFumulaExtrusion; ⤙⤚❲❳-rightAlmostFumulaExtrusion;
-             biAlmostFumulaExtrusion)
+             doubleAlmostFumulaExtrusion)
 
 module _ (F : Fumula f ℓf) where
   private
@@ -153,7 +153,7 @@ module _ (Fₗ : Fumula fₗ ℓfₗ) (Fᵣ : Fumula fᵣ ℓfᵣ) where
     module Fₗ = Fumula Fₗ
     module Fᵣ = Fumula Fᵣ
 
-  record BiFumulaExtrusion (x ℓx : Level) : Set (fₗ ⊔ fᵣ ⊔ suc x ⊔ ℓfₗ ⊔ ℓfᵣ ⊔ suc ℓx) where
+  record DoubleFumulaExtrusion (x ℓx : Level) : Set (fₗ ⊔ fᵣ ⊔ suc x ⊔ ℓfₗ ⊔ ℓfᵣ ⊔ suc ℓx) where
     infix 7 ❲_❳⤙_⤚_
     infix 7 _⤙_⤚❲_❳
     infix 4 _≈_
@@ -163,8 +163,8 @@ module _ (Fₗ : Fumula fₗ ℓfₗ) (Fᵣ : Fumula fᵣ ℓfᵣ) where
       ❲_❳⤙_⤚_ : Op₃ₗ Fₗ.Carrier Carrier
       _⤙_⤚❲_❳ : Op₃ᵣ Fᵣ.Carrier Carrier
       ◆ : Carrier
-      isBiFumulaExtrusion : IsBiFumulaExtrusion Fₗ Fᵣ _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳ ◆
-    open IsBiFumulaExtrusion isBiFumulaExtrusion public
+      isDoubleFumulaExtrusion : IsDoubleFumulaExtrusion Fₗ Fᵣ _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳ ◆
+    open IsDoubleFumulaExtrusion isDoubleFumulaExtrusion public
 
     ❲❳⤙⤚-leftFumulaExtrusion : LeftFumulaExtrusion Fₗ x ℓx
     ❲❳⤙⤚-leftFumulaExtrusion = record { isLeftFumulaExtrusion = ❲❳⤙⤚-isLeftFumulaExtrusion }
@@ -176,8 +176,8 @@ module _ (Fₗ : Fumula fₗ ℓfₗ) (Fᵣ : Fumula fᵣ ℓfᵣ) where
     open RightFumulaExtrusion ⤙⤚❲❳-rightFumulaExtrusion public
       using (⤙⤚❲❳-rightAlmostFumulaExtrusion)
 
-    biAlmostFumulaExtrusion : BiAlmostFumulaExtrusion Fₗ.almostFumula Fᵣ.almostFumula x ℓx
-    biAlmostFumulaExtrusion = record { isBiAlmostFumulaExtrusion = isBiAlmostFumulaExtrusion }
+    doubleAlmostFumulaExtrusion : DoubleAlmostFumulaExtrusion Fₗ.almostFumula Fᵣ.almostFumula x ℓx
+    doubleAlmostFumulaExtrusion = record { isDoubleAlmostFumulaExtrusion = isDoubleAlmostFumulaExtrusion }
 
 module _ (F : ReversibleFumula f ℓf) where
   private
@@ -196,12 +196,12 @@ module _ (F : ReversibleFumula f ℓf) where
       isFumulaExtrusion : IsFumulaExtrusion F _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳ ◆
     open IsFumulaExtrusion isFumulaExtrusion public
 
-    biFumulaExtrusion : BiFumulaExtrusion F.fumula F.fumula x ℓx
-    biFumulaExtrusion = record { isBiFumulaExtrusion = isBiFumulaExtrusion }
-    open BiFumulaExtrusion biFumulaExtrusion public
+    doubleFumulaExtrusion : DoubleFumulaExtrusion F.fumula F.fumula x ℓx
+    doubleFumulaExtrusion = record { isDoubleFumulaExtrusion = isDoubleFumulaExtrusion }
+    open DoubleFumulaExtrusion doubleFumulaExtrusion public
       using (❲❳⤙⤚-leftFumulaExtrusion; ⤙⤚❲❳-rightFumulaExtrusion;
              ❲❳⤙⤚-leftAlmostFumulaExtrusion; ⤙⤚❲❳-rightAlmostFumulaExtrusion;
-             biAlmostFumulaExtrusion)
+             doubleAlmostFumulaExtrusion)
 
     almostFumulaExtrusion : AlmostFumulaExtrusion F.reversibleAlmostFumula x ℓx
     almostFumulaExtrusion = record { isAlmostFumulaExtrusion = isAlmostFumulaExtrusion }
@@ -224,4 +224,4 @@ module _ (F : ReversibleFumula f ℓf) where
     open FumulaExtrusion fumulaExtrusion public
       using (❲❳⤙⤚-leftFumulaExtrusion; ⤙⤚❲❳-rightFumulaExtrusion;
              ❲❳⤙⤚-leftAlmostFumulaExtrusion; ⤙⤚❲❳-rightAlmostFumulaExtrusion;
-             biFumulaExtrusion; biAlmostFumulaExtrusion; almostFumulaExtrusion)
+             doubleFumulaExtrusion; doubleAlmostFumulaExtrusion; almostFumulaExtrusion)
diff --git a/src/Algebra/Fumula/Extrusion/Convert.agda b/src/Algebra/Fumula/Extrusion/Convert.agda
index d4dab49..f4e567a 100644
--- a/src/Algebra/Fumula/Extrusion/Convert.agda
+++ b/src/Algebra/Fumula/Extrusion/Convert.agda
@@ -208,6 +208,41 @@ module FromModule where
     rightFumulaExtrusion M = record { isRightFumulaExtrusion = isRightFumulaExtrusion R _≈ᴹ_ _+ᴹ_ 0ᴹ -ᴹ_ _*ᵣ_ isRightModule }
       where open RightModule M
 
+  module _ {rₗ rᵣ m rℓₗ rℓᵣ mℓ} (Rₗ : Ring rₗ rℓₗ) (Rᵣ : Ring rᵣ rℓᵣ) {Carrier : Set m} (_≈_ : Rel Carrier mℓ)
+           (_+_ : Op₂ Carrier) (0# : Carrier) (-_ : Op₁ Carrier)
+           (_*ₗ_ : Opₗ (Ring.Carrier Rₗ) Carrier) (_*ᵣ_ : Opᵣ (Ring.Carrier Rᵣ) Carrier) where
+    private
+      Fₗ : Fumula rₗ rℓₗ
+      Fₗ = FromRing.fumula Rₗ
+      module Rₗ where
+        open Ring Rₗ public
+        open RingProperties Rₗ public
+        open RingHelpers Rₗ public
+      module Fₗ where
+        open Fumula Fₗ public
+        open FumulaProperties Fₗ public
+      Fᵣ : Fumula rᵣ rℓᵣ
+      Fᵣ = FromRing.fumula Rᵣ
+      module Rᵣ where
+        open Ring Rᵣ public
+        open RingProperties Rᵣ public
+        open RingHelpers Rᵣ public
+      module Fᵣ where
+        open Fumula Fᵣ public
+        open FumulaProperties Fᵣ public
+
+      ❲_❳⤙_⤚_ : Op₃ₗ Fₗ.Carrier Carrier
+      ❲ s ❳⤙ z ⤚ x = (s *ₗ x) + z
+
+      _⤙_⤚❲_❳ : Op₃ᵣ Fᵣ.Carrier Carrier
+      x ⤙ z ⤚❲ s ❳ = (x *ᵣ s) + z
+
+      ◆ : Carrier
+      ◆ = 0#
+
+      isDoubleFumulaExtrusion : IsBimodule Rₗ Rᵣ _≈_ _+_ 0# -_ _*ₗ_ _*ᵣ_ → {!!}
+      isDoubleFumulaExtrusion = {!!}
+
 module FromFumulaExtrusion where
 
   module _ {f x fℓ xℓ} (F : Fumula f fℓ) {Carrier : Set x} (_≈_ : Rel Carrier xℓ)
diff --git a/src/Algebra/Fumula/Extrusion/Structures.agda b/src/Algebra/Fumula/Extrusion/Structures.agda
index b7ed821..e97badb 100644
--- a/src/Algebra/Fumula/Extrusion/Structures.agda
+++ b/src/Algebra/Fumula/Extrusion/Structures.agda
@@ -58,7 +58,7 @@ module _ (Fₗ : AlmostFumula fₗ ℓfₗ) (Fᵣ : AlmostFumula fᵣ ℓfᵣ) (
     module Fₗ = AlmostFumula Fₗ
     module Fᵣ = AlmostFumula Fᵣ
 
-  record IsBiAlmostFumulaExtrusion : Set (fₗ ⊔ fᵣ ⊔ x ⊔ ℓfₗ ⊔ ℓfᵣ ⊔ ℓx) where
+  record IsDoubleAlmostFumulaExtrusion : Set (fₗ ⊔ fᵣ ⊔ x ⊔ ℓfₗ ⊔ ℓfᵣ ⊔ ℓx) where
     private
       module L = LeftDefs ❲_❳⤙_⤚_ _≈_
       module R = RightDefs _⤙_⤚❲_❳ _≈_
@@ -97,9 +97,9 @@ module _ (F : ReversibleAlmostFumula f ℓf) (_≈_ : Rel {x} X ℓx)
 
   record IsAlmostFumulaExtrusion : Set (f ⊔ x ⊔ ℓf ⊔ ℓx) where
     field
-      isBiAlmostFumulaExtrusion : IsBiAlmostFumulaExtrusion F.almostFumula F.almostFumula _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳
+      isDoubleAlmostFumulaExtrusion : IsDoubleAlmostFumulaExtrusion F.almostFumula F.almostFumula _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳
 
-    open IsBiAlmostFumulaExtrusion isBiAlmostFumulaExtrusion public
+    open IsDoubleAlmostFumulaExtrusion isDoubleAlmostFumulaExtrusion public
 
   record IsReversibleAlmostFumulaExtrusion : Set (f ⊔ x ⊔ ℓf ⊔ ℓx) where
     open SimultaneousBiDefs ❲_❳⤙_⤚_ _⤙_⤚❲_❳ _≈_
@@ -160,14 +160,14 @@ module _ (Fₗ : Fumula fₗ ℓfₗ) (Fᵣ : Fumula fᵣ ℓfᵣ) (_≈_ : Rel
     module Fₗ = Fumula Fₗ
     module Fᵣ = Fumula Fᵣ
 
-  record IsBiFumulaExtrusion : Set (fₗ ⊔ fᵣ ⊔ x ⊔ ℓfₗ ⊔ ℓfᵣ ⊔ ℓx) where
+  record IsDoubleFumulaExtrusion : Set (fₗ ⊔ fᵣ ⊔ x ⊔ ℓfₗ ⊔ ℓfᵣ ⊔ ℓx) where
     private
       module L = LeftDefs ❲_❳⤙_⤚_ _≈_
       module R = RightDefs _⤙_⤚❲_❳ _≈_
     open BiDefs ❲_❳⤙_⤚_ _⤙_⤚❲_❳ _≈_
 
     field
-      isBiAlmostFumulaExtrusion : IsBiAlmostFumulaExtrusion Fₗ.almostFumula Fᵣ.almostFumula _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳
+      isDoubleAlmostFumulaExtrusion : IsDoubleAlmostFumulaExtrusion Fₗ.almostFumula Fᵣ.almostFumula _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳
       ❲❳⤙⤚-●ᶠ-inner-commuteᵣ : L.RightInnerCommutativeWith Fₗ.●
       ❲❳⤙⤚-◆ᶠ-pulloutₗ : L.LeftPulloutWith Fₗ._⤙_⤚_ Fₗ.◆
       ❲❳⤙⤚-◆-pulloutᵣ : L.RightPulloutWith ◆
@@ -186,7 +186,7 @@ module _ (Fₗ : Fumula fₗ ℓfₗ) (Fᵣ : Fumula fᵣ ℓfᵣ) (_≈_ : Rel
       ⤙⤚❲❳-◆ᶠ-◆-outer-associate : R.OuterAssociativeWith Fᵣ._⤙_⤚_ Fᵣ.◆ ◆
       ◆-outer-associate : OuterAssociativeWith ◆
 
-    open IsBiAlmostFumulaExtrusion isBiAlmostFumulaExtrusion public
+    open IsDoubleAlmostFumulaExtrusion isDoubleAlmostFumulaExtrusion public
 
     ◆-pullout : PulloutWith ◆
     ◆-pullout = ⤙⤚❲❳-◆-pulloutₗ , ❲❳⤙⤚-◆-pulloutᵣ
@@ -228,13 +228,13 @@ module _ (F : ReversibleFumula f ℓf) (_≈_ : Rel {x} X ℓx)
     open SimultaneousBiDefs ❲_❳⤙_⤚_ _⤙_⤚❲_❳ _≈_
 
     field
-      isBiFumulaExtrusion : IsBiFumulaExtrusion F.fumula F.fumula _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳ ◆
+      isDoubleFumulaExtrusion : IsDoubleFumulaExtrusion F.fumula F.fumula _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳ ◆
       ■ᶠ-outer-commute : OuterCommutativeWithUnderlying F.■
       ◆ᶠ-outer-commute : OuterCommutativeWithUnderlying F.◆
       ●ᶠ-outer-commute : OuterCommutativeWithUnderlying F.●
       ◆-outer-commute : OuterCommutativeWith ◆
 
-    open IsBiFumulaExtrusion isBiFumulaExtrusion public
+    open IsDoubleFumulaExtrusion isDoubleFumulaExtrusion public
 
     ●ᶠ-inner-commute : InnerCommutativeWith F.●
     ●ᶠ-inner-commute = ⤙⤚❲❳-●ᶠ-inner-commuteₗ , ❲❳⤙⤚-●ᶠ-inner-commuteᵣ
@@ -243,7 +243,7 @@ module _ (F : ReversibleFumula f ℓf) (_≈_ : Rel {x} X ℓx)
     ◆ᶠ-pullout = ❲❳⤙⤚-◆ᶠ-pulloutₗ , ⤙⤚❲❳-◆ᶠ-pulloutᵣ
 
     isAlmostFumulaExtrusion : IsAlmostFumulaExtrusion F.reversibleAlmostFumula _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳
-    isAlmostFumulaExtrusion = record { isBiAlmostFumulaExtrusion = isBiAlmostFumulaExtrusion }
+    isAlmostFumulaExtrusion = record { isDoubleAlmostFumulaExtrusion = isDoubleAlmostFumulaExtrusion }
 
   record IsReversibleFumulaExtrusion : Set (f ⊔ x ⊔ ℓf ⊔ ℓx) where
     open SimultaneousBiDefs ❲_❳⤙_⤚_ _⤙_⤚❲_❳ _≈_