Merge pull request #451 from agda/coend-colimits

Copy over a couple of properties from ends to coends
agda · Feb 21, 2025 · 58c75ac · 58c75ac
2 parents 8509bc5 + 220588c
commit 58c75ac
Showing 1 changed file with 7 additions and 1 deletion.
diff --git a/src/Categories/Diagram/Coend/Properties.agda b/src/Categories/Diagram/Coend/Properties.agda
@@ -6,7 +6,7 @@ open import Categories.Category.Core using (Category)
 open import Categories.Category.Product
 import Categories.Category.Construction.Cowedges as Cowedges
 open import Categories.Category.Construction.Functors
-open import Categories.Category.Equivalence
+open import Categories.Category.Equivalence as SE
 open import Categories.Category.Equivalence.Preserves
 open import Categories.Diagram.Coend
 open import Categories.Diagram.Colimit
@@ -137,6 +137,12 @@ module _ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′
 
   open StrongEquivalence Eq renaming (F to F⇒)
 
+  Coend-yields-colimit : Coend F → Colimit (Twist′ C D F)
+  Coend-yields-colimit ef = record { initial = pres-Initial (SE.sym Eq) (Coend⇒Initial F ef) }
+
+  colimit-yields-Coend : Colimit (Twist′ C D F) → Coend F
+  colimit-yields-Coend l = Initial⇒Coend F (pres-Initial Eq (Colimit.initial l))
+
   -- Coends and Colimits are equivalent, in the category Cowedge F
   Coend-as-Colimit : (coend : Coend F) → (cl : Colimit (Twist′ C D F)) → Coend.cowedge coend ≅ F₀ F⇒ (Colimit.initial.⊥ cl)
   Coend-as-Colimit coend cl = Initial.up-to-iso (Cowedges.Cowedges F) (Coend⇒Initial F coend) (pres-Initial Eq initial)