# Category Theory ## Categories and Precategories

### Precategory

$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$

### Isomorphism  $f : 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.$

### Lemma

$(f : A → B) → is-0-type(A ≅ B).$

#### Identity to Isomorphism

$precategory A | (a, b : A) → (a = b) → (a ≅ b).$

#### Example

$precategory Set | A → B ≡ A → B.$

### Category  $category A | precategory A | (a, b : A) → (a = b) ≃ (a ≅ b).$

#### Example

$precategory Set | category Set.$

#### Lemma

$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).$

#### Lemma

$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, _) : 𝐶𝑎𝑡.$

#### Example

$(A, _) : 𝐶𝑎𝑡 → _ : is-0-type(A) ≃ (a, b : A → is-(−1)-type(a ≃ b)).(A, _) : 𝐶𝑎𝑡 → a, b : A → _ : (a ≅ b) ≃ (a = b).$

#### Groupoid

$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.$

#### Example

$(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

### Functor  $(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 $(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 axiom$ ### 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.$

#### Lemma

A natural transformation γ : F → G is an isomorphism in B^A if and only if each γ_a is an isomorphism in B.

#### Theorem

$A : Precategory, B : Category → B^A : Category.$

### Composite of functors

#### Definition

$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

#### Definition

$F : A → B, G, H : B → C, γ : G → H, γ F : G F → H F, a : A, γ_[F(a)], b : B, K(γ_b).$

#### Lemma

$F, G : A → B, H, K : B → C, γ : F → G, δ : H → K,(δ G) (H γ) = (K γ) (δ F).$

#### Lemma

$H (G F) = (H G) F.$  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).

## Equivalence

#### Definition

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

#### Lemma

$F : A → B →(A ≃ B) = (G : B → A) × (G F ≃ 1_A) × (F G ≃ 1_B).$

### Injective

$F : A → B → F_[a, b]$

'Faithful'.

### Surjective

$F : A → B → F_[a, b]$

'Full'.

### Split Essentially Surjective

$F : A → B →(b : B) → (a : A) × F(a) ≃ b.$

#### Lemma

$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.$

#### Lemma

$F is bijective, A : Category →(b : B) → is-truncated_[−1]((a : A) × F(a) ≃ b). F is an equivalence = F is a week equivalence.$

### Isomorphism

F is bijective and F_0 is an equivalence of types. A ≅ B.

#### Lemma

$A, B : Precategory, F : A → B →(A ≅ B)≃ ≃.$

#### Lemma

$A, B : Precategory →(A = B) → (A ≅ B).$

#### Lemma

$A, B : Category →(A = B) → (A ≃ B).$

### Dual  $A : Precategory → A^* : Precategory, A^*_0 ≡ A_0, a →_[A^*] b ≡ A → B.$

### Product

$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').$

#### Lemma

$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  $A : Precategory, a : A, F : 𝑆𝑒𝑡^[A^*] →(y a →_[𝑆𝑒𝑡^[A^*]] F) ≅ F(a).$

#### Corollary

$y : A → 𝑆𝑒𝑡^[A^*] is bijective.$

#### Corollary

$A : Category → y_0 : A_0 → (𝑆𝑒𝑡^[A^*])_0 is an embedding.(y a = y b) → (a = b).$

### Representable

$F : 𝑆𝑒𝑡^[A^*] →(a : A) × y a ≅ F.$

#### Lemma

$A, B : Precategory, F : A → B → is-left-adjoint(F) ≃ (b : B) → is-representable(a ↦ F(a) →_b b).$

## Strict Category $A : Precategory, A_0 ≡ 0-type.$

### Monomorphism  $(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).$

#### Definition

$P(x) ≡ P_0(x) × P_1(x), P_0(x) ≡ (ω : Ω_0) → x_[|ω|] → x, P_1(x) ≡ (ω : Ω_1) → x_[|ω|] → (−1)-type_U.$

## Rezk Completion

#### Lemma

$(g : F(b) →_C G(b)) × (a : A) → (f : H(a) ≃ b) → (γ_a) = G(f^[−1]) g F(f).$

#### Theorem

$(- H) : C_b → C_a.$

#### Theorem

$A → A_^.$

## Diagonal Functor $C → C × C. a × b : Δ → .$

## Functor Category $F, G : C → D → η : F → G, Component of η at X η_X : F(X) → G(X), f : X → Y, η_Y ○ F(f) = G(f) ○ η_X.$

## Diagram    ### Commutative Diagram  ## Groupoid  $f : 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 ## Category of Sets  ## Category of Groups  ## Category of Modules  ## Category of Manifolds ## Categorification  ## Decategorification ## Indexed category  ## Limit ## Coinduction  ## Corecursion 