Simplify a lot of the Yoneda stuff, add more examples

Changes

1 changed files (+78/-43)

• Category.lean
  • @@ -51,6 +51,10 @@ f.map maps morphisms
    #synth Functor Option + #synth Functor Tree + + #synth Functor (Except String) + instance : LawfulFunctor List where map_const := by solve_by_elim id_map xs := by simp
  • @@ -79,6 +83,34 @@ theorem Cofunctor.comap_comp_comap [Cofunctor f] (g : α → β) (h : β → γ)
    funext fun _ => (comp_comap _ _ _).symm + /-- Hom-functor in enriched category -/ + @[simp] + instance (α : Type u) : Functor (α → ·) where + map f g := f ∘ g + + instance (α : Type u) : LawfulFunctor (α → ·) where + map_const := by solve_by_elim + id_map := by simp + comp_map := by simp [Function.comp_assoc] + + @[simp] + instance (α : Type u) : Cofunctor (· → α) where + comap f g := g ∘ f + id_comap := by simp + comp_comap := by simp [Function.comp_assoc] + + -- Most examples of cofunctors in Lean are these function object things + + /- + A function type is covariant if the free param is in an even depth and contravariant otherwise. + + α → · is co + · → α is contra + (· → α) → β is co + ((· → α) → β) → γ is contra + and so on + -/ + /-- Composition of two functors of same variance is a functor -/ @[simp] instance [Functor f] [LawfulFunctor f] [Functor g] [LawfulFunctor g] : Functor (f ∘ g) where
  • @@ -118,42 +150,41 @@ instance [Cofunctor f] [Functor g] [LawfulFunctor g] : Cofunctor (f ∘ g) where
    simp only [← Functor.map_comp_map h' h, Cofunctor.comp_comap (f := f)] - /-- Hom-functor in enriched category -/ - @[simp] - instance (α : Type u) : Functor (α → ·) where - map f g := f ∘ g - - instance (α : Type u) : LawfulFunctor (α → ·) where - map_const := by solve_by_elim - id_map := by simp - comp_map := by simp [Function.comp_assoc] - - @[simp] - instance (α : Type u) : Cofunctor (· → α) where - comap f g := g ∘ f - id_comap := by simp - comp_comap := by simp [Function.comp_assoc] - - -- Bifunctors map Lean × Lean to Lean #check Bifunctor #check LawfulBifunctor + -- `Sum` and `Prod` are bifunctors + #synth LawfulBifunctor Sum + #synth LawfulBifunctor Prod - /-- Profunctors: Useful for lenses -/ - class Profunctor (p : Type u → Type u → Type (u + 1)) where + + /-- Profunctors are useful for lenses -/ + class Profunctor (p : Type u → Type v → Type (max u v)) where dimap : (s → a) → (b → t) → (p a b → p s t) + id_dimap : ∀ {α β} (x : p α β), dimap id id x = x + dimap_dimap : + ∀ {α₀ α₁ α₂ β₀ β₁ β₂} (f : α₁ → α₀) (f' : α₂ → α₁) (g : β₀ → β₁) (g' : β₁ → β₂) (x : p α₀ β₀), + dimap f' g' (dimap f g x) = dimap (f ∘ f') (g' ∘ g) x + + -- Exponentials are profunctors + instance : Profunctor (· → ·) where + dimap f g h := g ∘ h ∘ f + id_dimap := by simp + dimap_dimap := by simp [Function.comp_assoc] inductive Procompose p q [Profunctor p] [Profunctor q] a b | mk : q a x → p x b → Procompose p q a b - def mapOut [Profunctor p] [Profunctor q] (pc : Procompose p q a b) (f : {x : Type} → q a x → p x b → c) := + def mapOut [Profunctor p] [Profunctor q] (pc : Procompose p q a b) (f : {x : Type u} → q a x → p x b → c) := match pc with | ⟨qax, pxb⟩ => f qax pxb instance [Profunctor p] [Profunctor q] : Profunctor (Procompose p q) where dimap l r | ⟨qax, pxb⟩ => ⟨Profunctor.dimap l id qax, Profunctor.dimap id r pxb⟩ + id_dimap := by simp [Profunctor.id_dimap] + dimap_dimap := by simp [Profunctor.dimap_dimap] def End p [Profunctor p] := ∀ x, p x x
  • @@ -165,21 +196,28 @@ inductive ProPair q p [Profunctor p] [Profunctor q] a b x y
    instance [Profunctor p] [Profunctor q] : Profunctor (ProPair q p a b) where dimap l r | ⟨qax, pxb⟩ => ⟨Profunctor.dimap id r qax, Profunctor.dimap l id pxb⟩ + id_dimap := by simp [Profunctor.id_dimap] + dimap_dimap := by simp [Profunctor.dimap_dimap] inductive CoendCompose p q [Profunctor p] [Profunctor q] a b | mk : Coend (ProPair q p a b) → CoendCompose p q a b instance [Profunctor p] [Profunctor q] : Profunctor (CoendCompose p q) where dimap l r - | ⟨x, ⟨qay, pxb⟩⟩ => ⟨x, ⟨Profunctor.dimap l id qay,Profunctor.dimap id r pxb⟩⟩ + | ⟨x, ⟨qay, pxb⟩⟩ => ⟨x, ⟨Profunctor.dimap l id qay, Profunctor.dimap id r pxb⟩⟩ + id_dimap := by + simp [Profunctor.id_dimap] + grind + dimap_dimap f f' g g' x := by + simp [Profunctor.id_dimap] - /-- - Natural transformations + /-- Type of a natural transformation (without the naturality condition) -/ + abbrev NaturalType.{u} (f : Type u → Type v) (g : Type u → Type v) := + {α : Type u} → f α → g α - 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 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] (η : NaturalType f g) where naturality (h : α → β) (x : f α) : h <$> (η x) = η (h <$> x) instance : Natural List Option List.head? where
  • @@ -194,18 +232,15 @@ instance : Natural Option List OptionToList where
    simp [OptionToList] grind - class Conatural f [Cofunctor f] g [Cofunctor g] (η : {α : Type u} → f α → g α) where + class Conatural f [Cofunctor f] g [Cofunctor g] (η : NaturalType f g) where naturality (h : β → α) (x : f α) : Cofunctor.comap h (η x) = η (Cofunctor.comap h x) - /-- - Yoneda forward map - g is not necessarily natural - -/ - def yoneda (g : {β : Type u} → (α → β) → f β) [Functor f] [LawfulFunctor f] : f α := g id + /-- Yoneda forward map (g is not necessarily natural) -/ + def yoneda (g : NaturalType (α → ·) f) [Functor f] [LawfulFunctor f] : f α := g id /-- Yoneda reverse map -/ - def yoneda' [Functor f] [LawfulFunctor f] (y : f α) : {β : Type u} → (α → β) → f β := (· <$> y) + def yoneda' [Functor f] [LawfulFunctor f] (y : f α) : NaturalType (α → ·) f := (· <$> y) /-- Reverse map always produces a natural transformation -/ instance [Functor f] [LawfulFunctor f] : Natural (α → ·) f (yoneda' y) where
  • @@ -213,31 +248,31 @@ instance [Functor f] [LawfulFunctor f] : Natural (α → ·) f (yoneda' y) where
    /-- Mapping and unmapping a natural transformation returns the itself Note that this does work for an arbitrary function between the hom-functor and `m` because we use the naturality condition. -/ - theorem yoneda_lemma (g : {β : Type u} → (α → β) → f β) [Functor f] [LawfulFunctor f] [N : Natural (α → ·) f g] : - (yoneda' (β := ·) (yoneda (f := f) g)) = (g (β := ·)) := by + theorem yoneda_lemma (g : NaturalType (α → ·) f) [Functor f] [LawfulFunctor f] [N : Natural (α → ·) f g] : yoneda' (yoneda g) x = g x := by unfold yoneda yoneda' simp [N.naturality] /-- Mapping and unmapping an element `m α` returns itself -/ - theorem yoneda_lemma' (y : f α) [Functor f] [LawfulFunctor f] : - yoneda (yoneda' (f := f) (α := α) y) = y := by + theorem yoneda_lemma' (y : f α) [Functor f] [LawfulFunctor f] : yoneda (yoneda' y) = y := by simp [yoneda, yoneda'] /-- Coyoneda forward map -/ - def coyoneda (g : {β : Type u} → (β → α) → f β) [Cofunctor f] : f α := g id + def coyoneda (g : NaturalType (· → α) f) [Cofunctor f] : f α := g id /-- Coyoneda reverse map -/ - def coyoneda' [Cofunctor f] (y : f α) : {β : Type u} → (β → α) → f β := (Cofunctor.comap · y) + def coyoneda' [Cofunctor f] (y : f α) : NaturalType (· → α) f := (Cofunctor.comap · y) + + /-- Reverse map always produces a natural transformation -/ + instance [Cofunctor f] : Conatural (· → α) f (coyoneda' y) where + naturality h x := by simp [coyoneda', Cofunctor.comp_comap] /-- Same but for Coyoneda -/ - theorem coyoneda_lemma (g : {β : Type u} → (β → α) → f β) [Cofunctor f] [N : Conatural (· → α) f g] : - (coyoneda' (β := ·) (coyoneda (f := f) g)) = (g (β := ·)) := by + theorem coyoneda_lemma (g : NaturalType (· → α) f) [Cofunctor f] [N : Conatural (· → α) f g] : coyoneda' (coyoneda g) x = g x := by unfold coyoneda coyoneda' simp [N.naturality] - theorem coyoneda_lemma' (y : f α) [Cofunctor f] : - coyoneda (coyoneda' (f := f) (α := α) y) = y := by + theorem coyoneda_lemma' (y : f α) [Cofunctor f] : coyoneda (coyoneda' y) = y := by simp [coyoneda, coyoneda', Cofunctor.id_comap]