Composition of natural transformations

Changes

1 changed files (+38/-2)

• Category.lean
  • @@ -37,6 +37,8 @@ https://math.andrej.com/2016/08/06/hask-is-not-a-category/
    -- Exponentials #check (· → ·) + -- Lean is a bicartesian closed category, which means it has an initial object, terminal object, sums, products, exponentials, and sums distribute over products. + /- Endofunctors in Lean!
  • @@ -134,6 +136,7 @@ instance [Cofunctor f] [Cofunctor g] : LawfulFunctor (f ∘ g) where
    id_map := by simp [Cofunctor.id_comap'] comp_map h h' x := by simp [← Cofunctor.comap_comp_comap] + -- If functors are sort of like "containers" for data, then functor composition is "nesting" two containers #synth LawfulFunctor (List ∘ Option)
  • @@ -212,7 +215,11 @@ instance [Profunctor p] [Profunctor q] : Profunctor (CoendCompose p q) where
    dimap_dimap := by simp [Profunctor.dimap_dimap] - /-- Type of a natural transformation (without the naturality condition) -/ + /-- + Type of a natural transformation (without the naturality condition) + + Intuitively, it represents moving data from one "container" to another + -/ abbrev NaturalType.{u} (f : Type u → Type v) (g : Type u → Type v) := {α : Type u} → f α → g α
  • @@ -235,6 +242,34 @@ instance : Natural Option List OptionToList where
    class Conatural f [Cofunctor f] g [Cofunctor g] (η : NaturalType f g) where naturality (h : β → α) (x : f α) : h <¥> (η x) = η (h <¥> x) + /-- + Vertical composition of natural transformations + + Intuitively this is like doing two data moves. + -/ + instance [Functor f] [LawfulFunctor f] [Functor g] [LawfulFunctor g] [Functor h] [LawfulFunctor h] [M : Natural f g η] [N : Natural g h μ] : + Natural f h (fun {α : Type u} ↦ @μ α ∘ @η α) where + naturality := by simp [N.naturality, M.naturality] + + /-- + Horizontal composition of natural transformations + + Intuitively this is like repackaging data in nested "containers" + -/ + instance (η : NaturalType f f') (μ : NaturalType g g') [Functor f] [LawfulFunctor f] [Functor f'] [LawfulFunctor f'] [Functor g] [LawfulFunctor g] [Functor g'] [LawfulFunctor g'] [M : Natural f f' η] [N : Natural g g' μ] : + Natural (g ∘ f) (g' ∘ f') (μ ∘ (Functor.map (f := g) η ·)) where + naturality := by simp [N.naturality, M.naturality] + + /-- Alternatively we do `μ` first and then the map second -/ + instance (η : NaturalType f f') (μ : NaturalType g g') [Functor f] [LawfulFunctor f] [Functor f'] [LawfulFunctor f'] [Functor g] [LawfulFunctor g] [Functor g'] [LawfulFunctor g'] [M : Natural f f' η] [N : Natural g g' μ] : + Natural (g ∘ f) (g' ∘ f') ((Functor.map (f := g') η ·) ∘ μ) where + naturality := by simp [N.naturality, M.naturality] + + /-- The two orderings are equivalent, which only requires the outer transformation to be natural -/ + lemma horizontal_comp_equiv (η : NaturalType f f') (μ : NaturalType g g') [Functor f] [LawfulFunctor f] [Functor f'] [LawfulFunctor f'] [Functor g] [LawfulFunctor g] [Functor g'] [LawfulFunctor g'] [N : Natural g g' μ] : + (μ ∘ (Functor.map (f := g) η ·)) x = ((Functor.map (f := g') η ·) ∘ μ) x:= by + simp [N.naturality] + /-- Yoneda forward map (g is not necessarily natural) -/ def yoneda (g : NaturalType (α → ·) f) [Functor f] [LawfulFunctor f] : f α := g id
  • @@ -302,8 +337,9 @@ instance [Applicative f] [LawfulApplicative f] [Applicative g] [LawfulApplicativ
    /- Sadly, in general monads do not compose 😿 - However, in some cases we can use monad transformers to compose them. https://carlo-hamalainen.net/2014/01/02/applicatives-compose-monads-do-not/ + + However, in some cases we can use monad transformers to compose them. -/ -- TODO: Kleisi categories