/Category.lean at e41f827da61bd4e86abf8530866d2211098b67d4

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 (· → ·)

-- Lean is a bicartesian closed category, which means it has an initial object, terminal object, sums, products, exponentials, and sums distribute over products.


/-
Endofunctors in Lean!

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)

infixr:100 " <¥> " => Cofunctor.comap

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 : β → γ) :
    ((g <¥> ·) ∘ (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]

-- If functors are sort of like "containers" for data, then functor composition is "nesting" two containers
#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) (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)

Intuitively, it represents moving data from one "container" to another
-/
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 α) : h <¥> (η x) = η (h <¥> x)

/--
Vertical composition of natural transformations

Intuitively this is like doing two data moves.
-/
instance [Functor f] [LawfulFunctor f] [Functor g] [LawfulFunctor g] [Functor h] [LawfulFunctor h] [M : Natural f g η] [N : Natural g h μ] :
    Natural f h (fun {α : Type u} ↦ @μ α ∘ @η α) where
  naturality := by simp [N.naturality, M.naturality]

/--
Horizontal composition of natural transformations

Intuitively this is like repackaging data in nested "containers"
-/
instance (η : NaturalType f f') (μ : NaturalType g g') [Functor f] [LawfulFunctor f] [Functor f'] [LawfulFunctor f'] [Functor g] [LawfulFunctor g] [Functor g'] [LawfulFunctor g'] [M : Natural f f' η] [N : Natural g g' μ] :
    Natural (g ∘ f) (g' ∘ f') (μ ∘ (Functor.map (f := g) η ·)) where
  naturality := by simp [N.naturality, M.naturality]

/-- Alternatively we do `μ` first and then the map second -/
instance (η : NaturalType f f') (μ : NaturalType g g') [Functor f] [LawfulFunctor f] [Functor f'] [LawfulFunctor f'] [Functor g] [LawfulFunctor g] [Functor g'] [LawfulFunctor g'] [M : Natural f f' η] [N : Natural g g' μ] :
    Natural (g ∘ f) (g' ∘ f') ((Functor.map (f := g') η ·) ∘ μ) where
  naturality := by simp [N.naturality, M.naturality]

/-- The two orderings are equivalent, which only requires the outer transformation to be natural -/
lemma horizontal_comp_equiv (η : NaturalType f f') (μ : NaturalType g g') [Functor f] [LawfulFunctor f] [Functor f'] [LawfulFunctor f'] [Functor g] [LawfulFunctor g] [Functor g'] [LawfulFunctor g'] [N : Natural g g' μ] :
    (μ ∘ (Functor.map (f := g) η ·)) x = ((Functor.map (f := g') η ·) ∘ μ) x:= by
  simp [N.naturality]


/-- 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
  simp [yoneda, yoneda', 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 := (· <¥> 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
  simp [coyoneda, coyoneda', N.naturality]

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


-- TODO: Applicatives
#check Applicative
#check LawfulApplicative

/-- Composition of two applicatives is an applicative -/
@[simp]
instance [Applicative f] [LawfulApplicative f] [Applicative g] [LawfulApplicative g] : Applicative (f ∘ g) where
  pure x := pure (f := f) (pure x)
  seq h x := Seq.seq (f := f) ((· <*> ·) <$> h) x

instance [Applicative f] [LawfulApplicative f] [Applicative g] [LawfulApplicative g] : LawfulApplicative (f ∘ g) where
  seqLeft_eq := by simp
  seqRight_eq := by simp
  pure_seq := by simp [pure_seq]
  map_pure := by simp
  seq_pure := by simp
  seq_assoc x h h' := by
    simp [seq_assoc, seq_map_assoc, map_seq]
    congr 3
    ext
    simp [seq_assoc]

-- TODO: Monads
#check Monad
#check LawfulMonad

/-
Sadly, in general monads do not compose 😿
https://carlo-hamalainen.net/2014/01/02/applicatives-compose-monads-do-not/

However, in some cases we can use monad transformers to compose them.
-/

-- TODO: Kleisi categories