/Category.lean at 9893d6a2b324d70f8d4dd487a09da05c1f5f19fc

import Mathlib

/-
Lean, the category!
Objects: Types
Morphisms: (Total) Functions

Resources:
https://raw.githubusercontent.com/BartoszMilewski/DaoFP/refs/heads/master/DaoFP.pdf
https://math.andrej.com/2016/08/06/hask-is-not-a-category/
-/

-- Initial object
#check Empty

-- Morphism from initial object
#check Empty.elim

-- Terminal object
#check PUnit

-- Identity morphism
#check id

-- Composition of morphism is associative
#check Function.comp_assoc

-- Equality of morphisms
#check funext

-- Sums (coproducts)
#check Sum

-- Products
#check Prod

-- Exponentials
#check (· → ·)


/-
Endofunctors
f maps objects
f.map maps morphisms
`(α → β) → f α → f β` is the same thing as `(α → β) → (f α → f β)`
-/
#check Functor
#check LawfulFunctor

#synth Functor List

#synth Functor Option

instance : LawfulFunctor List where
  map_const := by solve_by_elim
  id_map xs := by simp
  comp_map := by simp


/--
Contravariant (endo)functors (normal functors are "covariant" functors)

Also, contravariant functors are covariant functors in the opposite category

`map` turns a "producer of α" into a "producer of β"
`comap` 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)

theorem Cofunctor.id_comap' [Cofunctor f] : Cofunctor.comap (f := f) (@id α) = id := by
  ext x
  exact Cofunctor.id_comap (f := f) x

theorem Cofunctor.comap_comp_comap [Cofunctor f] (g : α → β) (h : β → γ) :
    ((Cofunctor.comap g) ∘ (Cofunctor.comap h) : f γ → f α) = Cofunctor.comap (f := f) (h ∘ g) :=
  funext fun _ => (comp_comap _ _ _).symm


/-- Composition of two functors of same variance is a functor -/
@[simp]
instance [Functor f] [LawfulFunctor f] [Functor g] [LawfulFunctor g] : Functor (f ∘ g) where
  map h x := Functor.map (f := f) (h <$> ·) x

instance [Functor f] [LawfulFunctor f] [Functor g] [LawfulFunctor g] : LawfulFunctor (f ∘ g) where
  map_const := by solve_by_elim
  id_map := by simp
  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 [Cofunctor f] [Cofunctor 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]

#synth LawfulFunctor (List ∘ Option)


/-- 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) (Cofunctor.comap h ·) x
  id_comap := by simp [Cofunctor.id_comap (f := g)]
  comp_comap := by simp [Cofunctor.comp_comap]

@[simp]
instance [Cofunctor f] [Functor g] [LawfulFunctor g] : Cofunctor (f ∘ g) where
  comap h x := Cofunctor.comap (f := f) (h <$> ·) x
  id_comap := by
    simp only [Function.comp_apply, id_map]
    exact Cofunctor.id_comap (f := f)
  comp_comap h h' x := by
    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


/-- Profunctors: Useful for lenses -/
class Profunctor (p : Type u → Type u → Type (u + 1)) where
  dimap : (s → a) → (b → t) → (p a b → p s t)

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) :=
  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⟩

def End p [Profunctor p] := ∀ x, p x x

def Coend p [Profunctor p] := Σ x, p x x

inductive ProPair q p [Profunctor p] [Profunctor q] a b x y
  | mk : q a y → p x b → ProPair q p 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⟩

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⟩⟩


/--
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)

instance : Natural List Option List.head? where
  naturality := by simp

def OptionToList : Option α → List α
  | some a => [a]
  | none => []

instance : Natural Option List OptionToList where
  naturality := by
    simp [OptionToList]
    grind

class Conatural f [Cofunctor f] g [Cofunctor g] (η : {α : Type u} → 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 reverse map -/
def yoneda' [Functor f] [LawfulFunctor f] (y : f α) : {β : Type u} → (α → β) → f β := (· <$> y)

/-- Reverse map always produces a natural transformation -/
instance [Functor f] [LawfulFunctor f] : Natural (α → ·) f (yoneda' y) where
  naturality h x := by simp [yoneda']; rfl

/-- 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
  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
  simp [yoneda, yoneda']


/-- Coyoneda forward map -/
def coyoneda (g : {β : Type u} → (β → α) → f β) [Cofunctor f] : f α := g id

/-- Coyoneda reverse map -/
def coyoneda' [Cofunctor f] (y : f α) : {β : Type u} → (β → α) → f β := (Cofunctor.comap · y)

/-- Same but for Coyoneda -/
theorem coyoneda_lemma (g : {β : Type u} → (β → α) → f β) [Cofunctor f] [N : Conatural (· → α) f g] :
    (coyoneda' (β := ·) (coyoneda (f := f) g)) = (g (β := ·)) := by
  unfold coyoneda coyoneda'
  simp [N.naturality]

theorem coyoneda_lemma' (y : f α) [Cofunctor f] :
    coyoneda (coyoneda' (f := f) (α := α) y) = y := by
  simp [coyoneda, coyoneda', Cofunctor.id_comap]


-- TODO: Applicatives, monads, Kleisi categories