Rename cofunctor to contrafunctor

Changes

1 changed files (+47/-40)

• Category.lean
  • @@ -23,7 +23,11 @@ TODO: Diagrams?
    -- Composition of morphism is associative #check Function.comp_assoc - -- Equality of morphisms + /- + Equality of morphisms + + If two functions return the same values for every input, then they are equal. This doesn't take into account time complexity though. + -/ #check funext -- Initial object
  • @@ -89,24 +93,26 @@ instance : LawfulFunctor List where
    /-- Contravariant functors (normal functors are "covariant" functors) are functors from Colean to Lean + They are occasionally called "cofunctors", which is a misnomer because functors are self-dual. + `map` turns a "producer of α" into a "producer of β" - `comap` turns a "consumer of α" into a "consumer of β" + `contramap` turns a "consumer of α" into a "consumer of β" -/ - class Cofunctor (f : Type u → Type v) where - comap : (β → α) → f α → f β - id_comap (x : f α) : comap id x = x - comp_comap (g : β → α) (h : γ → β) (x : f α) : comap (g ∘ h) x = comap h (comap g x) + class Contrafunctor (f : Type u → Type v) where + contramap : (β → α) → f α → f β + id_contramap (x : f α) : contramap id x = x + comp_contramap (g : β → α) (h : γ → β) (x : f α) : contramap (g ∘ h) x = contramap h (contramap g x) /-- This is not standard notation but I just made something up -/ - infixr:100 " <¥> " => Cofunctor.comap + infixr:100 " <¥> " => Contrafunctor.contramap - theorem Cofunctor.id_comap' [Cofunctor f] : Cofunctor.comap (f := f) (@id α) = id := by + theorem Contrafunctor.id_contramap' [Contrafunctor f] : Contrafunctor.contramap (f := f) (@id α) = id := by ext x - exact Cofunctor.id_comap x + exact Contrafunctor.id_contramap x - theorem Cofunctor.comap_comp_comap [Cofunctor f] (g : α → β) (h : β → γ) : - ((g <¥> ·) ∘ (h <¥> ·) : f γ → f α) = Cofunctor.comap (h ∘ g) := - funext fun _ ↦ (comp_comap _ _ _).symm + theorem Contrafunctor.contramap_comp_contramap [Contrafunctor f] (g : α → β) (h : β → γ) : + ((g <¥> ·) ∘ (h <¥> ·) : f γ → f α) = Contrafunctor.contramap (h ∘ g) := + funext fun _ ↦ (comp_contramap _ _ _).symm /-- Hom-functor in enriched category -/
  • @@ -120,12 +126,12 @@ instance (α : Type u) : LawfulFunctor (α → ·) where
    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] + instance (α : Type u) : Contrafunctor (· → α) where + contramap f g := g ∘ f + id_contramap := by simp + comp_contramap := by simp [Function.comp_assoc] - -- Most examples of cofunctors in Lean are these function object things + -- Most examples of contrafunctors in Lean are these function object things /- A function type is covariant if the free param is in an even depth and contravariant otherwise.
  • @@ -149,13 +155,13 @@ instance [Functor f] [LawfulFunctor f] [Functor g] [LawfulFunctor g] : LawfulFun
    comp_map h h' x := by simp; rfl @[simp] - instance [Cofunctor f] [Cofunctor g] : Functor (f ∘ g) where - map h x := Cofunctor.comap (f := f) (Cofunctor.comap h) x + instance [Contrafunctor f] [Contrafunctor g] : Functor (f ∘ g) where + map h x := Contrafunctor.contramap (f := f) (Contrafunctor.contramap h) x - instance [Cofunctor f] [Cofunctor g] : LawfulFunctor (f ∘ g) where + instance [Contrafunctor f] [Contrafunctor g] : LawfulFunctor (f ∘ g) where map_const := by solve_by_elim - id_map := by simp [Cofunctor.id_comap'] - comp_map h h' x := by simp [← Cofunctor.comap_comp_comap] + id_map := by simp [Contrafunctor.id_contramap'] + comp_map h h' x := by simp [← Contrafunctor.contramap_comp_contramap] -- If functors are sort of like "containers" for data, then functor composition is "nesting" two containers #synth LawfulFunctor (List ∘ Option)
  • @@ -163,19 +169,19 @@ instance [Cofunctor f] [Cofunctor g] : LawfulFunctor (f ∘ g) where
    /-- Composition of functors of opposite variance is a contravariant functor -/ @[simp] - instance [Functor f] [LawfulFunctor f] [Cofunctor g] : Cofunctor (f ∘ g) where - comap h x := Functor.map (f := f) (h <¥> ·) x - id_comap := by simp [Cofunctor.id_comap] - comp_comap := by simp [Cofunctor.comp_comap] + instance [Functor f] [LawfulFunctor f] [Contrafunctor g] : Contrafunctor (f ∘ g) where + contramap h x := Functor.map (f := f) (h <¥> ·) x + id_contramap := by simp [Contrafunctor.id_contramap] + comp_contramap := by simp [Contrafunctor.comp_contramap] @[simp] - instance [Cofunctor f] [Functor g] [LawfulFunctor g] : Cofunctor (f ∘ g) where - comap h x := Cofunctor.comap (f := f) (h <$> ·) x - id_comap := by + instance [Contrafunctor f] [Functor g] [LawfulFunctor g] : Contrafunctor (f ∘ g) where + contramap h x := Contrafunctor.contramap (f := f) (h <$> ·) x + id_contramap := by simp only [Function.comp_apply, id_map] - exact Cofunctor.id_comap - comp_comap h h' x := by - simp only [← Functor.map_comp_map h' h, Cofunctor.comp_comap] + exact Contrafunctor.id_contramap + comp_contramap h h' x := by + simp only [← Functor.map_comp_map h' h, Contrafunctor.comp_contramap] -- Bifunctors map Lean × Lean to Lean
  • @@ -275,7 +281,7 @@ def OptionToList : Option α → List α
    instance : Natural Option List OptionToList := ⟨by simp [OptionToList]; grind⟩ - class Conatural f [Cofunctor f] g [Cofunctor g] (η : NaturalType f g) where + class Conatural f [Contrafunctor f] g [Contrafunctor g] (η : NaturalType f g) where naturality (h : β → α) (x : f α) : h <¥> (η x) = η (h <¥> x) /--
  • @@ -332,24 +338,24 @@ theorem yoneda_lemma' (y : f α) [Functor f] [LawfulFunctor f] : yoneda (yoneda'
    simp [yoneda, yoneda'] /-- Coyoneda forward map -/ - def coyoneda (g : NaturalType (· → α) f) [Cofunctor f] : f α := + def coyoneda (g : NaturalType (· → α) f) [Contrafunctor f] : f α := g id /-- Coyoneda reverse map -/ - def coyoneda' [Cofunctor f] (y : f α) : NaturalType (· → α) f := + def coyoneda' [Contrafunctor f] (y : f α) : NaturalType (· → α) f := (· <¥> y) /-- Reverse map always produces a natural transformation -/ - instance [Cofunctor f] : Conatural (· → α) f (coyoneda' y) := - ⟨fun h x ↦ by simp [coyoneda', Cofunctor.comp_comap]⟩ + instance [Contrafunctor f] : Conatural (· → α) f (coyoneda' y) := + ⟨fun h x ↦ by simp [coyoneda', Contrafunctor.comp_contramap]⟩ /-- Same but for Coyoneda -/ - theorem coyoneda_lemma (g : NaturalType (· → α) f) [Cofunctor f] [N : Conatural (· → α) f g] : coyoneda' (coyoneda g) x = g x := by + theorem coyoneda_lemma (g : NaturalType (· → α) f) [Contrafunctor f] [N : Conatural (· → α) f g] : coyoneda' (coyoneda g) x = g x := by simp [coyoneda, coyoneda', N.naturality] /-- Same but for Coyoneda -/ - theorem coyoneda_lemma' (y : f α) [Cofunctor f] : coyoneda (coyoneda' y) = y := by - simp [coyoneda, coyoneda', Cofunctor.id_comap] + theorem coyoneda_lemma' (y : f α) [Contrafunctor f] : coyoneda (coyoneda' y) = y := by + simp [coyoneda, coyoneda', Contrafunctor.id_contramap] -- Applicative functors
  • @@ -547,6 +553,7 @@ instance [EndofunctorMonoid m] : Monad m where
    pure := EndofunctorMonoid.pure bind := bindFromJoin EndofunctorMonoid.join + -- TODO: This only works for `m` from `Type u → Type u`, but monads can be `Type u → Type v` in Lean /-- A monoid in the category of endofunctors is a monad -/ instance [EndofunctorMonoid m] [J : Natural (m ∘ m) m EndofunctorMonoid.join] [P : Natural Id m EndofunctorMonoid.pure] : LawfulMonad m := LawfulMonad.mk' m id_map