class Control.Category (Cat : Type u → Type u → Type v) : Type (max (u + 1) v)

A category $\mathcal{C}$ consists of:

• Objects: types $\alpha, \beta, \gamma, \ldots$
• Morphisms: $\text{Cat}\;\alpha\;\beta$ (the "arrows" from $\alpha$ to $\beta$)
• Identity: $\text{id}_\alpha : \text{Cat}\;\alpha\;\alpha$
• Composition: $(f \ggg g) : \text{Cat}\;\alpha\;\gamma$ for $f : \text{Cat}\;\alpha\;\beta$ and $g : \text{Cat}\;\beta\;\gamma$

Composition is in diagrammatic (left-to-right) order: comp f g means "first $f$, then $g$".

• id {α : Type u} : Cat α α

  The identity morphism: $\text{id}_\alpha : \text{Cat}\;\alpha\;\alpha$.

  $$\text{id} \ggg f = f = f \ggg \text{id}$$

• comp {α β γ : Type u} : Cat α β → Cat β γ → Cat α γ

  Composition in diagrammatic order: $(f \ggg g)(x) = g(f(x))$.

  $$\text{comp}\;f\;g : \text{Cat}\;\alpha\;\gamma$$

class Control.LawfulCategory (Cat : Type u → Type u → Type v) [Category Cat] : Prop

Laws for a lawful category:

1. Left identity: $\text{id} \ggg f = f$
2. Right identity: $f \ggg \text{id} = f$
3. Associativity: $(f \ggg g) \ggg h = f \ggg (g \ggg h)$

• id_comp {α β : Type u} (f : Cat α β) : Category.comp Category.id f = f

  Left identity: $\text{id} \ggg f = f$.

• comp_id {α β : Type u} (f : Cat α β) : Category.comp f Category.id = f

  Right identity: $f \ggg \text{id} = f$.

• comp_assoc {α β γ δ : Type u} (f : Cat α β) (g : Cat β γ) (h : Cat γ δ) : Category.comp (Category.comp f g) h = Category.comp f (Category.comp g h)

  Associativity: $(f \ggg g) \ggg h = f \ggg (g \ggg h)$.

structure Control.Fun (α β : Type u) : Type u

A wrapper for functions as a two-parameter type suitable for Category.

$$\text{Fun}\;\alpha\;\beta \;\cong\; (\alpha \to \beta)$$

Needed because Lean's → is not a two-parameter type constructor in the required form Type u → Type u → Type v.

• apply : α → β

  Apply the wrapped function.

@[implicit_reducible]

instance Control.Fun.instCategory : Category Fun

Functions form a category with:

• $\text{id} = \lambda x.\, x$
• $(f \ggg g)(x) = g(f(x))$

Equations

• Control.Fun.instCategory = { id := fun {α : Type ?u.12} => { apply := id }, comp := fun {α β γ : Type ?u.12} (f : Control.Fun α β) (g : Control.Fun β γ) => { apply := g.apply ∘ f.apply } }

instance Control.Fun.instLawfulCategory : LawfulCategory Fun

Functions form a lawful category — all three laws hold definitionally.

def Control.«term_>>>_» : Lean.TrailingParserDescr

Diagrammatic composition operator: $f \ggg g$ means "first $f$, then $g$".

$$f \ggg g = \text{Category.comp}\;f\;g$$

Equations

• Control.«term_>>>_» = Lean.ParserDescr.trailingNode `Control.«term_>>>_» 90 91 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " >>> ") (Lean.ParserDescr.cat `term 90))