Category Theory Notes

(extremely tentative and disorganized)

Basic Stuff

Resources: Richard Southwell (YouTube), Category Theory for Computer Scientists (Pierce), nLab, Wikipedia

• Categories
• Morphisms
• Hom sets
• Set category
• Terminal and initial objects
• Universal constructions
• Product
• Coproduct
• Dual

Basic Stuff

• Epimorphisms
• Homomorphisms
• Isomorphisms
• Exponential objects
• N^N x N -> N
• Product and coproduct in set theory

​

Posets, Preorders

• Poset category (set + <=): refl, trans, anti-sym
• Subset category (Sub(S) + subset relation)
• Preorder category (set + <)
• Product and coproduct in posets
• Product and coproduct in logic
• Exponential objects in posets and logic
• Bicartesian closed categories: terminal objects, products, co-products, exponential objects https://ncatlab.org/nlab/show/bicartesian+closed+category
• Heyting algebra

(Intuitionistic propositional logic?)

• Read: Poset inference rules with <= as \impl
• *Does the law of excluded middle hold?
• Show x /\ y -> y /\ x via category diagram
• Show: x /\ 1 = x
• Show: a /\ b <= a’ /\ b’ if a <= a’ and b <= b’
• Show: z /\ x <= y if z <= y^x
• Show: 1 <= y^x if 1 /\ x <= y

​

Internal logic

• Subobject classifiers
• read as “inclusion function”

​

​

​

• Internal logic of the category of Set
• Internal logic of the category on Subset(S) given set S
• Internal logic of the category of cartesian closed categories
• Minimal logic
• Simply typed lambda calculus
• Internal logic of toposes: Martin-Lof type theory
• Internal logic of the symmetric monoidal closed categories: linear logic

​

​

Internal logic

​

​

Typed lambda calculus with sums

• judgement: term : type, entailment relation (sequents)
• includes types A x B, A + B, A -> B, 1, 0
• internal language of bicartesian closed category
• types as objects, judgements as morphisms
• subobject classifier: X_a(X) = 1 if a : A, else 1
• weak, id, unit-i, x-i1, x-e1, x-e2 b

​

Intermediate Stuff

• Functors
• Natural transformations
• Pullbacks
• Pushouts
• Pullbacks in Set
• Equalizers
• Limits
• Adjoints
• Presheaves
• Sheaves
• Toposes

Category Theory for Linear Logicians

• Cartesian closed categories
• CCC’s relation to intuitionistic logic
• Symmetric monoidal closed categories
• Linearly distributive categories
• *-autonomous categories
• Multiplicative linear logic
• Nonsymmetric monoidal categories & geometry of interaction
• Monad theory for exponentials
• Full completeness

Deductive systems as categories

• Deductive systems as a graph:
• Objects are formulas, arrows are sequents
• Axioms are arrows A -> A (id_A)
• Composition rule is cut rule: f : A -> B, g : B -> C, g o f : A -> C.
• A category F(G) (deductive system formed from graph G):
• objects are formulas, arrows are equivalence classes of proofs

​

​

Operations on categories

• Dualization
• Products (categories C and D give rise to category C x D) with an obvious structure (which?)
• Subcategorization
• Functors
• For categories C and D, a functor F: C -> D is (F_ob, F_arr), where F_ob : Ob(C) -> Ob(D), and for arrows - if f : A -> B then F_arr (f): F_arr A -> F_arr B, with F(gf) = F(g)F(f), and F_arr(id_A) = id_{F_ob A}
• Contravariant functors
• F : C^{op} -> D. This reverses composition.

Category Theory for Linear Logicians

• Cartesian closed categories and relation to intuitionistic logic
• Symmetric monoidal closed categories
• Linearly distributive categories
• *-autonomous categories
• Functors
• Contravariant functors
• Forgetful functors (Poset -> Set, Top -> Set)
• Cartesian categories

Categorical Semantics

• Language
• Theory
• Signature
• Func(S), ar S* -> S
• Rel(S), ar S x S -> S

​

Category Theory in Logic

• Categorical logic
• Simply Typed Lambda Calculus
• Adjunctions
• Categorical proof-theoretic semantics
• Lambek Calculus
• Linear logic

​