adding TODO, starting to fix line length

maxsnew · May 25, 2024 · f8e25ae · f8e25ae
1 parent 5bd2365
commit f8e25ae
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/Cubical/Categories/Constructions/Coend/Base.agda b/Cubical/Categories/Constructions/Coend/Base.agda
@@ -15,7 +15,7 @@ module Cubical.Categories.Constructions.Coend.Base where
         variable
             ℓC ℓC' ℓD ℓD' : Level
 
-    module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}(F : Bifunctor (C ^op) C D)where
+    module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}(F : Bifunctor (C ^op) C D) where
 
         module C = Category C
         module D = Category D
@@ -36,6 +36,8 @@ module Cubical.Categories.Constructions.Coend.Base where
                 extranatural : {c c' : C.ob}(f : C [ c , c' ]) →
                     (F ⟪ C.id , f ⟫lr D.⋆  ψ c') ≡ ( F ⟪ f ,  C.id ⟫lr D.⋆ ψ c)
 
+        -- TODO : Can probably define a Presheaf structure for Cowedge
+        -- and then this should be isomorphic to a universal element of that presheaf.
         record Coend : Set ((ℓ-max ℓC (ℓ-max ℓC' (ℓ-max ℓD ℓD'))))  where
             open Cowedge
             field