/Category.lean at bc304c5ab5c70be9ed8a1f3eca3d9ee0805a3ca3

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