More TODOs

Changes

1 changed files (+6/-0)

• Category.lean
  • @@ -10,6 +10,8 @@ https://raw.githubusercontent.com/BartoszMilewski/DaoFP/refs/heads/master/DaoFP.
    https://math.andrej.com/2016/08/06/hask-is-not-a-category/ https://www.mit.edu/~xy/lean/ https://tannerduve.github.io/files/monads.pdf + + TODO: Diagrams? -/ -- Initial object
  • @@ -224,6 +226,10 @@ instance [Profunctor p] [Profunctor q] : Profunctor (CoendCompose p q) where
    id_dimap := by simp [Profunctor.id_dimap] dimap_dimap := by simp [Profunctor.dimap_dimap] + -- TODO: Existential lenses? + + -- TODO: Tambara modules and profunctor optics? + /-- Type of a natural transformation (without the naturality condition)