Category Theory


Categories and Precategories


1. A : π’ž. -- object 2. A, B : π’ž | A β†’ B : π’ž is-0-type(A β†’ B). -- morphism 3. A : π’ž | 1_A : A β†’ A. -- identity morphism 4. A, B, C : π’ž | g : (B β†’ C) β†’ f : (A β†’ B) β†’ g f : (A β†’ C). -- composition 5. A, B : π’ž | (f : A β†’ B) β†’ f = 1_B f = f 1_A. 6. A, B, C, D : A | f : A β†’ B, g : B β†’ C, h : C β†’ D β†’ h (g f) = (h g) f. -- associative


Wikipedia nLabf : A β†’ B | f : A β‰… B | (g : B β†’ A) Γ— (g f = 1_A) Γ— (f g = 1_B).

Homotopy Equivalence

f : A β†’ B, g : B β†’ A β†’ ⋆ : g f = 1_A, ⋆ : f g = 1_B β†’ ⋆ : a β‰… b. 1_A : a β‰… a, 1_A^[βˆ’1] = 1_A.


(f : A β†’ B) β†’ is-0-type(A β‰… B).

Identity to Isomorphism

precategory A | (a, b : A) β†’ (a = b) β†’ (a β‰… b).


precategory Set | A β†’ B ≑ A β†’ B.


Wikipedia nLabcategory A | precategory A | (a, b : A) β†’ (a = b) ≃ (a β‰… b).


precategory Set | category Set.


category A | is-1-type(A).(a, b : A) β†’ is-0-type(a β‰… b) β†’ (a = b) ≃ (a β‰… b) β†’ is-0-type(a = b).

Isomorphism to Identity

isotoid : (a β‰… b) β†’ (a = b).


p : a = a', q : b = b', f : A β†’ B β†’(p, q)_*(f) = idtoiso(q) β—¦ f β—¦ idtoiso(p)^[βˆ’1].

Example (Preorder)

precategory A | (a, b : A) β†’ is-(βˆ’1)-type(a β†’ b) | a ≀ a, -- reflexivity a ≀ b β†’ b ≀ c β†’ a ≀ c. -- transitivity(f : a ≀ b) β†’ (g : b ≀ a) β†’ (a β‰… b) β†’ is-(βˆ’1)-type(a β‰… b).(A, ≀) : Preord β†’ (a, b : A) β†’ is-(βˆ’1)-type(a = b) β†’ (a β‰… b β†’ a = b)β†’ (A, _) : πΆπ‘Žπ‘‘.


(A, _) : πΆπ‘Žπ‘‘ β†’ _ : is-0-type(A) ≃ (a, b : A β†’ is-(βˆ’1)-type(a ≃ b)).(A, _) : πΆπ‘Žπ‘‘ β†’ a, b : A β†’ _ : (a β‰… b) ≃ (a = b).


A : U β†’ ⋆ : is-1-type(A) β†’ (A, a = b) : Groupoid. A : U β†’ ⋆ : is-0-type(A) β†’ (A, a = b) : DiscCat.

Fundamental Pregroupoid

A : U β†’ (A, ||a = b||_0) : Precat β†’ a, b, c : A β†’(b = c) β†’ (a = b) β†’ (a = c) β†’ ||b = c||_0 β†’ ||a = b||_0 β†’ ||a = c||_0 β†’(A, ||a = b||_0) : FundPregroupoid.

Homotopy Precategory of Types

(U, ||A β†’ B||_0) : Precat, (U, ||A β†’ B||_0) : HPrecat.


(0-type_U, A β†’ B β†’ (βˆ’1)-type_U) : Precat β†’ A : 0-type_U β†’ 1_A(a, a') ≑ (a = a') β†’ R : A β†’_[𝑅𝑒𝑙] B β†’ S : B β†’_[𝑅𝑒𝑙] C β†’ (S β—¦ R)(a, c) ≑ ||b : B, R(a, b) Γ— S(b, c)|| β†’(0-type_U, A β†’ B β†’ (βˆ’1)-type_U) : 𝑅𝑒𝑙. R : A β‰… B β†’ 1.1. R(a, b), R^[βˆ’1](b', a) β†’ (R β—¦ R^[βˆ’1])(b', b) β†’ b' = b. 1.2. R(a, b), R^[βˆ’1](b, a') β†’ (R^[βˆ’1] β—¦ R)(a, a') β†’ a = a'. 2. a : A β†’ a = a β†’ (R^[βˆ’1] β—¦ R)(a, a) β†’ b : B, R(a, b), R^[βˆ’1](b', a). 3. 4. _ : 𝑅𝑒𝑙 β†’ πΆπ‘Žπ‘‘.

Functors and Transformations


Wikipedia nLab(A, _), (B, _) : Precat β†’ 1. F : A β†’ B. 2. a, b : A β†’ F_[a, b] : (A β†’ B) β†’ (F(a) β†’_B F(b)). 3. a : A β†’ F_[a, a](1_A) = 1_[F(a)]. 4. a, b, c : A β†’ f : A β†’ B, g : b β†’_A c β†’ F_[a, c](g β—¦ f) = F_[b, c](g) F_[a, b](f).

Natural Transformation

Wikipedia(A, _), (B, _) : Precat β†’ (F, F_[a, b]), (G, G_[a, b]) : Functor β†’ 1. a : A β†’ Ξ³_a : F(a) β†’_B G(a). -- components 2. a, b : A β†’ f : A β†’ B β†’ G_[a, b](f) β—¦ Ξ³_a = Ξ³_b β—¦ F_[a, b](f). -- naturality axiomNatural Transformation

Functor Precategory

(A, _), (B, _) : Precat β†’ (B^A, F β†’_[B^A] G) : Precat β†’ B^A : A β†’ B, F β†’_[B^A] G is the type of natural transformation F β†’ G.


A natural transformation Ξ³ : F β†’ G is an isomorphism in B^A if and only if each Ξ³_a is an isomorphism in B.


A : Precategory, B : Category β†’ B^A : Category.

Composite of functors


Functors F : A β†’ B, G : B β†’ C β†’ G_0 F_0 : A_0 β†’ C_0, a, b : A β†’ (G_[F(a), F(b)] F_[a, b]) : (A β†’ B) β†’ ((G F)(a) β†’_C (G F)(b)).

Composite of natural transformations and functors


F : A β†’ B, G, H : B β†’ C, Ξ³ : G β†’ H, Ξ³ F : G F β†’ H F, a : A, Ξ³_[F(a)], b : B, K(Ξ³_b).


F, G : A β†’ B, H, K : B β†’ C, Ξ³ : F β†’ G, Ξ΄ : H β†’ K,(Ξ΄ G) (H Ξ³) = (K Ξ³) (Ξ΄ F).


H (G F) = (H G) F.

Adjoint Functors/Adjunction

Wikipedia nLab

Functor F : A β†’ B β†’ is-left-adjoint(F) ≑

  • G : B β†’ A,
  • Ξ· : 1_A β†’ G F (unit),
  • Ξ΅ : F G β†’ 1_B (counit),
  • (e F) (F Ξ·) = 1_F, (G Ξ΅) (Ξ· G) = 1_G (triangle identities).



is-left-adjoint(F), A ≃ B.


F : A β†’ B β†’(A ≃ B) = (G : B β†’ A) Γ— (G F ≃ 1_A) Γ— (F G ≃ 1_B).


F : A β†’ B β†’ F_[a, b]



F : A β†’ B β†’ F_[a, b]


Split Essentially Surjective

F : A β†’ B β†’(b : B) β†’ (a : A) Γ— F(a) ≃ b.


A, B : Precategory, F : A β†’ B β†’(A ≃ B) ≃ (b : B) β†’ (a : A) Γ— F(a) ≃ b.

Essentially Surjective

F : A β†’ B β†’(b : B) β†’ mere (a : A) Γ— F(a) ≃ b.

Weak Equivalence

F is bijective and essentially surjective.


F is bijective, A : Category β†’(b : B) β†’ is-truncated_[βˆ’1]((a : A) Γ— F(a) ≃ b). F is an equivalence = F is a week equivalence.


F is bijective and F_0 is an equivalence of types. A β‰… B.


A, B : Precategory, F : A β†’ B β†’(A β‰… B)≃ ≃.


A, B : Precategory β†’(A = B) β†’ (A β‰… B).


A, B : Category β†’(A = B) β†’ (A ≃ B).


Wikipedia nLabA : Precategory β†’ A^* : Precategory, A^*_0 ≑ A_0, a β†’_[A^*] b ≑ A β†’ B.


A, B : Precategory β†’ A Γ— B : Precategory,(A Γ— B)_0 ≑ A_0 Γ— B_0,(a_0, b_0) β†’_[A Γ— B] (a_1, b_1) ≑ (a_0 β†’_A a_1) Γ— (b_0 β†’_B b_1), 1_[(a, b)] ≑ (1_A, 1_B),(g, g') (f, f') ≑ (g f, g' f').


A, B, C : Precategory β†’(A Γ— B β†’ C) ≃ (A β†’ C^B).A : Precategory β†’ hom_a : A^* Γ— A β†’ 𝑆𝑒𝑑.(a, b) : A^*_0 Γ— A_0 ≑ A_0 Γ— A_0,(f, f') : (a, b) β†’_[A^* Γ— A] (a', b'),(hom_a)_[(a, b), (a', b')](f, f') ≑ (g ↦ (f' g' f)) : (A β†’ B) β†’ (a' β†’_A b').

Yoneda Embedding

y : A β†’ 𝑆𝑒𝑑^[A^*],

Yoneda Lemma

Wikipedia nLabA : Precategory, a : A, F : 𝑆𝑒𝑑^[A^*] β†’(y a β†’_[𝑆𝑒𝑑^[A^*]] F) β‰… F(a).


y : A β†’ 𝑆𝑒𝑑^[A^*] is bijective.


A : Category β†’ y_0 : A_0 β†’ (𝑆𝑒𝑑^[A^*])_0 is an embedding.(y a = y b) β†’ (a = b).


F : 𝑆𝑒𝑑^[A^*] β†’(a : A) Γ— y a β‰… F.


A, B : Precategory, F : A β†’ B β†’ is-left-adjoint(F) ≃ (b : B) β†’ is-representable(a ↦ F(a) β†’_b b).

Strict Category

nLabA : Precategory, A_0 ≑ 0-type.


Wikipedia nLab(m f = m g) β†’ (f = g).


Structure Identity Principle

Notion of Structure

(P, H), P : X_0 β†’ U, x : X_0, P(x) ((P, H)-structures). x, y : X_0, f : x β†’_X y, Ξ± : P(x), Ξ² : P(y), H_[Ξ± Ξ²](f) ((P, H)-homomorphism). x : X_0, Ξ± : P(x), H_[Ξ± Ξ±](1_x). x, y, z : X_0, Ξ± : P(x), Ξ² : P(y), Ξ³ : P(z), f : x β†’_X y, g : y β†’_X z, H_[Ξ± Ξ²](f) β†’ H_[Ξ² Ξ³](g) β†’ H_[Ξ± Ξ³](g f).(Ξ± ≀_x Ξ²) ≑ H_[Ξ± Ξ²](1_x). A ≑ Str_[(P, H)](X) (precategory of (P, H)-structures), A_0 ≑ (x : X_0) Γ— P(x),(x, Ξ±) : A_0, |(x, Ξ±)| ≑ x.(x, Ξ±), (y, Ξ²) : A_0 β†’(x, Ξ±) β†’_A (y, Ξ²) ≑ {f : x β†’ y | H_[Ξ± Ξ²](f)}.

Theorem: Structure identity principle

X, (P, H), Str_[(P, H)](X).


P(x) ≑ P_0(x) Γ— P_1(x), P_0(x) ≑ (Ο‰ : Ξ©_0) β†’ x_[|Ο‰|] β†’ x, P_1(x) ≑ (Ο‰ : Ξ©_1) β†’ x_[|Ο‰|] β†’ (βˆ’1)-type_U.

Rezk Completion


(g : F(b) β†’_C G(b)) Γ— (a : A) β†’ (f : H(a) ≃ b) β†’ (Ξ³_a) = G(f^[βˆ’1]) g F(f).


(- H) : C_b β†’ C_a.


A β†’ A_^.

Diagonal Functor

WikipediaC β†’ C Γ— C. a Γ— b : Ξ” β†’ <a, b>.

Functor Category

WikipediaF, G : C β†’ D β†’ Ξ· : F β†’ G, Component of Ξ· at X Ξ·_X : F(X) β†’ G(X), f : X β†’ Y, Ξ·_Y β—‹ F(f) = G(f) β—‹ Ξ·_X.


Wikipedia nLabProductSum

Commutative Diagram

Wikipedia nLab


Wikipedia nLabf : A β†’ B, g : B β†’ C, h : C β†’ D g f : A β†’ C, h g : B β†’ D, (h g) f : A β†’ D, h (g f) : A β†’ D, f^[βˆ’1] f = id_a, f f^[βˆ’1] = id_b

Internal Category


Small category


Initial Object

Terminal Object

Category of Sets

Wikipedia nLab

Category of Groups

Wikipedia nLab

Category of Rings

Category of Modules

Wikipedia nLab

Category of Manifolds



Wikipedia nLab



Indexed category

Wikipedia nLab




Wikipedia nLab