/Category.lean at 973a861ebdab0b6a2a2f382e4ee077531ed0853a

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

#synth Functor Tree

#synth Functor (Except String)

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


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


-- Bifunctors map Lean × Lean to Lean
#check Bifunctor
#check LawfulBifunctor

-- `Sum` and `Prod` are bifunctors
#synth LawfulBifunctor Sum
#synth LawfulBifunctor Prod


/-- Profunctors are useful for lenses -/
class Profunctor (p : Type u → Type v → Type*) 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 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]

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

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

abbrev ProPair q p [Profunctor p] [Profunctor q] a b x y :=
  q a y × p x b

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]

abbrev CoendCompose p q [Profunctor p] [Profunctor q] a b :=
  Coend (ProPair q p 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)⟩
  id_dimap := by simp [Profunctor.id_dimap]
  dimap_dimap := by simp [Profunctor.dimap_dimap]


/-- 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] (η : NaturalType 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] (η : 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 : NaturalType (α → ·) f) [Functor f] [LawfulFunctor f] : f α := g id

/-- Yoneda reverse map -/
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
  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 : 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' y) = y := by
  simp [yoneda, yoneda']


/-- Coyoneda forward map -/
def coyoneda (g : NaturalType (· → α) f) [Cofunctor f] : f α := g id

/-- Coyoneda reverse map -/
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 : 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' y) = y := by
  simp [coyoneda, coyoneda', Cofunctor.id_comap]


-- TODO: Applicatives, monads, Kleisi categories