From 34609d58ff45bd539b83e67bd5110d19dc3d10ef Mon Sep 17 00:00:00 2001
From: Calvin Lee <pounce@integraldoma.in>
Date: Tue, 25 Jun 2024 13:57:12 +0000
Subject: [PATCH 1/5] End calculus

---
 .../Category/Construction/Functors.agda       |   2 +
 .../Category/Construction/TwistedArrow.agda   |  37 ++-
 src/Categories/Diagram/End/Fubini.agda        | 206 ++++++++++++++
 .../End/Instances/NaturalTransformation.agda  |  66 +++++
 src/Categories/Diagram/End/Parameterized.agda | 223 +++++++++++++++
 src/Categories/Diagram/End/Properties.agda    | 263 ++++++++++++------
 src/Categories/Functor/Bifunctor.agda         |   7 +-
 .../Functor/Bifunctor/Properties.agda         |   4 +
 src/Categories/Functor/Instance/Twisted.agda  |  83 ++----
 .../NaturalTransformation/Equivalence.agda    |  45 ++-
 10 files changed, 761 insertions(+), 175 deletions(-)
 create mode 100644 src/Categories/Diagram/End/Fubini.agda
 create mode 100644 src/Categories/Diagram/End/Instances/NaturalTransformation.agda
 create mode 100644 src/Categories/Diagram/End/Parameterized.agda

diff --git a/src/Categories/Category/Construction/Functors.agda b/src/Categories/Category/Construction/Functors.agda
index df91df99c..33505936d 100644
--- a/src/Categories/Category/Construction/Functors.agda
+++ b/src/Categories/Category/Construction/Functors.agda
@@ -130,6 +130,8 @@ module curry {o₁ e₁ ℓ₁} {C₁ : Category o₁ e₁ ℓ₁}
   open Category
   open NaturalIsomorphism
 
+  module ₀ (F : Bifunctor C₁ C₂ D) = Functor (Functor.F₀ curry F)
+
   -- Currying preserves natural isos.
   -- This makes |curry.F₀| a map between the hom-setoids of Cats.
 
diff --git a/src/Categories/Category/Construction/TwistedArrow.agda b/src/Categories/Category/Construction/TwistedArrow.agda
index 01211c247..411dba6a8 100644
--- a/src/Categories/Category/Construction/TwistedArrow.agda
+++ b/src/Categories/Category/Construction/TwistedArrow.agda
@@ -1,20 +1,26 @@
 {-# OPTIONS --without-K --safe #-}
+open import Data.Product using (_,_; _×_; map; zip)
+open import Function.Base using (_$_; flip)
+open import Level
+open import Relation.Binary.Core using (Rel)
+
 open import Categories.Category using (Category; module Definitions)
+open import Categories.Category.Product renaming (Product to _×ᶜ_)
+open import Categories.Functor
+
+import Categories.Morphism as M
+import Categories.Morphism.Reasoning as MR
 
 -- Definition of the "Twisted Arrow" Category of a Category 𝒞
 module Categories.Category.Construction.TwistedArrow {o ℓ e} (𝒞 : Category o ℓ e) where
 
-open import Level
-open import Data.Product using (_,_; _×_; map; zip)
-open import Function.Base using (_$_; flip)
-open import Relation.Binary.Core using (Rel)
+private
+  open module 𝒞 = Category 𝒞
 
-import Categories.Morphism as M
-open M 𝒞
-open import Categories.Morphism.Reasoning 𝒞
 
-open Category 𝒞
+open M 𝒞
 open Definitions 𝒞
+open MR 𝒞
 open HomReasoning
 
 private
@@ -68,3 +74,18 @@ TwistedArrow = record
     cod⇒ m₁ ∘ (cod⇒ m₂ ∘ Morphism.arr A) ∘ (dom⇐ m₂ ∘ dom⇐ m₁) ≈⟨ refl⟩∘⟨ (pullˡ assoc) ⟩
     cod⇒ m₁ ∘ (cod⇒ m₂ ∘ Morphism.arr A ∘ dom⇐ m₂) ∘ dom⇐ m₁   ≈⟨ (refl⟩∘⟨ square m₂ ⟩∘⟨refl) ⟩
     cod⇒ m₁ ∘ Morphism.arr B ∘ dom⇐ m₁ ∎
+
+
+-- Consider TwistedArrow as the comma category * / Hom[C][-,-]
+-- We have the codomain functor TwistedArrow → C.op × C
+
+module _ where
+  open Morphism
+  open Morphism⇒
+  open Functor
+  Forget : Functor TwistedArrow (𝒞.op ×ᶜ 𝒞)
+  Forget .F₀ x = dom x , cod x
+  Forget .F₁ f = dom⇐ f , cod⇒ f
+  Forget .identity = Equiv.refl , Equiv.refl
+  Forget .homomorphism = Equiv.refl , Equiv.refl
+  Forget .F-resp-≈ e = e
diff --git a/src/Categories/Diagram/End/Fubini.agda b/src/Categories/Diagram/End/Fubini.agda
new file mode 100644
index 000000000..d5be65ed8
--- /dev/null
+++ b/src/Categories/Diagram/End/Fubini.agda
@@ -0,0 +1,206 @@
+{-# OPTIONS --without-K --lossy-unification #-}
+
+open import Level
+open import Data.Product using (Σ; _,_; _×_) renaming (proj₁ to fst; proj₂ to snd)
+open import Function using (_$_)
+
+open import Categories.Category
+open import Categories.Category.Construction.Functors
+open import Categories.Category.Product renaming (Product to _×ᶜ_)
+open import Categories.Diagram.End using () renaming (End to ∫)
+open import Categories.Diagram.End.Properties
+open import Categories.Diagram.End.Parameterized renaming (EndF to ⨏)
+open import Categories.Diagram.Wedge
+open import Categories.Functor renaming (id to idF)
+open import Categories.Functor.Bifunctor
+open import Categories.Functor.Bifunctor.Properties
+open import Categories.NaturalTransformation using (NaturalTransformation)
+open import Categories.NaturalTransformation.Dinatural
+
+import Categories.Morphism as M
+import Categories.Morphism.Reasoning as MR
+
+module Categories.Diagram.End.Fubini where
+variable
+  o ℓ e : Level
+  C P D : Category o ℓ e
+
+module Functor-Swaps  (F : Bifunctor (Category.op C ×ᶜ Category.op P) (C ×ᶜ P) D) where
+  private
+    module C = Category C
+    module P = Category P
+
+  -- just shuffling arguments
+  -- An end of F ′ can be taken iterated, instead of in the product category
+  _′ : Bifunctor (P.op ×ᶜ P) (C.op ×ᶜ C) D
+  _′ = F ∘F ((πˡ ∘F πʳ ※ πˡ ∘F πˡ) ※ (πʳ ∘F πʳ ※ πʳ ∘F πˡ))
+
+  -- An end of F ′′ is the same as F, but the order in the product category is reversed
+  _′′ : Bifunctor (Category.op P ×ᶜ Category.op C) (P ×ᶜ C) D
+  _′′ = F ∘F (Swap ⁂ Swap)
+
+open Functor-Swaps
+
+module _  (F : Bifunctor (Category.op C ×ᶜ Category.op P) (C ×ᶜ P) D)
+          {ω : ∀ ((p , q) : Category.Obj P × Category.Obj P) → ∫ (appˡ (F ′) (p , q))}
+           where
+  open M D
+  private
+    module C = Category C
+    module P = Category P
+    module D = Category D
+    open module F = Functor F using (F₀; F₁; F-resp-≈)
+    ∫F = (⨏ (F ′) {ω})
+    module ∫F = Functor ∫F
+
+    module ω ((p , q) : P.Obj × P.Obj) = ∫ (ω (p , q))
+
+  open _≅_
+  open Iso
+  open DinaturalTransformation using (α)
+  open NaturalTransformation using (η)
+  open Wedge renaming (E to apex)
+  open Category D
+  open import Categories.Morphism.Reasoning D
+  open HomReasoning
+  -- we show that wedges of (∫.E e₀) are in bijection with wedges of F
+  -- following MacLane §IX.8
+  private module _ (ρ : Wedge ∫F) where
+    private
+      open module ρ = Wedge ρ using () renaming (E to x)
+    -- 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
+            ≈⟨ 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
+            ≈⟨ (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
+            ≈⟨ (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
+            ≈⟨ 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)
+          -- 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
+            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨  ⟺ identityʳ ⟩
+          F₁ ((f , P.id) , (C.id , P.id)) ∘ ω.dinatural.α (p , q) d ∘ ∫F.F₁ (P.id , s) ∘ ρ.dinatural.α 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
+            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ ⟩
+          F₁ ((f , P.id) , (C.id , P.id)) ∘ ω.dinatural.α (p , q) d ∘ ∫F.F₁ (s , P.id) ∘ ρ.dinatural.α 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)
+            ≈⟨ 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
+            ≈˘⟨ refl⟩∘⟨ identityʳ ⟩
+          F₁ ((f , s) , (C.id , P.id)) ∘ (ω.dinatural.α (q , q) d ∘ ρ.dinatural.α q) ∘ id
+          ∎
+        }
+      }
+
+  -- now the opposite direction
+  private module _ (ξ : Wedge F) where
+    private
+      open module ξ = Wedge ξ using () renaming (E to x)
+    ρ : Wedge ∫F
+    ρ .apex = x
+    ρ .dinatural = dtHelper record
+      { α = λ 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
+          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ ⟩
+        ω.dinatural.α (p , q) c ∘ ∫F.₁ (P.id , f) ∘ ω.factor (p , 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)) _
+          ≈⟨ refl⟩∘⟨ ω.universal (p , p) ⟩
+        F₁ ((C.id , P.id) , (C.id , f)) ∘ ξ.dinatural.α (c , p)
+          ≈˘⟨ refl⟩∘⟨ identityʳ ⟩
+        F₁ ((C.id , 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
+          ≈⟨ refl⟩∘⟨ identityʳ ⟩
+        F₁ ((C.id , f) , (C.id , P.id)) ∘ ξ.dinatural.α (c , q)
+          ≈˘⟨ refl⟩∘⟨ ω.universal (q , q) ⟩
+        F₁ ((C.id , f) , (C.id , P.id)) ∘ ω.dinatural.α (q , q) c ∘ ω.factor (q , 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) _
+          ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ ⟩
+        ω.dinatural.α (p , q) c ∘ ∫F.₁ (f , P.id) ∘ ω.factor (q , q) _ ∘ id
+          ∎
+      }
+  -- 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.
+  module _ {{eᵢ : ∫ (⨏ (F ′) {ω})}} where
+    private
+      module eᵢ = ∫ eᵢ
+    eₚ : ∫ F
+    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} ⟩
+      ω.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)
+    module eₚ = ∫ eₚ
+
+    -- corollary: if a product end exists, it is iso
+    Fubini : {eₚ' : ∫ F} → ∫.E eᵢ ≅ ∫.E eₚ'
+    Fubini {eₚ'} = end-unique eₚ eₚ'
+
+  -- TODO show that an end ∫ F yields an end of ∫ (⨏ (F ′) {ω})
+
+module _ (F : Bifunctor (Category.op C ×ᶜ Category.op P) (C ×ᶜ P) D)
+         {ωᴾ : ∀ ((p , q) : Category.Obj P × Category.Obj P) → ∫ (appˡ (F ′) (p , q))}
+         {ωᶜ : ∀ ((c , d) : Category.Obj C × Category.Obj C) → ∫ (appˡ (F ′′ ′)(c , d))}
+         {{e₁ : ∫ (⨏ (F ′) {ωᴾ})}} {{e₂ : ∫ (⨏ (F ′′ ′) {ωᶜ})}} where
+  open M D
+  -- since `F` and `F′′` are functors from different categories we can't construct a
+  -- natural isomorphism between them. Instead it is best to show that eₚ F is an end in
+  -- ∫ (F ′′) or vice-versa, and then Fubini follows due to uniqueness of ends
+  open Wedge renaming (E to apex)
+  private
+    eₚ′′ : ∫ (F ′′)
+    eₚ′′  .∫.wedge .apex = eₚ.wedge.E F
+    eₚ′′  .∫.wedge .dinatural = dtHelper record
+      { α = λ (p , c) → eₚ.dinatural.α F (c , p)
+      ; commute = λ (s , f) → eₚ.dinatural.commute F (f , s)
+      }
+    eₚ′′  .∫.factor W = eₚ.factor F record
+      { W ; dinatural = dtHelper record
+        { α = λ (c , p) → W.dinatural.α (p , c)
+        ; commute = λ (f , s) → W.dinatural.commute (s , f)
+        }
+      }
+      where module W = Wedge W
+    eₚ′′  .∫.universal {W} {p , c} = eₚ.universal F
+    eₚ′′  .∫.unique {W} {g} h = eₚ.unique F h
+
+  Fubini′ : ∫.E e₁ ≅ ∫.E e₂
+  Fubini′ = ≅.trans (Fubini F {ωᴾ} {eₚ' = eₚ F} ) $
+            ≅.trans (end-unique eₚ′′ (eₚ (F ′′)))
+                    (≅.sym (Fubini (F ′′) {ωᶜ} {eₚ' = eₚ (F ′′)}))
diff --git a/src/Categories/Diagram/End/Instances/NaturalTransformation.agda b/src/Categories/Diagram/End/Instances/NaturalTransformation.agda
new file mode 100644
index 000000000..3a8a30a60
--- /dev/null
+++ b/src/Categories/Diagram/End/Instances/NaturalTransformation.agda
@@ -0,0 +1,66 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Product using (Σ; _,_)
+open import Function using (_$_)
+open import Level
+
+open import Categories.Category
+open import Categories.Category.Instance.Setoids
+open import Categories.Category.Product
+open import Categories.Diagram.End using () renaming (End to ∫)
+open import Categories.Functor renaming (id to idF)
+open import Categories.Functor.Hom
+open import Categories.NaturalTransformation renaming (id to idN)
+open import Categories.NaturalTransformation.Dinatural using (DinaturalTransformation; dtHelper)
+open import Categories.NaturalTransformation.Equivalence
+open import Function.Bundles using (Func)
+
+import Categories.Diagram.Wedge as Wedges
+import Categories.Morphism as M
+import Categories.Morphism.Reasoning as MR
+
+module Categories.Diagram.End.Instances.NaturalTransformation {ℓ e o′}
+  {C : Category ℓ ℓ e} {D : Category o′ ℓ ℓ} (F G : Functor C D) where
+
+private
+  module C = Category C
+  module D = Category D
+  open module F = Functor F using (F₀; F₁)
+  module G = Functor G
+
+open Wedges (Hom[ D ][-,-] ∘F (F.op ⁂ G))
+open D
+open HomReasoning
+open MR D
+open NaturalTransformation renaming (η to app)
+open ∫ hiding (dinatural)
+open Wedge
+open Func
+
+NTs-are-End : ∫ (Hom[ D ][-,-] ∘F (F.op ⁂ G))
+NTs-are-End .wedge .E = (≃-setoid F G)
+NTs-are-End .wedge .dinatural = dtHelper record
+  { α = λ C → record
+    { to = λ η → η .app C
+    ; cong = λ e → e
+    }
+  ; commute = λ {X} {Y} f {η} → begin
+    G.₁ f ∘ η .app X ∘ F₁ C.id  ≈⟨ pullˡ (η .sym-commute f) ⟩
+    (η .app Y ∘ F₁ f) ∘ F₁ C.id ≈⟨ refl⟩∘⟨ F.identity ⟩
+    (η .app Y ∘ F₁ f) ∘ id      ≈⟨ id-comm ⟩
+    id ∘ η .app Y ∘ F₁ f        ≈⟨ ⟺ G.identity ⟩∘⟨refl ⟩
+    G.₁ C.id ∘ η .app Y ∘ F₁ f  ∎
+  }
+NTs-are-End .factor W .to s = ntHelper record
+  { η = λ X → W.dinatural.α X .to s
+  -- basically the opposite proof of above
+  ; commute = λ {X} {Y} f → begin
+    W.dinatural.α Y .to s ∘ F₁ f            ≈⟨ introˡ G.identity ⟩
+    G.₁ C.id ∘ W.dinatural.α Y .to s ∘ F₁ f ≈˘⟨ W.dinatural.commute f ⟩
+    G.₁ f ∘ W.dinatural.α X .to s ∘ F₁ C.id ≈⟨ refl⟩∘⟨ elimʳ F.identity ⟩
+    G.F₁ f ∘ W.dinatural.α X .to s          ∎
+  }
+  where module W = Wedge W
+NTs-are-End .factor W .cong e {x} = W .dinatural.α x .cong e
+NTs-are-End .universal = Equiv.refl
+NTs-are-End .unique h = Equiv.sym h
diff --git a/src/Categories/Diagram/End/Parameterized.agda b/src/Categories/Diagram/End/Parameterized.agda
new file mode 100644
index 000000000..d504cb159
--- /dev/null
+++ b/src/Categories/Diagram/End/Parameterized.agda
@@ -0,0 +1,223 @@
+{-# OPTIONS --without-K #-}
+module Categories.Diagram.End.Parameterized where
+
+open import Level
+open import Function using (_$_)
+open import Data.Product using (Σ; _,_)
+
+open import Categories.Category
+open import Categories.Category.Construction.Functors
+open import Categories.Category.Product renaming (Product to _×ᶜ_)
+open import Categories.Diagram.End renaming (End to ∫)
+open import Categories.Diagram.End.Properties
+open import Categories.Diagram.Wedge
+open import Categories.Functor hiding (id)
+open import Categories.Functor.Bifunctor
+open import Categories.Functor.Bifunctor.Properties
+open import Categories.Functor.Limits
+open import Categories.NaturalTransformation renaming (_∘ʳ_ to _▹ⁿ_; id to idN)
+open import Categories.NaturalTransformation.Dinatural hiding (_≃_)
+open import Categories.NaturalTransformation.NaturalIsomorphism renaming (_≃_ to _≃ⁱ_)
+open import Categories.NaturalTransformation.Equivalence
+
+import Categories.Category.Construction.Wedges as Wedges
+import Categories.Morphism as M
+import Categories.Morphism.Reasoning as MR
+
+-- The following conventions are taken in this file: C is the 'source' category
+-- and D is the destination. If two source categories are needed, the other is
+-- called 'P' for "parameter", following MacLane. F, G and H are functors and ef,
+-- eg and eh are witnesses of their respective ends.
+
+private
+  variable
+    o ℓ e : Level
+    P C D E : Category o ℓ e
+
+-- we use MacLane's notation for paramaterized ends (CWM §IX.5)
+_♯ : Functor (P ×ᶜ (Category.op C ×ᶜ C)) D → Functor (Category.op C ×ᶜ C) (Functors P D)
+F ♯ = curry.₀ F.flip
+  where module F = Bifunctor F
+
+end-η♯ : {F G : Functor (P ×ᶜ (Category.op C ×ᶜ C)) D} (η : NaturalTransformation F G)
+         ⦃ ef : ∫ (F ♯) ⦄ ⦃ eg : ∫ (G ♯) ⦄ → NaturalTransformation (∫.E ef) (∫.E eg)
+end-η♯ η ⦃ ef ⦄ ⦃ eg ⦄ = end-η (curry.₁ (η ▹ⁿ Swap))
+
+module _ (F : Functor (P ×ᶜ ((Category.op C) ×ᶜ C)) D) {ω : ∀ X → ∫ (appˡ F X)} where
+  private
+    module F = Functor F
+
+    module C = Category C
+    module D = Category D
+    module P = Category P
+    module NT = NaturalTransformation
+    F′ = curry.₀ F
+    module ω (p : P.Obj) = ∫ (ω p)
+  open D
+  open HomReasoning
+
+  open MR D
+  open module F′ = Functor F′
+  open ∫ hiding (E)
+  open NT using (η)
+
+  EndF : Functor P D
+  EndF = record
+    { F₀           = λ X → ω.E X
+    ; F₁           = λ {X} {Y} f → end-η (curry.₀.₁ F f) ⦃ ω X ⦄ ⦃ ω Y ⦄
+    ; identity     = λ {A} → begin
+      end-η (curry.₀.₁ F P.id) ⦃ ω A ⦄ ⦃ ω A ⦄ ≈⟨ end-η-resp-≈ ⦃ ω A ⦄ ⦃ ω A ⦄ (curry.₀.identity F) ⟩
+      end-η idN ⦃ ω A ⦄ ⦃ ω A ⦄                ≈⟨ end-identity ⦃ ω A ⦄ ⟩
+      id                                       ∎
+    ; homomorphism = λ {A B C} {f g} → begin
+      end-η (curry.₀.₁ F (P [ g ∘ f ])) ⦃ ω A ⦄ ⦃ ω C ⦄ 
+        ≈⟨ end-η-resp-≈ ⦃ ω A ⦄ ⦃ ω C ⦄ (curry.₀.homomorphism F) ⟩
+      end-η (curry.₀.₁ F g ∘ᵥ curry.₀.₁ F f ) ⦃ ω A ⦄ ⦃ ω C ⦄
+        ≈⟨  end-η-resp-∘ (curry.₀.₁ F f) (curry.₀.₁ F g) ⦃ ω A ⦄ ⦃ ω B ⦄ ⦃ ω C ⦄ ⟩
+      end-η (curry.₀.₁ F g) ⦃ ω B ⦄ ⦃ ω C ⦄ ∘ end-η (curry.₀.₁ F f) ⦃ ω A ⦄ ⦃ ω B ⦄
+        ∎
+    ; F-resp-≈     = λ {A B f g} eq → end-η-resp-≈ ⦃ ω A ⦄ ⦃ ω B ⦄ (curry.₀.F-resp-≈ F eq)
+    }
+
+
+  -- The parameter theorem
+  EndF-is-End : ∫ (F ♯)
+  EndF-is-End .∫.wedge .Wedge.E = EndF
+  EndF-is-End .∫.wedge .Wedge.dinatural = dtHelper record
+    { α = λ c → ntHelper record
+      { η = λ p → ω.dinatural.α p c
+      ; commute = λ {p} {q} f → begin
+        ω.dinatural.α q c ∘ end-η (curry.₀.₁ F f) ⦃ ω p ⦄ ⦃ ω q ⦄
+        ≈⟨ end-η-commute ⦃ ω p ⦄ ⦃ ω q ⦄ (curry.₀.₁ F f) c ⟩
+        (curry.₀.₁ F f) .η (c , c) ∘ ω.dinatural.α p c
+        ∎
+      }
+    ; commute = λ f {p} → ω.dinatural.commute p f
+    }
+  EndF-is-End .∫.factor W = ntHelper record
+    { η = λ p → ω.factor p (W' p)
+    ; commute = λ {p} {q} f → ω.unique′ q $ λ {c} → begin
+      ω.dinatural.α q c ∘ ω.factor q (W' q) ∘ F'.₁ f
+      ≈⟨ pullˡ (ω.universal q) ⟩
+      W.dinatural.α c .η q ∘ F'.₁ f 
+      ≈⟨ W.dinatural.α c .NaturalTransformation.commute f  ⟩
+      (curry.₀.₁ F f) .η (c , c) ∘ W.dinatural.α c .η p
+      ≈˘⟨ refl⟩∘⟨ ω.universal p ⟩
+      (curry.₀.₁ F f) .η (c , c) ∘ ω.dinatural.α p c ∘ factor (ω p) (W' p)
+      ≈˘⟨ extendʳ  (end-η-commute ⦃ ω p ⦄ ⦃ ω q ⦄ (curry.₀.₁ F f) c) ⟩
+      ω.dinatural.α q c ∘ end-η (curry.₀.₁ F f) ⦃ ω p ⦄ ⦃ ω q ⦄ ∘ ω.factor p (W' p)
+      ∎
+    }
+    where module W = Wedge W
+          F' = W.E
+          module F' = Functor F'
+          W' : (p : P.Obj) → Wedge (appˡ F p)
+          W' p = record
+            { E = F'.₀ p
+            ; dinatural = dtHelper record
+              { α = λ c → W.dinatural.α c .η p
+              ; commute = λ f → W.dinatural.commute f
+              }
+            }
+          module W' p = Wedge (W' p)
+  EndF-is-End .∫.universal {W} {c} {p} = ω.universal p
+  EndF-is-End .∫.unique h {p} = ω.unique p h
+
+-- Continuous functors preserve EndF
+-- this takes way too much time to check for some reason
+module _ {C : Category o ℓ e}
+         (J : Functor (P ×ᶜ ((Category.op C) ×ᶜ C)) D)
+         (F : Functor D E) {ω : ∀ X → ∫ (appˡ J X)} {cont : Continuous (o ⊔ ℓ) (ℓ ⊔ e) e F} where
+  private
+    module D = Category D
+    module P = Category P
+    module C = Category C
+    module E = Category E
+    open module F = Functor F using (F₀; F₁; F-resp-≈)
+    open module J = Functor J using () renaming (F₀ to J₀; F₁ to J₁)
+    module ω (X : P.Obj) = ∫ (ω X)
+    module appˡJ  = curry.₀ J
+    module appˡFJ  = curry.₀ (F ∘F J)
+
+  open E
+  open HomReasoning
+  appˡ-resp-∘ : ∀ X → F ∘F appˡ J X ≃ⁱ appˡ (F ∘F J) X
+  appˡ-resp-∘ X = niHelper record
+    { η = λ Y → id
+    ; η⁻¹ = λ Y → id
+    ; commute = λ f → identityˡ ○ ⟺ identityʳ
+    ; iso = λ Y → record
+      { isoˡ = identity²
+      ; isoʳ = identity²
+      }
+    }
+  --module appˡ-resp-∘ X = NaturalIsomorphism (appˡ-resp-∘ X)
+
+  Continuous-preserve-endf-motive : ∀ X → ∫ (appˡ (F ∘F J) X)
+  Continuous-preserve-endf-motive X = ≅-yields-end (appˡ-resp-∘ X) (contF-as-end (appˡ J X) F {cont} (ω X))
+
+  open NaturalTransformation using (η)
+
+  private
+    ω' = Continuous-preserve-endf-motive
+    module ω' (X : P.Obj) = ∫ (ω' X)
+    --module EndF {A B} (J : Functor A B) {ω} = Functor (EndF J {ω})
+
+  open MR E
+  Continuous-pres-EndF :  F ∘F (EndF J {ω}) ≃ⁱ EndF (F ∘F J) {ω'}
+  Continuous-pres-EndF = niHelper record
+    { η = λ X → E.id
+    ; η⁻¹ = λ Y → E.id
+    ; commute = λ {p} {q} f → begin
+      id ∘ Functor.F₁ (F ∘F EndF J {ω}) f ≈⟨ identityˡ ⟩
+      Functor.F₁ (F ∘F EndF J {ω}) f      ≡⟨⟩
+      F₁ (end-η (appˡJ.₁ f) ⦃ ω p ⦄ ⦃ ω q ⦄)
+        ≈⟨ ω'.unique′ q (λ {A} → begin
+          ω'.dinatural.α q A ∘ F₁ (end-η (appˡJ.₁ f) ⦃ ω p ⦄ ⦃ ω q ⦄)
+            ≈⟨ lemma ⟩∘⟨refl ⟩
+          F₁ (ω.dinatural.α q A) ∘ F₁ (end-η (appˡJ.₁ f) ⦃ ω p ⦄ ⦃ ω q ⦄)
+            ≈˘⟨ F.homomorphism ⟩
+          F₁ (ω.dinatural.α q A D.∘ end-η (appˡJ.₁ f) ⦃ ω p ⦄ ⦃ ω q ⦄)
+            ≈⟨ F-resp-≈ (end-η-commute ⦃ ω p ⦄ ⦃ ω q ⦄ (appˡJ.₁ f) A ) ⟩
+          F₁ ((appˡJ.₁ f) .η (A , A) D.∘ (ω.dinatural.α p A))
+            ≈⟨ F.homomorphism ⟩
+          F₁ ((appˡJ.₁ f) .η (A , A)) ∘ F₁ (ω.dinatural.α p A)
+            ≈˘⟨ refl⟩∘⟨ lemma ⟩
+          F₁ ((appˡJ.₁ f) .η (A , A)) ∘ (ω'.dinatural.α p A)
+            ≡⟨⟩
+          appˡFJ.₁ f .η (A , A) ∘ ω'.dinatural.α p A
+            ≈˘⟨ end-η-commute ⦃ ω' p ⦄ ⦃ ω' q ⦄ (appˡFJ.₁ f) A ⟩
+          ω'.dinatural.α q A ∘ end-η (appˡFJ.₁ f) ⦃ ω' p ⦄ ⦃ ω' q ⦄
+            ∎
+        )⟩
+      end-η (appˡFJ.₁ f) ⦃ ω' p ⦄ ⦃ ω' q ⦄
+        ≡⟨⟩
+      Functor.F₁ (EndF (F ∘F J) {ω'}) f   ≈˘⟨ identityʳ ⟩
+      Functor.F₁ (EndF (F ∘F J) {ω'}) f ∘ id
+        ∎
+    ; iso = λ Y → record
+      { isoˡ = E.identity²
+      ; isoʳ = E.identity²
+      }
+    }
+    where open E.HomReasoning
+          lemma : ∀ {q A} → ω'.dinatural.α q A ≈ F₁ (ω.dinatural.α q A)
+          lemma {q} {A} = begin
+            ω'.dinatural.α q A
+              ≡⟨⟩
+            id ∘ F₁ (J₁ (P.id , C.id , C.id)) ∘
+            id ∘ F₁ (J₁ (P.id , C.id , C.id) D.∘ ω.dinatural.α q A)
+              ≈⟨ identityˡ ⟩
+            F₁ (J₁ (P.id , C.id , C.id)) ∘
+            id ∘ F₁ (J₁ (P.id , C.id , C.id) D.∘ ω.dinatural.α q A)
+              ≈⟨ F-resp-≈ J.identity ⟩∘⟨refl ⟩
+            F₁ (D.id) ∘ id ∘ F₁ (J₁ (P.id , C.id , C.id) D.∘ ω.dinatural.α q A)
+              ≈⟨ elimˡ F.identity ⟩
+            id ∘ F₁ (J₁ (P.id , C.id , C.id) D.∘ ω.dinatural.α q A)
+              ≈⟨ identityˡ ⟩
+            F₁ (J₁ (P.id , C.id , C.id) D.∘ ω.dinatural.α q A)
+              ≈⟨ F-resp-≈ (D.∘-resp-≈ˡ J.identity) ⟩
+            F₁ (D.id D.∘ ω.dinatural.α q A)
+              ≈⟨ F-resp-≈ D.identityˡ ⟩
+            F₁ (ω.dinatural.α q A) 
+              ∎
diff --git a/src/Categories/Diagram/End/Properties.agda b/src/Categories/Diagram/End/Properties.agda
index 7268be5b7..daaeb4803 100644
--- a/src/Categories/Diagram/End/Properties.agda
+++ b/src/Categories/Diagram/End/Properties.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --without-K --safe --lossy-unification #-}
 
 module Categories.Diagram.End.Properties where
 
@@ -7,40 +7,50 @@ open import Data.Product using (Σ; _,_)
 open import Function using (_$_)
 
 open import Categories.Category
-open import Categories.Category.Product
 open import Categories.Category.Construction.Functors
 open import Categories.Category.Construction.TwistedArrow
-open import Categories.Category.Equivalence
+open import Categories.Category.Equivalence as SE using (StrongEquivalence)
 open import Categories.Category.Equivalence.Preserves
+open import Categories.Category.Product renaming (Product to _×ᶜ_)
 open import Categories.Diagram.Cone
-open import Categories.Diagram.End as ∫
+open import Categories.Diagram.End renaming (End to ∫)
 open import Categories.Diagram.Limit
+open import Categories.Diagram.Limit.Properties
 open import Categories.Diagram.Wedge
 open import Categories.Diagram.Wedge.Properties
 open import Categories.Functor hiding (id)
 open import Categories.Functor.Bifunctor
+open import Categories.Functor.Bifunctor.Properties
 open import Categories.Functor.Instance.Twisted
-import Categories.Morphism as M
-open import Categories.NaturalTransformation hiding (id)
-open import Categories.NaturalTransformation.Dinatural
+open import Categories.Functor.Limits
+open import Categories.NaturalTransformation renaming (_∘ʳ_ to _▹ⁿ_; id to idN)
+open import Categories.NaturalTransformation.Dinatural hiding (_≃_)
+open import Categories.NaturalTransformation.Equivalence renaming (_≃_ to _≃ⁿ_)
+open import Categories.NaturalTransformation.NaturalIsomorphism renaming (_≃_ to _≃ⁱ_)
+open import Categories.NaturalTransformation.NaturalIsomorphism.Properties
 open import Categories.Object.Terminal as Terminal
 
 import Categories.Category.Construction.Wedges as Wedges
-open import Categories.Object.Terminal
-
+import Categories.Morphism as M
 import Categories.Morphism.Reasoning as MR
 
+-- The following conventions are taken in this file: C is the 'source' category
+-- and D is the destination. If two source categories are needed, the other is
+-- called 'P' for "parameter", following MacLane. F, G and H are functors and ef,
+-- eg and eh are witnesses of their respective ends.
+
 private
   variable
-    o ℓ e : Level
-    C D E : Category o ℓ e
+    o ℓ e o′ ℓ′ e′ : Level
+    P C D E : Category o ℓ e
+
+open Category using (o-level; ℓ-level; e-level)
 
-module _ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
-  (F : Bifunctor (Category.op C) C D) where
+module _ (F : Bifunctor (Category.op C) C D) where
   open Wedges F
 
   -- Being an End is the same as being a Terminal object in the category of Wedges
-  End⇒Terminal : End F → Terminal Wedges
+  End⇒Terminal : ∫ F → Terminal Wedges
   End⇒Terminal c =  record
     { ⊤ = wedge
     ; ⊤-is-terminal = record
@@ -49,9 +59,9 @@ module _ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ 
       }
     }
     where
-    open End c
+    open ∫ c
 
-  Terminal⇒End : Terminal Wedges → End F
+  Terminal⇒End : Terminal Wedges → ∫ F
   Terminal⇒End i = record
     { wedge = ⊤
     ; factor = λ W → u {W₁ = W} !
@@ -62,97 +72,67 @@ module _ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ 
     open Terminal.Terminal i
     open Wedge-Morphism
 
-module _ {C : Category o ℓ e}
-         (F : Functor E (Functors (Product (Category.op C) C) D)) where
-  private
-    module C = Category C
-    module D = Category D
-    module E = Category E
-    module NT = NaturalTransformation
-  open D
-  open HomReasoning
-
-  open MR D
-  open Functor F
-  open End hiding (E)
-  open NT using (η)
-
-  EndF : (∀ X → End (F₀ X)) → Functor E D
-  EndF end = record
-    { F₀           = λ X → End.E (end X)
-    ; F₁           = F₁′
-    ; identity     = λ {A} → unique (end A) (id-comm ○ ∘-resp-≈ˡ (⟺ identity))
-    ; homomorphism = λ {A B C} {f g} → unique (end C) $ λ {Z} → begin
-      dinatural.α (end C) Z ∘ F₁′ g ∘ F₁′ f                       ≈⟨ pullˡ (universal (end C)) ⟩
-      (η (F₁ g) (Z , Z) ∘ dinatural.α (end B) Z) ∘ F₁′ f          ≈⟨ pullʳ (universal (end B)) ⟩
-      η (F₁ g) (Z , Z) ∘ η (F₁ f) (Z , Z) ∘ dinatural.α (end A) Z ≈˘⟨ pushˡ homomorphism ⟩
-      η (F₁ (g E.∘ f)) (Z , Z) ∘ dinatural.α (end A) Z            ∎
-    ; F-resp-≈     = λ {A B f g} eq → unique (end B) $ λ {Z} → begin
-      dinatural.α (end B) Z ∘ F₁′ g                               ≈⟨ universal (end B) ⟩
-      η (F₁ g) (Z , Z) ∘ dinatural.α (end A) Z                    ≈˘⟨ F-resp-≈ eq ⟩∘⟨refl ⟩
-      η (F₁ f) (Z , Z) ∘ dinatural.α (end A) Z                    ∎
-    }
-    where F₁′ : ∀ {X Y} → X E.⇒ Y → End.E (end X) ⇒ End.E (end Y)
-          F₁′ {X} {Y} f = factor (end Y) $ record
-            { E         = End.E (end X)
-            ; dinatural = F₁ f <∘ dinatural (end X)
-            }
-
 -- A Natural Transformation between two functors induces an arrow between the
 -- (object part of) the respective ends.
-module _ {P Q : Functor (Product (Category.op C) C) D} (P⇒Q : NaturalTransformation P Q) where
-  open End renaming (E to end)
+module _ {F G : Functor ((Category.op C) ×ᶜ C) D} (F⇒G : NaturalTransformation F G) where
+  open ∫ renaming (E to end)
   open Category D
 
-  end-η : {ep : End P} {eq : End Q} → end ep ⇒ end eq
-  end-η {ep} {eq} = factor eq (record
-    { E = End.E ep
-    ; dinatural = dtHelper record
-      { α = λ c → η (c , c) ∘ dinatural.α ep c
-      ; commute = λ {C} {C′} f → begin
-        Q.₁ (C.id , f) ∘ (η (C , C) ∘ αp C) ∘ D.id       ≈⟨ pullˡ sym-assoc ⟩
-        ((Q.₁ (C.id , f) ∘ η (C , C)) ∘ αp C) ∘ D.id     ≈⟨ nt.sym-commute (C.id , f) ⟩∘⟨refl ⟩∘⟨refl ⟩
-        ((η (C , C′) ∘ P.₁ (C.id , f)) ∘ αp C) ∘ D.id    ≈⟨ assoc²αε ⟩
-        η (C , C′) ∘ (P.₁ (C.id , f) ∘ αp C ∘ D.id)      ≈⟨ refl⟩∘⟨ αp-comm f ⟩
-        η (C , C′) ∘ P.₁ (f , C.id) ∘ αp C′ ∘ D.id       ≈⟨ assoc²εα ⟩
-        ((η (C , C′) ∘ P.₁ (f , C.id)) ∘ αp C′) ∘ D.id   ≈⟨ nt.commute (f , C.id) ⟩∘⟨refl ⟩∘⟨refl ⟩
-        ((Q.₁ (f , C.id) ∘ η (C′ , C′)) ∘ αp C′) ∘ D.id  ≈⟨ pushˡ assoc ⟩
-        Q.₁ (f , C.id) ∘ (η (C′ , C′) ∘ αp C′) ∘ D.id    ∎
-      }
-    })
-    where
-    module nt = NaturalTransformation P⇒Q
-    open nt using (η)
-    open HomReasoning
-    module C = Category C
-    module D = Category D
-    module P = Functor P
-    module Q = Functor Q
-    open DinaturalTransformation (dinatural ep) renaming (α to αp; commute to αp-comm)
-    open DinaturalTransformation (dinatural eq) renaming (α to αq; commute to αq-comm)
-    open Wedge
-    open MR D
+  opaque
+    end-η : {{ef : ∫ F}} {{eg : ∫ G}} → end ef ⇒ end eg
+    end-η {{ef}} {{eg}} = factor eg (record
+      { E = ∫.E ef
+      ; dinatural = dtHelper record
+        { α = λ c → η (c , c) ∘ dinatural.α ef c
+        ; commute = λ {C} {C′} f → begin
+          G.₁ (C.id , f) ∘ (η (C , C) ∘ αf C) ∘ D.id       ≈⟨ pullˡ sym-assoc ⟩
+          ((G.₁ (C.id , f) ∘ η (C , C)) ∘ αf C) ∘ D.id     ≈⟨ nt.sym-commute (C.id , f) ⟩∘⟨refl ⟩∘⟨refl ⟩
+          ((η (C , C′) ∘ F.₁ (C.id , f)) ∘ αf C) ∘ D.id    ≈⟨ assoc²αε ⟩
+          η (C , C′) ∘ (F.₁ (C.id , f) ∘ αf C ∘ D.id)      ≈⟨ refl⟩∘⟨ αf-comm f ⟩
+          η (C , C′) ∘ F.₁ (f , C.id) ∘ αf C′ ∘ D.id       ≈⟨ assoc²εα ⟩
+          ((η (C , C′) ∘ F.₁ (f , C.id)) ∘ αf C′) ∘ D.id   ≈⟨ nt.commute (f , C.id) ⟩∘⟨refl ⟩∘⟨refl ⟩
+          ((G.₁ (f , C.id) ∘ η (C′ , C′)) ∘ αf C′) ∘ D.id  ≈⟨ pushˡ assoc ⟩
+          G.₁ (f , C.id) ∘ (η (C′ , C′) ∘ αf C′) ∘ D.id    ∎
+        }
+      })
+      where
+      module nt = NaturalTransformation F⇒G
+      open nt using (η)
+      open HomReasoning
+      module C = Category C
+      module D = Category D
+      module F = Functor F
+      module G = Functor G
+      open DinaturalTransformation (dinatural ef) renaming (α to αf; commute to αf-comm)
+      open DinaturalTransformation (dinatural eg) renaming (α to αg; commute to αg-comm)
+      open Wedge
+      open MR D
 
 -- The real start of the End Calculus. Maybe need to move such properties elsewhere?
 -- This is an unpacking of the lhs of Eq. (25) of Loregian's book.
-module _ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
-  (F : Bifunctor (Category.op C) C D) where
+module _ (F : Bifunctor (Category.op C) C D) where
   private
     Eq = ConesTwist≅Wedges F
     module O = M D
   open M (Wedges.Wedges F)
   open Functor
 
-  open StrongEquivalence Eq renaming (F to F⇒)
+  open StrongEquivalence Eq renaming (F to F⇒; G to F⇐)
+
+  End-yields-limit : ∫ F → Limit (Twist C D F)
+  End-yields-limit ef = record { terminal = pres-Terminal (SE.sym Eq) (End⇒Terminal F ef) }
+
+  limit-yields-End : Limit (Twist C D F) → ∫ F
+  limit-yields-End l = Terminal⇒End F (pres-Terminal Eq (Limit.terminal l))
 
   -- Ends and Limits are equivalent, in the category Wedge F
-  End-as-Limit : (end : End F) → (l : Limit (Twist C D F)) → End.wedge end ≅ F₀ F⇒ (Limit.terminal.⊤ l)
+  End-as-Limit : (end : ∫ F) → (l : Limit (Twist C D F)) → ∫.wedge end ≅ F₀ F⇒ (Limit.terminal.⊤ l)
   End-as-Limit end l = Terminal.up-to-iso (Wedges.Wedges F) (End⇒Terminal F end) (pres-Terminal Eq terminal)
     where
     open Limit l
 
   -- Which then induces that the objects, in D, are also equivalent.
-  End-as-Limit-on-Obj : (end : End F) → (l : Limit (Twist C D F)) → End.E end O.≅ Limit.apex l
+  End-as-Limit-on-Obj : (end : ∫ F) → (l : Limit (Twist C D F)) → ∫.E end O.≅ Limit.apex l
   End-as-Limit-on-Obj end l = record
     { from = Wedge-Morphism.u (M._≅_.from X≅Y)
     ; to = Wedge-Morphism.u (M._≅_.to X≅Y)
@@ -164,3 +144,112 @@ module _ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ 
     where
       X≅Y = End-as-Limit end l
       open Category D
+module _ {F : Bifunctor (Category.op C) C D} (ω₁ ω₂ : ∫ F) where
+  private
+    module ω₁ = ∫ ω₁
+    module ω₂ = ∫ ω₂
+  open Category D
+  open M D
+  open _≅_
+  open Iso
+  open MR D
+  open HomReasoning
+
+  end-unique : ∫.E ω₁ ≅ ∫.E ω₂
+  end-unique .to = ω₁.factor ω₂.wedge
+  end-unique .from = ω₂.factor ω₁.wedge
+  end-unique .iso .isoʳ = ω₂.unique′ $ pullˡ ω₂.universal ○ ω₁.universal ○ ⟺ identityʳ
+  end-unique .iso .isoˡ = ω₁.unique′ $ pullˡ ω₁.universal ○ ω₂.universal ○ ⟺ identityʳ
+
+module _ {C : Category o ℓ e } {D : Category o′ ℓ′ e′} where
+  open MR D
+  private
+    open module D = Category D
+    module C = Category C
+    variable
+     F G H : Functor ((Category.op C) ×ᶜ C) D
+  open HomReasoning
+  open NaturalTransformation using (η)
+
+  opaque
+    unfolding end-η
+
+    -- "Partial functorality"
+    end-identity : {{ef : ∫ F}} → end-η (idN {F = F}) ≈ id
+    end-identity {F = F} {{ef}} = ∫.unique ef id-comm
+
+    end-η-commute : {{ef : ∫ F}} {{eg : ∫ G}} (α : NaturalTransformation F G) → 
+                    (c : C.Obj) → ∫.dinatural.α eg c ∘ end-η α ≈ α .η (c , c) ∘ ∫.dinatural.α ef c
+    end-η-commute ⦃ _ ⦄ ⦃ eg ⦄ α c = ∫.universal eg
+
+    end-η-resp-≈ : {{ef : ∫ F}} {{eg : ∫ G}} {α β : NaturalTransformation F G} →
+                   α ≃ⁿ β → end-η α ≈ end-η β
+    end-η-resp-≈ {{ef}} {{eg}} e = ∫.unique eg $ ∫.universal eg ○ ⟺ e ⟩∘⟨refl
+
+    end-η-resp-∘ : (α : NaturalTransformation F G) (β : NaturalTransformation G H)
+                   {{ef : ∫ F}} {{eg : ∫ G}} {{eh : ∫ H}} →
+                   end-η (β ∘ᵥ α) ≈ end-η β ∘ end-η α
+    end-η-resp-∘ α β {{ef}} {{eg}} {{eh}} = eh.unique $ extendʳ eh.universal ○ refl⟩∘⟨ eg.universal ○ sym-assoc
+      where module eg = ∫ eg
+            module eh = ∫ eh
+
+module _ {F G : Functor ((Category.op C) ×ᶜ C) D} (F≃G : F ≃ⁱ G) {{ef : ∫ F}} {{eg : ∫ G}} where
+  open Category D
+  open M D
+  open _≅_
+  open Iso
+  open HomReasoning
+  open module F≃G = NaturalIsomorphism F≃G
+  -- a duplicate proof of [_]-resp-≅ for the "partial" case
+  end-resp-≅ : ∫.E ef ≅ ∫.E eg
+  end-resp-≅ .to = end-η F⇐G
+  end-resp-≅ .from = end-η F⇒G
+  end-resp-≅ .iso .isoʳ = ⟺ (end-η-resp-∘ F⇐G F⇒G) ○ end-η-resp-≈ {α = F⇒G ∘ᵥ F⇐G} {β = idN} (λ {x} → F≃G.iso.isoʳ x) ○ end-identity {F = G}
+  end-resp-≅ .iso .isoˡ = ⟺ (end-η-resp-∘ F⇒G F⇐G) ○ end-η-resp-≈ {α = F⇐G ∘ᵥ F⇒G} {β = idN} (λ {x} → F≃G.iso.isoˡ x) ○ end-identity {F = F}
+
+  -- but really we would like something stronger---that ef implies eg and vice versa
+module _ {F G : Functor ((Category.op C) ×ᶜ C) D} (F≃G : F ≃ⁱ G) where
+  ≅-yields-end : ∫ F → ∫ G
+  ≅-yields-end ef = limit-yields-End G (≃-resp-lim (Twistⁿⁱ C D F≃G) (End-yields-limit F ef))
+
+-- continuous functors preserve ends
+module _ {C : Category o ℓ e}
+         (J : Bifunctor (Category.op C) C D) (F : Functor D E)
+         {cont : Continuous (o ⊔ ℓ) (ℓ ⊔ e) e F} where
+  open Category E
+  open M E
+  open _≅_
+  open Iso
+  open ∫ hiding (E)
+  private
+    module F = Functor F
+    module J = Bifunctor J
+    module E = Category E
+  -- i don't have a better name for this
+  -- the converse follows only if J reflects limits
+  open import Categories.Diagram.Cone.Properties
+  open import Categories.Diagram.Limit.Properties
+
+  module _ (ej : ∫ J) where
+    private
+      module ej = ∫ ej
+      j-limit : Limit (Twist C D J)
+      j-limit = End-yields-limit J ej
+      --new-limit
+      f-limit : Limit (F ∘F (J ∘F Forget C))
+      f-limit .Limit.terminal = record
+        { ⊤ = F-map-Coneˡ F (Limit.limit j-limit)
+        ; ⊤-is-terminal = cont j-limit
+        }
+      -- for this we merely need to transport across the associator
+      f-limit′ : Limit (Twist C E (F ∘F J))
+      f-limit′ = ≃-resp-lim (sym-associator (Forget C) J F) f-limit
+
+    -- really we want IsEnd `F.₀ (∫.E ej)` (F ∘F J)
+    contF-as-end : ∫ (F ∘F J)
+    contF-as-end = limit-yields-End (F ∘F J) f-limit′
+    _ : F.₀ (∫.E ej) ≅ (∫.E contF-as-end)
+    _ =  ≅.refl
+
+  Continuous-pres-End : {ej : ∫ J} {ef : ∫ (F ∘F J)} → F.₀ (∫.E ej) ≅ ∫.E ef
+  Continuous-pres-End {ej} {ef} = end-unique (contF-as-end ej) ef
diff --git a/src/Categories/Functor/Bifunctor.agda b/src/Categories/Functor/Bifunctor.agda
index 08640262c..be8a4786e 100644
--- a/src/Categories/Functor/Bifunctor.agda
+++ b/src/Categories/Functor/Bifunctor.agda
@@ -1,7 +1,4 @@
 {-# OPTIONS --without-K --safe #-}
-module Categories.Functor.Bifunctor where
-
--- Bifunctor, aka a Functor from C × D to E
 open import Level
 open import Data.Product using (_,_)
 
@@ -10,6 +7,10 @@ open import Categories.Functor
 open import Categories.Functor.Construction.Constant
 open import Categories.Category.Product
 
+module Categories.Functor.Bifunctor where
+
+-- Bifunctor, aka a Functor from C × D to E
+
 private
   variable
     o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴ o⁗ ℓ⁗ e⁗ : Level
diff --git a/src/Categories/Functor/Bifunctor/Properties.agda b/src/Categories/Functor/Bifunctor/Properties.agda
index 43ddc7b10..f60e01e64 100644
--- a/src/Categories/Functor/Bifunctor/Properties.agda
+++ b/src/Categories/Functor/Bifunctor/Properties.agda
@@ -6,8 +6,12 @@ open import Level
 open import Data.Product using (Σ; _,_)
 
 open import Categories.Category
+open import Categories.Category.Product
 open import Categories.Functor
 open import Categories.Functor.Bifunctor
+open import Categories.Functor.Construction.Constant
+open import Categories.NaturalTransformation using (NaturalTransformation; _∘ˡ_) renaming (id to idN)
+
 import Categories.Morphism.Reasoning as MR
 
 private
diff --git a/src/Categories/Functor/Instance/Twisted.agda b/src/Categories/Functor/Instance/Twisted.agda
index 3088328fe..b88c861b5 100644
--- a/src/Categories/Functor/Instance/Twisted.agda
+++ b/src/Categories/Functor/Instance/Twisted.agda
@@ -1,62 +1,39 @@
 {-# OPTIONS --without-K --safe #-}
-open import Categories.Category using (Category; module Definitions)
 
--- Definition of the "Twisted" Functor between certain Functor Categories
-module Categories.Functor.Instance.Twisted {o ℓ e o′ ℓ′ e′} (𝒞 : Category o ℓ e) (𝒟 : Category o′ ℓ′ e′) where
+open import Level
+open import Data.Product using (_,_)
 
-import Categories.Category.Construction.TwistedArrow as TW
-open import Categories.Category.Product
+open import Categories.Category using (Category; module Definitions)
+
+open import Categories.Category.Construction.TwistedArrow
+open import Categories.Category.Product renaming (Product to _×ᶜ_)
 open import Categories.Category.Construction.Functors
 open import Categories.Functor
+open import Categories.Functor.Bifunctor
 open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; _ⓘʳ_)
+open import Categories.Functor.Limits using (Continuous)
 
-open import Data.Product using (_,_)
+
+-- Definition of the "Twisted" Functor between certain Functor Categories
+module Categories.Functor.Instance.Twisted {o ℓ e o′ ℓ′ e′} (C : Category o ℓ e) (D : Category o′ ℓ′ e′)where
 
 private
-  module C = Category 𝒞
-
-Twist : Functor (Product C.op 𝒞) 𝒟 → Functor (TW.TwistedArrow 𝒞) 𝒟
-Twist F = record
-  { F₀ = λ x → F₀ (dom x , cod x)
-  ; F₁ = λ f → F₁ (dom⇐ f , cod⇒ f)
-  ; identity = identity
-  ; homomorphism = homomorphism
-  ; F-resp-≈ = F-resp-≈
-  }
-  where
-  open Functor F
-  open TW.Morphism
-  open TW.Morphism⇒
-
-Twist′ : Functor (Product C.op 𝒞) 𝒟 → Functor (Category.op (TW.TwistedArrow C.op)) 𝒟
-Twist′ F = record
-  { F₀ = λ x → F₀ (dom x , cod x)
-  ; F₁ = λ f → F₁ (dom⇐ f , cod⇒ f)
-  ; identity = identity
-  ; homomorphism = homomorphism
-  ; F-resp-≈ = F-resp-≈
-  }
-  where
-  open Functor F
-  open TW.Morphism
-  open TW.Morphism⇒
-
-Twisted : Functor (Functors (Product C.op 𝒞) 𝒟) (Functors (TW.TwistedArrow 𝒞) 𝒟)
-Twisted = record
-  { F₀ = Twist
-  ; F₁ = Nat
-  ; identity = D.Equiv.refl
-  ; homomorphism = D.Equiv.refl
-  ; F-resp-≈ = λ f≈g → f≈g
-  }
-  where
-  open TW.Morphism
-  open TW.Morphism⇒
-  module D = Category 𝒟
-  Nat : {F G : Functor (Product C.op 𝒞) 𝒟} → NaturalTransformation F G → NaturalTransformation (Twist F) (Twist G)
-  Nat nt = ntHelper record
-    { η = λ x → η nt (dom x , cod x)
-    ; commute = λ f → commute nt (dom⇐ f , cod⇒ f)
-    }
-    where
-    open NaturalTransformation
+  module C = Category C
+  module D = Category D
+
+open Morphism
+open Morphism⇒
+-- precomposition with the forgetful functor
+Twist : Functor (C.op ×ᶜ C) D → Functor (TwistedArrow C) D
+Twist F = F ∘F Forget C
+
+Twist′ : Functor (C.op ×ᶜ C) D → Functor (Category.op (TwistedArrow C.op)) D
+Twist′ F = F ∘F (Functor.op (Forget C.op))
+
+-- precomposition is functorial
+Twisted : Functor (Functors (C.op ×ᶜ C) D) (Functors (TwistedArrow C) D)
+Twisted = appʳ product (Forget C)
+
+Twistⁿⁱ : ∀ {F G : Functor (C.op ×ᶜ C) D } → (F ≃ G) → Twist F ≃ Twist G
+Twistⁿⁱ α = α ⓘʳ Forget C
diff --git a/src/Categories/NaturalTransformation/Equivalence.agda b/src/Categories/NaturalTransformation/Equivalence.agda
index fd27ebe9c..ca6d937b6 100644
--- a/src/Categories/NaturalTransformation/Equivalence.agda
+++ b/src/Categories/NaturalTransformation/Equivalence.agda
@@ -1,8 +1,5 @@
 {-# OPTIONS --without-K --safe #-}
 
--- define a less-than-great equivalence on natural transformations
-module Categories.NaturalTransformation.Equivalence where
-
 open import Level
 open import Relation.Binary using (Rel; IsEquivalence; Setoid)
 
@@ -10,27 +7,27 @@ open import Categories.Category
 open import Categories.Functor
 open import Categories.NaturalTransformation.Core
 
-private
-  variable
-    o ℓ e o′ ℓ′ e′ : Level
-    C D E : Category o ℓ e
-
--- This ad hoc equivalence for NaturalTransformation should really be 'modification'
---  (yep, tricategories!). What is below is only part of the definition of a 'modification'.  TODO
-infix 4 _≃_
-
-_≃_ : ∀ {F G : Functor C D} → Rel (NaturalTransformation F G) _
-_≃_ {D = D} X Y = ∀ {x} → D [ NaturalTransformation.η X x ≈ NaturalTransformation.η Y x ]
-
-≃-isEquivalence : ∀ {F G : Functor C D} → IsEquivalence (_≃_ {F = F} {G})
-≃-isEquivalence {D = D} {F} {G} = record
-  { refl  = refl
-  ; sym   = λ f → sym f -- need to eta-expand to get things to line up properly
-  ; trans = λ f g → trans f g
-  }
-  where open Category.Equiv D
-
-≃-setoid : ∀ (F G : Functor C D) → Setoid _ _
+-- define a less-than-great equivalence on natural transformations
+module Categories.NaturalTransformation.Equivalence {o ℓ e o′ ℓ′ e′ : Level}
+    {C : Category o ℓ e} {D : Category o′ ℓ′ e′} where
+
+module _ {F G : Functor C D} where
+  infix 4 _≃_
+  open Category.Equiv D
+
+  -- This ad hoc equivalence for NaturalTransformation should really be 'modification'
+  --  (yep, tricategories!). What is below is only part of the definition of a 'modification'.  TODO
+  _≃_ : Rel (NaturalTransformation F G) (o ⊔ e′)
+  _≃_ X Y = ∀ {x} → D [ NaturalTransformation.η X x ≈ NaturalTransformation.η Y x ]
+
+  ≃-isEquivalence : IsEquivalence _≃_
+  ≃-isEquivalence = record
+    { refl  = refl
+    ; sym   = λ f → sym f -- need to eta-expand to get things to line up properly
+    ; trans = λ f g → trans f g
+    }
+
+≃-setoid : ∀ (F G : Functor C D) → Setoid (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) (o ⊔ e′)
 ≃-setoid F G = record
   { Carrier       = NaturalTransformation F G
   ; _≈_           = _≃_

From 20ffc64f372ec139b7877bb9e1721264107d5355 Mon Sep 17 00:00:00 2001
From: Calvin Lee <pounce@integraldoma.in>
Date: Fri, 14 Jun 2024 13:33:17 +0000
Subject: [PATCH 2/5] add --safe

---
 src/Categories/Diagram/End/Fubini.agda        | 2 +-
 src/Categories/Diagram/End/Parameterized.agda | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Categories/Diagram/End/Fubini.agda b/src/Categories/Diagram/End/Fubini.agda
index d5be65ed8..8bcef78d7 100644
--- a/src/Categories/Diagram/End/Fubini.agda
+++ b/src/Categories/Diagram/End/Fubini.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K --lossy-unification #-}
+{-# OPTIONS --without-K --lossy-unification --safe #-}
 
 open import Level
 open import Data.Product using (Σ; _,_; _×_) renaming (proj₁ to fst; proj₂ to snd)
diff --git a/src/Categories/Diagram/End/Parameterized.agda b/src/Categories/Diagram/End/Parameterized.agda
index d504cb159..85f971106 100644
--- a/src/Categories/Diagram/End/Parameterized.agda
+++ b/src/Categories/Diagram/End/Parameterized.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --safe #-}
 module Categories.Diagram.End.Parameterized where
 
 open import Level

From 38923f126232a09d17f0b507a5ac4f3f71892d3f Mon Sep 17 00:00:00 2001
From: Calvin Lee <pounce@integraldoma.in>
Date: Sat, 15 Jun 2024 10:07:35 +0000
Subject: [PATCH 3/5] adjust naming

---
 src/Categories/Diagram/End/Parameterized.agda | 77 +++++++++----------
 1 file changed, 37 insertions(+), 40 deletions(-)

diff --git a/src/Categories/Diagram/End/Parameterized.agda b/src/Categories/Diagram/End/Parameterized.agda
index 85f971106..4dd289ea6 100644
--- a/src/Categories/Diagram/End/Parameterized.agda
+++ b/src/Categories/Diagram/End/Parameterized.agda
@@ -153,18 +153,35 @@ module _ {C : Category o ℓ e}
     }
   --module appˡ-resp-∘ X = NaturalIsomorphism (appˡ-resp-∘ X)
 
-  Continuous-preserve-endf-motive : ∀ X → ∫ (appˡ (F ∘F J) X)
-  Continuous-preserve-endf-motive X = ≅-yields-end (appˡ-resp-∘ X) (contF-as-end (appˡ J X) F {cont} (ω X))
-
   open NaturalTransformation using (η)
+  open MR E
 
-  private
-    ω' = Continuous-preserve-endf-motive
-    module ω' (X : P.Obj) = ∫ (ω' X)
-    --module EndF {A B} (J : Functor A B) {ω} = Functor (EndF J {ω})
+  Fω : ∀ X → ∫ (appˡ (F ∘F J) X)
+  Fω X = ≅-yields-end (appˡ-resp-∘ X) (contF-as-end (appˡ J X) F {cont} (ω X))
+  module Fω (p : P.Obj) = ∫ (Fω p)
+
+  Fω≈Fω : ∀ {p : P.Obj} {c : C.Obj} → Fω.dinatural.α p c ≈ F.₁ (ω.dinatural.α p c)
+  Fω≈Fω {p} {A} = begin
+    Fω.dinatural.α p A
+      ≡⟨⟩
+    id ∘ F₁ (J₁ (P.id , C.id , C.id)) ∘
+    id ∘ F₁ (J₁ (P.id , C.id , C.id) D.∘ ω.dinatural.α p A)
+      ≈⟨ identityˡ ⟩
+    F₁ (J₁ (P.id , C.id , C.id)) ∘
+    id ∘ F₁ (J₁ (P.id , C.id , C.id) D.∘ ω.dinatural.α p A)
+      ≈⟨ F-resp-≈ J.identity ⟩∘⟨refl ⟩
+    F₁ (D.id) ∘ id ∘ F₁ (J₁ (P.id , C.id , C.id) D.∘ ω.dinatural.α p A)
+      ≈⟨ elimˡ F.identity ⟩
+    id ∘ F₁ (J₁ (P.id , C.id , C.id) D.∘ ω.dinatural.α p A)
+      ≈⟨ identityˡ ⟩
+    F₁ (J₁ (P.id , C.id , C.id) D.∘ ω.dinatural.α p A)
+      ≈⟨ F-resp-≈ (D.∘-resp-≈ˡ J.identity) ⟩
+    F₁ (D.id D.∘ ω.dinatural.α p A)
+      ≈⟨ F-resp-≈ D.identityˡ ⟩
+    F₁ (ω.dinatural.α p A) 
+      ∎
 
-  open MR E
-  Continuous-pres-EndF :  F ∘F (EndF J {ω}) ≃ⁱ EndF (F ∘F J) {ω'}
+  Continuous-pres-EndF :  F ∘F (EndF J {ω}) ≃ⁱ EndF (F ∘F J) {Fω}
   Continuous-pres-EndF = niHelper record
     { η = λ X → E.id
     ; η⁻¹ = λ Y → E.id
@@ -172,9 +189,9 @@ module _ {C : Category o ℓ e}
       id ∘ Functor.F₁ (F ∘F EndF J {ω}) f ≈⟨ identityˡ ⟩
       Functor.F₁ (F ∘F EndF J {ω}) f      ≡⟨⟩
       F₁ (end-η (appˡJ.₁ f) ⦃ ω p ⦄ ⦃ ω q ⦄)
-        ≈⟨ ω'.unique′ q (λ {A} → begin
-          ω'.dinatural.α q A ∘ F₁ (end-η (appˡJ.₁ f) ⦃ ω p ⦄ ⦃ ω q ⦄)
-            ≈⟨ lemma ⟩∘⟨refl ⟩
+        ≈⟨ Fω.unique′ q (λ {A} → begin
+          Fω.dinatural.α q A ∘ F₁ (end-η (appˡJ.₁ f) ⦃ ω p ⦄ ⦃ ω q ⦄)
+            ≈⟨ Fω≈Fω ⟩∘⟨refl ⟩
           F₁ (ω.dinatural.α q A) ∘ F₁ (end-η (appˡJ.₁ f) ⦃ ω p ⦄ ⦃ ω q ⦄)
             ≈˘⟨ F.homomorphism ⟩
           F₁ (ω.dinatural.α q A D.∘ end-η (appˡJ.₁ f) ⦃ ω p ⦄ ⦃ ω q ⦄)
@@ -182,18 +199,18 @@ module _ {C : Category o ℓ e}
           F₁ ((appˡJ.₁ f) .η (A , A) D.∘ (ω.dinatural.α p A))
             ≈⟨ F.homomorphism ⟩
           F₁ ((appˡJ.₁ f) .η (A , A)) ∘ F₁ (ω.dinatural.α p A)
-            ≈˘⟨ refl⟩∘⟨ lemma ⟩
-          F₁ ((appˡJ.₁ f) .η (A , A)) ∘ (ω'.dinatural.α p A)
+            ≈˘⟨ refl⟩∘⟨ Fω≈Fω ⟩
+          F₁ ((appˡJ.₁ f) .η (A , A)) ∘ (Fω.dinatural.α p A)
             ≡⟨⟩
-          appˡFJ.₁ f .η (A , A) ∘ ω'.dinatural.α p A
-            ≈˘⟨ end-η-commute ⦃ ω' p ⦄ ⦃ ω' q ⦄ (appˡFJ.₁ f) A ⟩
-          ω'.dinatural.α q A ∘ end-η (appˡFJ.₁ f) ⦃ ω' p ⦄ ⦃ ω' q ⦄
+          appˡFJ.₁ f .η (A , A) ∘ Fω.dinatural.α p A
+            ≈˘⟨ end-η-commute ⦃ Fω p ⦄ ⦃ Fω q ⦄ (appˡFJ.₁ f) A ⟩
+          Fω.dinatural.α q A ∘ end-η (appˡFJ.₁ f) ⦃ Fω p ⦄ ⦃ Fω q ⦄
             ∎
         )⟩
-      end-η (appˡFJ.₁ f) ⦃ ω' p ⦄ ⦃ ω' q ⦄
+      end-η (appˡFJ.₁ f) ⦃ Fω p ⦄ ⦃ Fω q ⦄
         ≡⟨⟩
-      Functor.F₁ (EndF (F ∘F J) {ω'}) f   ≈˘⟨ identityʳ ⟩
-      Functor.F₁ (EndF (F ∘F J) {ω'}) f ∘ id
+      Functor.F₁ (EndF (F ∘F J) {Fω}) f   ≈˘⟨ identityʳ ⟩
+      Functor.F₁ (EndF (F ∘F J) {Fω}) f ∘ id
         ∎
     ; iso = λ Y → record
       { isoˡ = E.identity²
@@ -201,23 +218,3 @@ module _ {C : Category o ℓ e}
       }
     }
     where open E.HomReasoning
-          lemma : ∀ {q A} → ω'.dinatural.α q A ≈ F₁ (ω.dinatural.α q A)
-          lemma {q} {A} = begin
-            ω'.dinatural.α q A
-              ≡⟨⟩
-            id ∘ F₁ (J₁ (P.id , C.id , C.id)) ∘
-            id ∘ F₁ (J₁ (P.id , C.id , C.id) D.∘ ω.dinatural.α q A)
-              ≈⟨ identityˡ ⟩
-            F₁ (J₁ (P.id , C.id , C.id)) ∘
-            id ∘ F₁ (J₁ (P.id , C.id , C.id) D.∘ ω.dinatural.α q A)
-              ≈⟨ F-resp-≈ J.identity ⟩∘⟨refl ⟩
-            F₁ (D.id) ∘ id ∘ F₁ (J₁ (P.id , C.id , C.id) D.∘ ω.dinatural.α q A)
-              ≈⟨ elimˡ F.identity ⟩
-            id ∘ F₁ (J₁ (P.id , C.id , C.id) D.∘ ω.dinatural.α q A)
-              ≈⟨ identityˡ ⟩
-            F₁ (J₁ (P.id , C.id , C.id) D.∘ ω.dinatural.α q A)
-              ≈⟨ F-resp-≈ (D.∘-resp-≈ˡ J.identity) ⟩
-            F₁ (D.id D.∘ ω.dinatural.α q A)
-              ≈⟨ F-resp-≈ D.identityˡ ⟩
-            F₁ (ω.dinatural.α q A) 
-              ∎

From ce6a7b6219218ac15bf218616eb99967b8e94701 Mon Sep 17 00:00:00 2001
From: Calvin Lee <pounce@integraldoma.in>
Date: Tue, 25 Jun 2024 14:05:51 +0000
Subject: [PATCH 4/5] adjust imports

---
 .../Category/Construction/Functors.agda       |  6 +++
 .../Category/Construction/TwistedArrow.agda   | 43 +++++++---------
 src/Categories/Diagram/End/Fubini.agda        | 28 +++++-----
 src/Categories/Diagram/End/Properties.agda    | 51 +++++++++----------
 src/Categories/Functor/Bifunctor.agda         |  8 +--
 .../Functor/Bifunctor/Properties.agda         |  3 --
 src/Categories/Functor/Instance/Twisted.agda  | 32 ++++++------
 .../NaturalTransformation/Equivalence.agda    | 13 ++---
 8 files changed, 90 insertions(+), 94 deletions(-)

diff --git a/src/Categories/Category/Construction/Functors.agda b/src/Categories/Category/Construction/Functors.agda
index 33505936d..d6f1d1e87 100644
--- a/src/Categories/Category/Construction/Functors.agda
+++ b/src/Categories/Category/Construction/Functors.agda
@@ -188,6 +188,12 @@ uncurry {C₁ = C₁} {C₂ = C₂} {D = D} = record
           } where module t = NaturalTransformation t
                   open NaturalTransformation
 
+module uncurry {o₁ e₁ ℓ₁} {C₁ : Category o₁ e₁ ℓ₁}
+               {o₂ e₂ ℓ₂} {C₂ : Category o₂ e₂ ℓ₂}
+               {o′ e′ ℓ′} {D  : Category o′ e′ ℓ′}
+               where
+  open Functor (uncurry {C₁ = C₁} {C₂ = C₂} {D = D}) public
+
 module _ {o₁ e₁ ℓ₁} {C₁ : Category o₁ e₁ ℓ₁}
          {o₂ e₂ ℓ₂} {C₂ : Category o₂ e₂ ℓ₂}
          {o′ e′ ℓ′} {D  : Category o′ e′ ℓ′} where
diff --git a/src/Categories/Category/Construction/TwistedArrow.agda b/src/Categories/Category/Construction/TwistedArrow.agda
index 411dba6a8..772db92e8 100644
--- a/src/Categories/Category/Construction/TwistedArrow.agda
+++ b/src/Categories/Category/Construction/TwistedArrow.agda
@@ -1,28 +1,25 @@
 {-# OPTIONS --without-K --safe #-}
-open import Data.Product using (_,_; _×_; map; zip)
-open import Function.Base using (_$_; flip)
-open import Level
-open import Relation.Binary.Core using (Rel)
 
 open import Categories.Category using (Category; module Definitions)
-open import Categories.Category.Product renaming (Product to _×ᶜ_)
-open import Categories.Functor
-
-import Categories.Morphism as M
-import Categories.Morphism.Reasoning as MR
 
 -- Definition of the "Twisted Arrow" Category of a Category 𝒞
 module Categories.Category.Construction.TwistedArrow {o ℓ e} (𝒞 : Category o ℓ e) where
 
-private
-  open module 𝒞 = Category 𝒞
+open import Level
+open import Data.Product using (_,_; _×_; map; zip)
+open import Function.Base using (_$_; flip)
+open import Relation.Binary.Core using (Rel)
 
+open import Categories.Category.Product renaming (Product to _×ᶜ_)
+open import Categories.Functor using (Functor)
+open import Categories.Morphism.Reasoning 𝒞 using (pullˡ; pullʳ )
 
-open M 𝒞
+private
+  open module 𝒞 = Category 𝒞
 open Definitions 𝒞
-open MR 𝒞
 open HomReasoning
 
+
 private
   variable
     A B C : Obj
@@ -78,14 +75,12 @@ TwistedArrow = record
 
 -- Consider TwistedArrow as the comma category * / Hom[C][-,-]
 -- We have the codomain functor TwistedArrow → C.op × C
-
-module _ where
-  open Morphism
-  open Morphism⇒
-  open Functor
-  Forget : Functor TwistedArrow (𝒞.op ×ᶜ 𝒞)
-  Forget .F₀ x = dom x , cod x
-  Forget .F₁ f = dom⇐ f , cod⇒ f
-  Forget .identity = Equiv.refl , Equiv.refl
-  Forget .homomorphism = Equiv.refl , Equiv.refl
-  Forget .F-resp-≈ e = e
+open Functor
+Codomain : Functor TwistedArrow (𝒞.op ×ᶜ 𝒞)
+Codomain .F₀ x = dom , cod
+  where open Morphism x
+Codomain .F₁ f = dom⇐ , cod⇒
+  where open Morphism⇒ f
+Codomain .identity = Equiv.refl , Equiv.refl
+Codomain .homomorphism = Equiv.refl , Equiv.refl
+Codomain .F-resp-≈ e = e
diff --git a/src/Categories/Diagram/End/Fubini.agda b/src/Categories/Diagram/End/Fubini.agda
index 8bcef78d7..97c03feb3 100644
--- a/src/Categories/Diagram/End/Fubini.agda
+++ b/src/Categories/Diagram/End/Fubini.agda
@@ -1,26 +1,26 @@
 {-# OPTIONS --without-K --lossy-unification --safe #-}
 
+module Categories.Diagram.End.Fubini where
+
 open import Level
 open import Data.Product using (Σ; _,_; _×_) renaming (proj₁ to fst; proj₂ to snd)
 open import Function using (_$_)
 
-open import Categories.Category
-open import Categories.Category.Construction.Functors
-open import Categories.Category.Product renaming (Product to _×ᶜ_)
+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 ∫)
-open import Categories.Diagram.End.Properties
-open import Categories.Diagram.End.Parameterized renaming (EndF to ⨏)
-open import Categories.Diagram.Wedge
-open import Categories.Functor renaming (id to idF)
-open import Categories.Functor.Bifunctor
-open import Categories.Functor.Bifunctor.Properties
+open import Categories.Diagram.End.Properties using (end-η-commute; end-unique)
+open import Categories.Diagram.End.Parameterized using () renaming (EndF to ⨏)
+open import Categories.Diagram.Wedge using (Wedge)
+open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
+open import Categories.Functor.Bifunctor using (Bifunctor; appˡ)
 open import Categories.NaturalTransformation using (NaturalTransformation)
-open import Categories.NaturalTransformation.Dinatural
+open import Categories.NaturalTransformation.Dinatural using (DinaturalTransformation; dtHelper)
 
 import Categories.Morphism as M
 import Categories.Morphism.Reasoning as MR
 
-module Categories.Diagram.End.Fubini where
 variable
   o ℓ e : Level
   C P D : Category o ℓ e
@@ -82,7 +82,7 @@ module _  (F : Bifunctor (Category.op C ×ᶜ Category.op P) (C ×ᶜ P) D)
           (F₁ ((C.id , P.id) , (C.id , s)) ∘ F₁ ((C.id , P.id) , (f , P.id)) ∘ ω.dinatural.α (p , p) c) ∘ ρ.dinatural.α 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
-            ≈⟨ (refl⟩∘⟨ ω.dinatural.commute (p , p) f ) ⟩∘⟨refl ⟩
+            ≈⟨ (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
             ≈⟨ 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
@@ -93,7 +93,7 @@ module _  (F : Bifunctor (Category.op C ×ᶜ Category.op P) (C ×ᶜ P) D)
           -- 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 )) ⟩
+            ≈⟨ 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
             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨  ⟺ identityʳ ⟩
@@ -201,6 +201,6 @@ module _ (F : Bifunctor (Category.op C ×ᶜ Category.op P) (C ×ᶜ P) D)
     eₚ′′  .∫.unique {W} {g} h = eₚ.unique F h
 
   Fubini′ : ∫.E e₁ ≅ ∫.E e₂
-  Fubini′ = ≅.trans (Fubini F {ωᴾ} {eₚ' = eₚ F} ) $
+  Fubini′ = ≅.trans (Fubini F {ωᴾ} {eₚ' = eₚ F}) $
             ≅.trans (end-unique eₚ′′ (eₚ (F ′′)))
                     (≅.sym (Fubini (F ′′) {ωᶜ} {eₚ' = eₚ (F ′′)}))
diff --git a/src/Categories/Diagram/End/Properties.agda b/src/Categories/Diagram/End/Properties.agda
index daaeb4803..b6f60547c 100644
--- a/src/Categories/Diagram/End/Properties.agda
+++ b/src/Categories/Diagram/End/Properties.agda
@@ -2,43 +2,40 @@
 
 module Categories.Diagram.End.Properties where
 
+-- The following conventions are taken in this file: C is the 'source' category
+-- and D is the destination. If two source categories are needed, the other is
+-- called 'P' for "parameter", following MacLane. F, G and H are functors and ef,
+-- eg and eh are witnesses of their respective ends.
+
 open import Level
 open import Data.Product using (Σ; _,_)
 open import Function using (_$_)
 
-open import Categories.Category
-open import Categories.Category.Construction.Functors
-open import Categories.Category.Construction.TwistedArrow
+open import Categories.Category using (Category)
+open import Categories.Category.Construction.Functors using (Functors)
+open import Categories.Category.Construction.TwistedArrow using (Codomain)
 open import Categories.Category.Equivalence as SE using (StrongEquivalence)
-open import Categories.Category.Equivalence.Preserves
-open import Categories.Category.Product renaming (Product to _×ᶜ_)
-open import Categories.Diagram.Cone
-open import Categories.Diagram.End renaming (End to ∫)
-open import Categories.Diagram.Limit
-open import Categories.Diagram.Limit.Properties
-open import Categories.Diagram.Wedge
-open import Categories.Diagram.Wedge.Properties
-open import Categories.Functor hiding (id)
-open import Categories.Functor.Bifunctor
-open import Categories.Functor.Bifunctor.Properties
-open import Categories.Functor.Instance.Twisted
-open import Categories.Functor.Limits
-open import Categories.NaturalTransformation renaming (_∘ʳ_ to _▹ⁿ_; id to idN)
+open import Categories.Category.Equivalence.Preserves using (pres-Terminal)
+open import Categories.Category.Product using () renaming (Product to _×ᶜ_)
+open import Categories.Diagram.End using () renaming (End to ∫)
+open import Categories.Diagram.Limit using (Limit)
+open import Categories.Diagram.Limit.Properties using (≃-resp-lim)
+open import Categories.Diagram.Wedge using (Wedge; module Wedge-Morphism)
+open import Categories.Diagram.Wedge.Properties using (ConesTwist≅Wedges)
+open import Categories.Functor using (Functor; _∘F_)
+open import Categories.Functor.Bifunctor using (Bifunctor)
+open import Categories.Functor.Instance.Twisted using (Twist; Twistⁿⁱ)
+open import Categories.Functor.Limits using (Continuous)
+open import Categories.NaturalTransformation using (NaturalTransformation; _∘ᵥ_) renaming (_∘ʳ_ to _▹ⁿ_; id to idN)
 open import Categories.NaturalTransformation.Dinatural hiding (_≃_)
-open import Categories.NaturalTransformation.Equivalence renaming (_≃_ to _≃ⁿ_)
-open import Categories.NaturalTransformation.NaturalIsomorphism renaming (_≃_ to _≃ⁱ_)
-open import Categories.NaturalTransformation.NaturalIsomorphism.Properties
+open import Categories.NaturalTransformation.Equivalence using () renaming (_≃_ to _≃ⁿ_)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; sym-associator) renaming (_≃_ to _≃ⁱ_)
 open import Categories.Object.Terminal as Terminal
 
 import Categories.Category.Construction.Wedges as Wedges
 import Categories.Morphism as M
 import Categories.Morphism.Reasoning as MR
 
--- The following conventions are taken in this file: C is the 'source' category
--- and D is the destination. If two source categories are needed, the other is
--- called 'P' for "parameter", following MacLane. F, G and H are functors and ef,
--- eg and eh are witnesses of their respective ends.
-
 private
   variable
     o ℓ e o′ ℓ′ e′ : Level
@@ -236,14 +233,14 @@ module _ {C : Category o ℓ e}
       j-limit : Limit (Twist C D J)
       j-limit = End-yields-limit J ej
       --new-limit
-      f-limit : Limit (F ∘F (J ∘F Forget C))
+      f-limit : Limit (F ∘F (J ∘F Codomain C))
       f-limit .Limit.terminal = record
         { ⊤ = F-map-Coneˡ F (Limit.limit j-limit)
         ; ⊤-is-terminal = cont j-limit
         }
       -- for this we merely need to transport across the associator
       f-limit′ : Limit (Twist C E (F ∘F J))
-      f-limit′ = ≃-resp-lim (sym-associator (Forget C) J F) f-limit
+      f-limit′ = ≃-resp-lim (sym-associator (Codomain C) J F) f-limit
 
     -- really we want IsEnd `F.₀ (∫.E ej)` (F ∘F J)
     contF-as-end : ∫ (F ∘F J)
diff --git a/src/Categories/Functor/Bifunctor.agda b/src/Categories/Functor/Bifunctor.agda
index be8a4786e..4fa92a45b 100644
--- a/src/Categories/Functor/Bifunctor.agda
+++ b/src/Categories/Functor/Bifunctor.agda
@@ -1,4 +1,8 @@
 {-# OPTIONS --without-K --safe #-}
+
+-- Bifunctor, aka a Functor from C × D to E
+module Categories.Functor.Bifunctor where
+
 open import Level
 open import Data.Product using (_,_)
 
@@ -7,10 +11,6 @@ open import Categories.Functor
 open import Categories.Functor.Construction.Constant
 open import Categories.Category.Product
 
-module Categories.Functor.Bifunctor where
-
--- Bifunctor, aka a Functor from C × D to E
-
 private
   variable
     o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴ o⁗ ℓ⁗ e⁗ : Level
diff --git a/src/Categories/Functor/Bifunctor/Properties.agda b/src/Categories/Functor/Bifunctor/Properties.agda
index f60e01e64..3e563223e 100644
--- a/src/Categories/Functor/Bifunctor/Properties.agda
+++ b/src/Categories/Functor/Bifunctor/Properties.agda
@@ -6,11 +6,8 @@ open import Level
 open import Data.Product using (Σ; _,_)
 
 open import Categories.Category
-open import Categories.Category.Product
 open import Categories.Functor
 open import Categories.Functor.Bifunctor
-open import Categories.Functor.Construction.Constant
-open import Categories.NaturalTransformation using (NaturalTransformation; _∘ˡ_) renaming (id to idN)
 
 import Categories.Morphism.Reasoning as MR
 
diff --git a/src/Categories/Functor/Instance/Twisted.agda b/src/Categories/Functor/Instance/Twisted.agda
index b88c861b5..01951dfda 100644
--- a/src/Categories/Functor/Instance/Twisted.agda
+++ b/src/Categories/Functor/Instance/Twisted.agda
@@ -1,22 +1,21 @@
 {-# OPTIONS --without-K --safe #-}
 
+open import Categories.Category using (Category; module Definitions)
+
+-- Definition of the "Twisted" Functor between certain Functor Categories
+module Categories.Functor.Instance.Twisted {o ℓ e o′ ℓ′ e′} (C : Category o ℓ e) (D : Category o′ ℓ′ e′)where
+
 open import Level
 open import Data.Product using (_,_)
 
-open import Categories.Category using (Category; module Definitions)
-
-open import Categories.Category.Construction.TwistedArrow
-open import Categories.Category.Product renaming (Product to _×ᶜ_)
-open import Categories.Category.Construction.Functors
-open import Categories.Functor
-open import Categories.Functor.Bifunctor
+open import Categories.Category.Construction.Functors using (Functors; product)
+open import Categories.Category.Construction.TwistedArrow using (TwistedArrow; Morphism; Morphism⇒; Codomain)
+open import Categories.Category.Product using () renaming (Product to _×ᶜ_)
+open import Categories.Functor using (Functor; _∘F_)
+open import Categories.Functor.Bifunctor using (appʳ)
+open import Categories.Functor.Limits using (Continuous)
 open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
 open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; _ⓘʳ_)
-open import Categories.Functor.Limits using (Continuous)
-
-
--- Definition of the "Twisted" Functor between certain Functor Categories
-module Categories.Functor.Instance.Twisted {o ℓ e o′ ℓ′ e′} (C : Category o ℓ e) (D : Category o′ ℓ′ e′)where
 
 private
   module C = Category C
@@ -24,16 +23,17 @@ private
 
 open Morphism
 open Morphism⇒
+
 -- precomposition with the forgetful functor
 Twist : Functor (C.op ×ᶜ C) D → Functor (TwistedArrow C) D
-Twist F = F ∘F Forget C
+Twist F = F ∘F Codomain C
 
 Twist′ : Functor (C.op ×ᶜ C) D → Functor (Category.op (TwistedArrow C.op)) D
-Twist′ F = F ∘F (Functor.op (Forget C.op))
+Twist′ F = F ∘F (Functor.op (Codomain C.op))
 
 -- precomposition is functorial
 Twisted : Functor (Functors (C.op ×ᶜ C) D) (Functors (TwistedArrow C) D)
-Twisted = appʳ product (Forget C)
+Twisted = appʳ product (Codomain C)
 
 Twistⁿⁱ : ∀ {F G : Functor (C.op ×ᶜ C) D } → (F ≃ G) → Twist F ≃ Twist G
-Twistⁿⁱ α = α ⓘʳ Forget C
+Twistⁿⁱ α = α ⓘʳ Codomain C
diff --git a/src/Categories/NaturalTransformation/Equivalence.agda b/src/Categories/NaturalTransformation/Equivalence.agda
index ca6d937b6..5dfcfdfae 100644
--- a/src/Categories/NaturalTransformation/Equivalence.agda
+++ b/src/Categories/NaturalTransformation/Equivalence.agda
@@ -1,16 +1,17 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level
-open import Relation.Binary using (Rel; IsEquivalence; Setoid)
-
 open import Categories.Category
-open import Categories.Functor
-open import Categories.NaturalTransformation.Core
 
 -- define a less-than-great equivalence on natural transformations
-module Categories.NaturalTransformation.Equivalence {o ℓ e o′ ℓ′ e′ : Level}
+module Categories.NaturalTransformation.Equivalence {o ℓ e o′ ℓ′ e′}
     {C : Category o ℓ e} {D : Category o′ ℓ′ e′} where
 
+open import Level
+open import Relation.Binary using (Rel; IsEquivalence; Setoid)
+
+open import Categories.Functor using (Functor)
+open import Categories.NaturalTransformation.Core using (NaturalTransformation)
+
 module _ {F G : Functor C D} where
   infix 4 _≃_
   open Category.Equiv D

From 22d3550aabace66d731042e4ce01893f43b8d8a8 Mon Sep 17 00:00:00 2001
From: Calvin Lee <pounce@integraldoma.in>
Date: Wed, 19 Jun 2024 16:46:04 +0000
Subject: [PATCH 5/5] golf fubini proofs

---
 src/Categories/Diagram/End/Fubini.agda | 100 ++++++++++++++-----------
 1 file changed, 58 insertions(+), 42 deletions(-)

diff --git a/src/Categories/Diagram/End/Fubini.agda b/src/Categories/Diagram/End/Fubini.agda
index 97c03feb3..6f67e8ea6 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)