Link to optics page

Changes

1 changed files (+5/-1)

• Category.lean
  • @@ -172,7 +172,11 @@ instance [Cofunctor f] [Functor g] [LawfulFunctor g] : Cofunctor (f ∘ g) where
    #check LawfulMvFunctor - /-- Profunctors are useful for lenses -/ + /-- + Profunctors are useful for lenses and optics + + For more info about optics see https://marcosh.github.io/post/2025/10/07/the-mondrian-introduction-to-functional-optics.html + -/ class Profunctor (p : Type u → Type v → Type*) where dimap : (s → a) → (b → t) → (p a b → p s t) id_dimap (x : p α β) : dimap id id x = x