diff --git a/src/Categories/Diagram/End/Fubini.agda b/src/Categories/Diagram/End/Fubini.agda
index 97c03feb..6f67e8ea 100644
--- a/src/Categories/Diagram/End/Fubini.agda
+++ b/src/Categories/Diagram/End/Fubini.agda
@@ -6,7 +6,7 @@ open import Level
 open import Data.Product using (Σ; _,_; _×_) renaming (proj₁ to fst; proj₂ to snd)
 open import Function using (_$_)
 
-open import Categories.Category using (Category)
+open import Categories.Category using (Category; _[_,_]; _[_∘_])
 open import Categories.Category.Construction.Functors using (Functors; curry)
 open import Categories.Category.Product using (πˡ; πʳ; _⁂_; _※_; Swap) renaming (Product to _×ᶜ_)
 open import Categories.Diagram.End using () renaming (End to ∫)
@@ -49,6 +49,8 @@ module _  (F : Bifunctor (Category.op C ×ᶜ Category.op P) (C ×ᶜ P) D)
     module C = Category C
     module P = Category P
     module D = Category D
+    C×P = (C ×ᶜ P)
+    module C×P = Category C×P
     open module F = Functor F using (F₀; F₁; F-resp-≈)
     ∫F = (⨏ (F ′) {ω})
     module ∫F = Functor ∫F
@@ -57,7 +59,7 @@ module _  (F : Bifunctor (Category.op C ×ᶜ Category.op P) (C ×ᶜ P) D)
 
   open _≅_
   open Iso
-  open DinaturalTransformation using (α)
+  open DinaturalTransformation
   open NaturalTransformation using (η)
   open Wedge renaming (E to apex)
   open Category D
@@ -71,47 +73,58 @@ module _  (F : Bifunctor (Category.op C ×ᶜ Category.op P) (C ×ᶜ P) D)
     -- first, our wedge gives us a wedge in the product
     ξ : Wedge F
     ξ .apex = x
-    ξ .dinatural = dtHelper record
-      { α = λ { (c , p) → ω.dinatural.α (p , p) c ∘ ρ.dinatural.α p }
-      ; commute = λ { {c , p} {d , q} (f , s) → begin
-          F₁ ((C.id , P.id) , (f , s)) ∘ (ω.dinatural.α (p , p) c ∘ ρ.dinatural.α p) ∘ id
+    ξ .dinatural .α (c , p) = ω.dinatural.α (p , p) c ∘ ρ.dinatural.α p
+    -- unfolded because dtHelper means opening up a record (i.e. no where clause)
+    ξ .dinatural .op-commute (f , s) = assoc ○ ⟺ (ξ .dinatural .commute (f , s)) ○ sym-assoc
+    ξ .dinatural .commute {c , p} {d , q} (f , s) = begin
+          F₁ (C×P.id , (f , s)) ∘ (ωp,p c ∘ ρp) ∘ id
             ≈⟨ refl⟩∘⟨ identityʳ ⟩
           -- First we show dinaturality in C, which is 'trivial'
-          F₁ ((C.id , P.id) , (f , s)) ∘ (ω.dinatural.α (p , p) c ∘ ρ.dinatural.α p)
-            ≈⟨ (F-resp-≈ ((C.Equiv.sym C.identity² , P.Equiv.sym P.identity²) , (C.Equiv.sym C.identityˡ , P.Equiv.sym P.identityʳ)) ○ F.homomorphism) ⟩∘⟨refl ○ pullˡ assoc ⟩
-          (F₁ ((C.id , P.id) , (C.id , s)) ∘ F₁ ((C.id , P.id) , (f , P.id)) ∘ ω.dinatural.α (p , p) c) ∘ ρ.dinatural.α p
+          F₁ (C×P.id , (f , s)) ∘ (ωp,p c ∘ ρp)
+            ≈⟨ F-resp-≈ ((C.Equiv.sym C.identity² , P.Equiv.sym P.identity²) , (C.Equiv.sym C.identityˡ , P.Equiv.sym P.identityʳ)) ⟩∘⟨refl ⟩
+          F₁ (C×P [ C×P.id ∘ C×P.id ] , C [ C.id ∘ f ] , P [ s ∘ P.id ]) ∘ (ωp,p c ∘ ρ.dinatural.α p)
+            ≈⟨ F.homomorphism ⟩∘⟨refl ⟩
+          (F₁ (C×P.id , (C.id , s)) ∘ F₁ (C×P.id , (f , P.id))) ∘ (ωp,p c ∘ ρp)
+            ≈⟨ assoc²γβ ⟩
+          (F₁ (C×P.id , (C.id , s)) ∘ F₁ (C×P.id , (f , P.id)) ∘ ωp,p c) ∘ ρp
             ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ ⟺ identityʳ) ⟩∘⟨refl ⟩
-          (F₁ ((C.id , P.id) , (C.id , s)) ∘ F₁ ((C.id , P.id) , (f , P.id)) ∘ ω.dinatural.α (p , p) c ∘ id) ∘ ρ.dinatural.α p
+          (F₁ (C×P.id , (C.id , s)) ∘ F₁ (C×P.id , (f , P.id)) ∘ ωp,p c ∘ id) ∘ ρp
             ≈⟨ (refl⟩∘⟨ ω.dinatural.commute (p , p) f) ⟩∘⟨refl ⟩
-          (F₁ ((C.id , P.id) , (C.id , s)) ∘ F₁ ((f , P.id) , (C.id , P.id)) ∘ ω.dinatural.α (p , p) d ∘ id) ∘ ρ.dinatural.α p
+          (F₁ (C×P.id , (C.id , s)) ∘ F₁ ((f , P.id) , C×P.id) ∘ ωp,p d ∘ id) ∘ ρp
             ≈⟨ extendʳ (⟺ F.homomorphism ○ F-resp-≈ ((MR.id-comm C , P.Equiv.refl) , (C.Equiv.refl , MR.id-comm P)) ○ F.homomorphism) ⟩∘⟨refl ⟩
           -- now, we must show dinaturality in P
-          -- First, some reassosiations to make things easier
-          (F₁ ((f , P.id) , (C.id , P.id)) ∘ F₁ ((C.id , P.id) , (C.id , s)) ∘ ω.dinatural.α (p , p) d ∘ id) ∘ ρ.dinatural.α p
-            ≈⟨ assoc ○ refl⟩∘⟨ assoc ○ refl⟩∘⟨ refl⟩∘⟨ identityʳ ⟩∘⟨refl ⟩
-          F₁ ((f , P.id) , (C.id , P.id)) ∘ (F₁ ((C.id , P.id) , (C.id , s)) ∘ ω.dinatural.α (p , p) d ∘ ρ.dinatural.α p)
+          -- First, we get rid of the identity and reassoc
+          (F₁ ((f , P.id) , C×P.id) ∘ F₁ (C×P.id , (C.id , s)) ∘ ωp,p d ∘ id) ∘ ρp
+            ≈⟨ assoc²βε ⟩
+          F₁ ((f , P.id) , C×P.id) ∘ F₁ (C×P.id , (C.id , s)) ∘ (ωp,p d ∘ id)  ∘ ρp
+            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ ⟩∘⟨refl ⟩
+          F₁ ((f , P.id) , C×P.id) ∘ F₁ (C×P.id , (C.id , s)) ∘ ωp,p d ∘ ρp
           -- this is the hard part: we use commutativity from the bottom face of the cube.
           -- The fact that this exists (an arrow between ∫ F (p,p,- ,-) to ∫ F (p,q,- ,-)) is due to functorality of ∫ and curry₀.
           -- The square commutes by universiality of ω
             ≈⟨ refl⟩∘⟨ extendʳ (⟺ (end-η-commute ⦃ ω (p , p) ⦄ ⦃ ω (p , q) ⦄ (curry.₀.₁ (F ′) (P.id , s)) d)) ⟩
           -- now we can use dinaturality in ρ, which annoyingly has an `id` tacked on the end
-          F₁ ((f , P.id) , (C.id , P.id)) ∘ ω.dinatural.α (p , q) d ∘ ∫F.F₁ (P.id , s) ∘ ρ.dinatural.α p
+          F₁ ((f , P.id) , C×P.id) ∘ ωp,q d ∘ ∫F.F₁ (P.id , s) ∘ ρp
             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨  ⟺ identityʳ ⟩
-          F₁ ((f , P.id) , (C.id , P.id)) ∘ ω.dinatural.α (p , q) d ∘ ∫F.F₁ (P.id , s) ∘ ρ.dinatural.α p ∘ id
+          F₁ ((f , P.id) , C×P.id) ∘ ωp,q d ∘ ∫F.F₁ (P.id , s) ∘ ρp ∘ id
             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ρ.dinatural.commute s ⟩
-          F₁ ((f , P.id) , (C.id , P.id)) ∘ ω.dinatural.α (p , q) d ∘ ∫F.F₁ (s , P.id) ∘ ρ.dinatural.α q ∘ id
+          F₁ ((f , P.id) , C×P.id) ∘ ωp,q d ∘ ∫F.F₁ (s , P.id) ∘ ρq ∘ id
             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ ⟩
-          F₁ ((f , P.id) , (C.id , P.id)) ∘ ω.dinatural.α (p , q) d ∘ ∫F.F₁ (s , P.id) ∘ ρ.dinatural.α q
+          F₁ ((f , P.id) , C×P.id) ∘ ωp,q d ∘ ∫F.F₁ (s , P.id) ∘ ρq
           -- and now we're done. step backward through the previous isomorphisms to get dinaturality in f and s together
             ≈⟨ refl⟩∘⟨ extendʳ (end-η-commute ⦃ ω (q , q) ⦄ ⦃ ω (p , q) ⦄ (curry.₀.₁ (F ′) (s , P.id)) d) ⟩
-          F₁ ((f , P.id) , (C.id , P.id)) ∘ (F₁ ((C.id , s) , (C.id , P.id)) ∘ ω.dinatural.α (q , q) d ∘ ρ.dinatural.α q)
+          F₁ ((f , P.id) , C×P.id) ∘ (F₁ ((C.id , s) , C×P.id) ∘ ωq,q d ∘ ρq)
             ≈⟨ pullˡ (⟺ F.homomorphism ○ F-resp-≈ ((C.identityˡ , P.identityʳ) , (C.identity² , P.identity²))) ⟩
-          F₁ ((f , s) , (C.id , P.id)) ∘ ω.dinatural.α (q , q) d ∘ ρ.dinatural.α q
+          F₁ ((f , s) , C×P.id) ∘ ωq,q d ∘ ρq
             ≈˘⟨ refl⟩∘⟨ identityʳ ⟩
-          F₁ ((f , s) , (C.id , P.id)) ∘ (ω.dinatural.α (q , q) d ∘ ρ.dinatural.α q) ∘ id
+          F₁ ((f , s) , C×P.id) ∘ (ωq,q d ∘ ρq) ∘ id
           ∎
-        }
-      }
+      where ωp,p = ω.dinatural.α (p , p)
+            ωp,q = ω.dinatural.α (p , q)
+            ωq,q = ω.dinatural.α (q , q)
+            ρp = ρ.dinatural.α p
+            ρq = ρ.dinatural.α q
+
 
   -- now the opposite direction
   private module _ (ξ : Wedge F) where
@@ -119,37 +132,41 @@ module _  (F : Bifunctor (Category.op C ×ᶜ Category.op P) (C ×ᶜ P) D)
       open module ξ = Wedge ξ using () renaming (E to x)
     ρ : Wedge ∫F
     ρ .apex = x
-    ρ .dinatural = dtHelper record
-      { α = λ p → ω.factor (p , p) record
+    ρ .dinatural .α p = ω.factor (p , p) record
         { E = x
         ; dinatural = dtHelper record
           { α = λ c → ξ.dinatural.α (c , p)
           ; commute = λ f → ξ.dinatural.commute (f , P.id)
           }
         }
-          -- end-η-commute ⦃ ω (?) ⦄ ⦃ ω (?) ⦄ (curry.₀.₁ (F ′) (?)) ?
-      ; commute = λ {p} {q} f → ω.unique′ (p , q) λ {c} → begin
-        ω.dinatural.α (p , q) c ∘ ∫F.₁ (P.id , f) ∘ ω.factor (p , p) _ ∘ id
+    ρ .dinatural .op-commute f = assoc ○ ⟺ (ρ .dinatural .commute f) ○ sym-assoc
+    ρ .dinatural .commute {p} {q} f = ω.unique′ (p , q) λ {c} → begin
+        ωp,q c ∘ ∫F.₁ (P.id , f) ∘ ρp ∘ id
           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ ⟩
-        ω.dinatural.α (p , q) c ∘ ∫F.₁ (P.id , f) ∘ ω.factor (p , p) _
+        ωp,q c ∘ ∫F.₁ (P.id , f) ∘ ρp
           ≈⟨ extendʳ $ end-η-commute ⦃ ω (p , p) ⦄ ⦃ ω (p , q) ⦄ (curry.₀.₁ (F ′) (P.id , f)) c ⟩
-        F₁ ((C.id , P.id) , (C.id , f)) ∘ ω.dinatural.α (p , p) c ∘ ∫.factor (ω (p , p)) _
+        F₁ (C×P.id , (C.id , f)) ∘ ωp,p c ∘ ρp
           ≈⟨ refl⟩∘⟨ ω.universal (p , p) ⟩
-        F₁ ((C.id , P.id) , (C.id , f)) ∘ ξ.dinatural.α (c , p)
+        F₁ (C×P.id , (C.id , f)) ∘ ξ.dinatural.α (c , p)
           ≈˘⟨ refl⟩∘⟨ identityʳ ⟩
-        F₁ ((C.id , P.id) , (C.id , f)) ∘ ξ.dinatural.α (c , p) ∘ id
+        F₁ (C×P.id , (C.id , f)) ∘ ξ.dinatural.α (c , p) ∘ id
           ≈⟨ ξ.dinatural.commute (C.id , f) ⟩
-        F₁ ((C.id , f) , (C.id , P.id)) ∘ ξ.dinatural.α (c , q) ∘ id
+        F₁ ((C.id , f) , C×P.id) ∘ ξ.dinatural.α (c , q) ∘ id
           ≈⟨ refl⟩∘⟨ identityʳ ⟩
-        F₁ ((C.id , f) , (C.id , P.id)) ∘ ξ.dinatural.α (c , q)
+        F₁ ((C.id , f) , C×P.id) ∘ ξ.dinatural.α (c , q)
           ≈˘⟨ refl⟩∘⟨ ω.universal (q , q) ⟩
-        F₁ ((C.id , f) , (C.id , P.id)) ∘ ω.dinatural.α (q , q) c ∘ ω.factor (q , q) _
+        F₁ ((C.id , f) , C×P.id) ∘ ωq,q c ∘ ρq
           ≈˘⟨ extendʳ $ end-η-commute ⦃ ω (q , q) ⦄ ⦃ ω (p , q) ⦄ (curry.₀.₁ (F ′) (f , P.id)) c ⟩
-        ω.dinatural.α (p , q) c ∘ ∫F.₁ (f , P.id) ∘ ω.factor (q , q) _
+        ωp,q c ∘ ∫F.₁ (f , P.id) ∘ ρq
           ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ ⟩
-        ω.dinatural.α (p , q) c ∘ ∫F.₁ (f , P.id) ∘ ω.factor (q , q) _ ∘ id
+        ωp,q c ∘ ∫F.₁ (f , P.id) ∘ ρq ∘ id
           ∎
-      }
+      where ωp,p = ω.dinatural.α (p , p)
+            ωp,q = ω.dinatural.α (p , q)
+            ωq,q = ω.dinatural.α (q , q)
+            ρp = ρ  .dinatural.α p
+            ρq = ρ  .dinatural.α q
+
   -- This construction is actually stronger than Fubini. It states that the
   -- iterated end _is_ an end in the product category.
   -- Thus the product end need not exist.
@@ -160,9 +177,8 @@ module _  (F : Bifunctor (Category.op C ×ᶜ Category.op P) (C ×ᶜ P) D)
     eₚ .∫.wedge = ξ eᵢ.wedge
     eₚ .∫.factor W = eᵢ.factor (ρ W)
     eₚ .∫.universal {W} {c , p} = begin
-      ξ eᵢ.wedge .dinatural.α (c , p) ∘ eᵢ.factor (ρ W)               ≈⟨ Equiv.refl ⟩
-      (ω.dinatural.α (p , p) c ∘ eᵢ.dinatural.α p)  ∘ eᵢ.factor (ρ W) ≈⟨ assoc ⟩
-      ω.dinatural.α (p , p) c ∘ (eᵢ.dinatural.α p  ∘ eᵢ.factor (ρ W)) ≈⟨ refl⟩∘⟨ eᵢ.universal {ρ W} {p} ⟩
+      ξ eᵢ.wedge .dinatural.α (c , p) ∘ eᵢ.factor (ρ W)               ≡⟨⟩
+      (ω.dinatural.α (p , p) c ∘ eᵢ.dinatural.α p)  ∘ eᵢ.factor (ρ W) ≈⟨ pullʳ (eᵢ.universal {ρ W} {p}) ⟩
       ω.dinatural.α (p , p) c ∘ (ρ W) .dinatural.α p                  ≈⟨ ω.universal (p , p) ⟩
       W .dinatural.α  (c , p)                                         ∎
     eₚ .∫.unique {W} {g} h = eᵢ.unique λ {A = p} → Equiv.sym $ ω.unique (p , p) (sym-assoc ○ h)