Comment about natural transformations

Changes

1 changed files (+5/-1)

• Category.lean
  • @@ -174,7 +174,11 @@ instance [Profunctor p] [Profunctor q] : Profunctor (CoendCompose p q) where
    | ⟨x, ⟨qay, pxb⟩⟩ => ⟨x, ⟨Profunctor.dimap l id qay,Profunctor.dimap id r pxb⟩⟩ - /- Natural transformations -/ + /-- + Natural transformations + + Naturality is automatically guarenteed for parametrically polymorphic functions (where the implementation is the same for each type), AKA "theorems for free". This is not guarenteed in general though since we could have a function which inspects the input type and does something crazy. + -/ class Natural f [Functor f] [LawfulFunctor f] g [Functor g] [LawfulFunctor g] (η : {α : Type u} → f α → g α) where naturality (h : α → β) (x : f α) : h <$> (η x) = η (h <$> x)