4 Higher Category🔗ℹ

In this chapter, we’ll explore more sophisticated and generalized frameworks such as 2-categories and bicategories. These higher-dimensional constructs extend the notion of categories by introducing additional layers of structure, enabling us to model more complex relationships and interactions between objects and morphisms through a higher category.

4.1 2-Category🔗ℹ

A set (0-category) is defined by a collection of elements (0-cells). Extending this idea, a category (1-category) is defined by two collections: objects (0-cells) and morphisms (1-cells). Importantly, in a category, objects can be seen as identity morphisms, a special case of morphisms.

This natural progression leads us to consider whether we can extend our abstraction to include 2-morphisms (2-cells). In other words, we can think about constructing a 2-category, which is defined by not only 0-cells and 1-cells but also 2-cells. Just as in a 1-category, each 0-cell is an identity 1-cell, in a 2-category, each 1-cell is an identity 2-cell.

We already have an example of such a structure: 𝐂𝐚𝐭. In 𝐂𝐚𝐭, categories serve as 0-cells, functors act as 1-cells, and natural transformations provide the additional layer of abstraction as 2-cells. This makes 𝐂𝐚𝐭 a natural reference for understanding the concept of 2-categories.

To formalize this idea, we look at how 𝐂𝐚𝐭 operates. There are two distinct composition operations for natural transformations within 𝐂𝐚𝐭: horizontal composition and vertical composition. The interaction between these two forms of composition follows the interchange law. We can describe 𝐂𝐚𝐭 in terms of three interrelated categories: the base category 𝐂𝐚𝐭ᵇ, the horizontal category 𝐂𝐚𝐭ʰ, and the vertical category 𝐂𝐚𝐭ᵛ.

Note that 𝒞2 of a 1-category 𝒞 is the collection of composable pairs.

Using these properties, we define a 2-category 𝐂 as a structure consisting of three collections: 𝐂i of i-morphisms (i-cells) for i = 0, 1, 2. In 𝐂, there are two ways to compose 2-cells: horizontal composition and vertical composition, which satisfy the interchange law. Additionally, 𝐂 can be described in terms of three 1-categories:

• The base category 𝐂b: 𝐂b0 = 𝐂0 and 𝐂b1 = 𝐂1.

• The horizontal category 𝐂h: 𝐂h0 = 𝐂0 and 𝐂h1 = 𝐂2.

• The vertical category 𝐂v: 𝐂v0 = 𝐂1 and 𝐂v1 = 𝐂2.

An isomorphism α : F ⇒ G in 𝐂v is called a 2-isomorphism, and F and G are 2-isomorphic to each other.

In a category 𝒞, the morphisms from a to x form a hom set 𝒞(a, x). This structure naturally extends in a 2-category 𝐂: the 1-cells from 𝒜 to 𝒳 and their corresponding 2-cells form a hom category 𝐂(𝒜, 𝒳), where the composition of morphisms is precisely the vertical composition of 2-cells in 𝐂.

Exercise: Show that every functor category [𝒞 → 𝒟] is the hom category 𝐂𝐚𝐭(𝒞, 𝒟).

To verify the properties of 2-categories, we define some check procedures to automate the testing of essential properties within a 2-category:

"code/higher_category/check.rkt"

#lang racket/base

(require rackunit)

(provide (all-defined-out))

(define (check-2-cat 𝐂)

(define-values (domᵛ𝐂 codᵛ𝐂 ∙𝐂 domʰ𝐂 codʰ𝐂 ∘𝐂 ?𝐂 =𝐂) (𝐂))

(λ (𝒞 𝒟 ℰ F G H K L M α0 β0 α1 β1)

(check-pred ?𝐂 𝒞) (check-pred ?𝐂 𝒟) (check-pred ?𝐂 ℰ)

(check-pred ?𝐂 F) (check-pred ?𝐂 G) (check-pred ?𝐂 H)

(check-pred ?𝐂 K) (check-pred ?𝐂 L) (check-pred ?𝐂 M)

(check-pred ?𝐂 α0) (check-pred ?𝐂 β0)

(check-pred ?𝐂 α1) (check-pred ?𝐂 β1)

;; Existence of identity 1-cells

(check-true (=𝐂 𝒞 (domʰ𝐂 𝒞) (codʰ𝐂 𝒞)))

;; Existence of identity 2-cells

(check-true (=𝐂 F (domᵛ𝐂 F) (codᵛ𝐂 F)))

;; Identity 1-cells are also identity 2-cells

(check-true (=𝐂 𝒞 (domᵛ𝐂 𝒞) (codᵛ𝐂 𝒞)))

;; Existence of vertical composition

(check-true (=𝐂 G (codᵛ𝐂 α0) (domᵛ𝐂 β0)))

(check-true (=𝐂 F (domᵛ𝐂 (∙𝐂 β0 α0)) (domᵛ𝐂 α0)))

(check-true (=𝐂 H (codᵛ𝐂 (∙𝐂 β0 α0)) (codᵛ𝐂 β0)))

;; Existence of horizontally composition

(check-true (=𝐂 𝒟 (codʰ𝐂 α0) (domʰ𝐂 α1)))

(check-true (=𝐂 𝒞 (domʰ𝐂 (∘𝐂 α1 α0)) (domʰ𝐂 α0)))

(check-true (=𝐂 ℰ (codʰ𝐂 (∘𝐂 α1 α0)) (codʰ𝐂 α1)))

;; Domain/codomain alignment for 2-cells

(check-true (=𝐂 𝒞 (domʰ𝐂 α0) (domʰ𝐂 (domᵛ𝐂 α0)) (domʰ𝐂 (codᵛ𝐂 α0))))

(check-true (=𝐂 𝒟 (codʰ𝐂 α0) (codʰ𝐂 (domᵛ𝐂 α0)) (codʰ𝐂 (codᵛ𝐂 α0))))

;; Source/target preservation under horizontal composition

(check-true (=𝐂 (∘𝐂 K F) (domᵛ𝐂 (∘𝐂 α1 α0)) (∘𝐂 (domᵛ𝐂 α1) (domᵛ𝐂 α0))))

(check-true (=𝐂 (∘𝐂 L G) (codᵛ𝐂 (∘𝐂 α1 α0)) (∘𝐂 (codᵛ𝐂 α1) (codᵛ𝐂 α0))))

;; Interchange law

(check-true (=𝐂 (∙𝐂 (∘𝐂 β1 β0) (∘𝐂 α1 α0)) (∘𝐂 (∙𝐂 β1 α1) (∙𝐂 β0 α0))))))

(define (check-oo2c 𝐂)

(define-values (domᵛ𝐂 codᵛ𝐂 ∙𝐂 domʰ𝐂 codʰ𝐂 ∘𝐂 ?𝐂 =𝐂) (𝐂))

(define ∗ (∘𝐂))

(check-pred ?𝐂 ∗)

(check-true (=𝐂 ∗ (domʰ𝐂 ∗) (codʰ𝐂 ∗)))

(define check-𝐂 (check-2-cat 𝐂))

(λ (F G H K L M α0 β0 α1 β1) (check-𝐂 ∗ ∗ ∗ F G H K L M α0 β0 α1 β1)))

The following code demonstrates a 2-category example in Racket:

"code/higher_category/PRel.rkt"

#lang typed/racket/base/no-check

(require racket/set racket/promise

"../category/Pair.rkt"

"../category/Rel.rkt")

(provide 𝐏𝐑𝐞𝐥)

(define (𝐏𝐑𝐞𝐥 . _) (values domᵛ codᵛ ∙ domʰ codʰ ∘ ? =))

(define-values (dom𝒫 cod𝒫 ∘𝒫 ?𝒫 =𝒫) (𝐏𝐚𝐢𝐫))

(define-values (domℛ codℛ ∘ℛ ?ℛ =ℛ) (𝐑𝐞𝐥))

(define domᵛ dom𝒫)

(define codᵛ cod𝒫)

(define ∙ ∘𝒫)

(define (domʰ m) (define a (domℛ (car m))) (cons a a))

(define (codʰ m) (define b (codℛ (cdr m))) (cons b b))

(define ∘

(case-λ

[(m) m]

[(m1 m2)

(define a (∘ℛ (car m1) (car m2)))

(define b (∘ℛ (cdr m1) (cdr m2)))

(cons a b)]

[(m1 m2 . m*) (apply ∘ (∘ m1 m2) m*)]))

(define =

(case-λ

[(_) #t]

[(m1 m2)

(and (=ℛ (car m1) (car m2))

(=ℛ (cdr m1) (cdr m2)))]

[(m1 m2 . m*) (and (= m1 m2) (apply = m2 m*))]))

(define (? m)

(and (?𝒫 m)

(let ([a (car m)] [b (cdr m)])

(and (?ℛ a) (?ℛ b)

(=ℛ (domℛ a) (domℛ b))

(=ℛ (codℛ a) (codℛ b))))))

(module+ test

(require "check.rkt" rackunit)

;; Relations

(define c (relation (lazy c) (lazy c) (set '(c0 . c0) '(c1 . c1) '(c2 . c2))))

(define d (relation (lazy d) (lazy d) (set '(d0 . d0) '(d1 . d1) '(d2 . d2))))

(define e (relation (lazy e) (lazy e) (set '(e0 . e0) '(e1 . e1) '(e2 . e2))))

(define f (relation (lazy c) (lazy d) (set '(c0 . d0) '(c1 . d1) '(c2 . d2))))

(define g (relation (lazy c) (lazy d) (set '(c0 . d1) '(c1 . d2) '(c2 . d0))))

(define h (relation (lazy c) (lazy d) (set '(c0 . d2) '(c1 . d0) '(c2 . d1))))

(define k (relation (lazy d) (lazy e) (set '(d0 . e0) '(d1 . e1) '(d2 . e2))))

(define l (relation (lazy d) (lazy e) (set '(d0 . e1) '(d1 . e2) '(d2 . e0))))

(define m (relation (lazy d) (lazy e) (set '(d0 . e2) '(d1 . e0) '(d2 . e1))))

;; 0-cells

(define 𝒞 (cons c c))

(define 𝒟 (cons d d))

(define ℰ (cons e e))

;; 1-cells

(define F (cons f f))

(define G (cons g g))

(define H (cons h h))

(define K (cons k k))

(define L (cons l l))

(define M (cons m m))

;; 2-cells

(define α0 (cons f g))

(define β0 (cons g h))

(define α1 (cons k l))

(define β1 (cons l m))

(define check-𝐏𝐑𝐞𝐥 (check-2-cat 𝐏𝐑𝐞𝐥))

(check-𝐏𝐑𝐞𝐥 𝒞 𝒟 ℰ F G H K L M α0 β0 α1 β1))

In a general 2-category, we may not know the specific internal structure of the 1-cells. However, we can draw inspiration from the concept of global elements. In 𝐂𝐚𝐭, any category 𝒞 is isomorphic to 𝒞1. This observation motivates us to define a similar concept in any 2-category 𝐂 that contains a terminal object 1. Specifically, for any 0-cell 𝒞 : 𝐂, we define the 1-cells from 1 to 𝒞 as the global objects of 𝒞, and the 2-cells between them as the global morphisms of 𝒞.

Having introduced the concept of 2-categories, we naturally consider the mappings between 2-categories. Just as 0-functors (functions) map between 0-categories and 1-functors (functors) map between 1-categories by preserving their structure, 2-functors map between 2-categories, preserving the richer structure.

To define a 2-functor, we note that a 2-category 𝐂 consists of three collections: 𝐂0, 𝐂1 and 𝐂2. Consequently, a 2-functor F : 𝐂 → 𝐃 consists of three functions: F0 : 𝐂0 → 𝐃0, F1 : 𝐂1 → 𝐃1, and F2 : 𝐂2 → 𝐃2. Additionally, F can be described in terms of three 1-functors:

• The base functor Fb : 𝐂b → 𝐃b: Fb0 = F0 and Fb1 = F1.

• The horizontal functor Fh : 𝐂h → 𝐃h: Fh0 = F0 and Fh1 = F2.

• The vertical functor Fv : 𝐂v → 𝐃v: Fv0 = F1 and Fv1 = F2.

4.1.1 Strict Monoidal Category🔗ℹ

A strict monoidal category (𝒞, ⊗, I) is a category 𝒞 equipped with a tensor product ⊗ and a tensor unit I. The tensor product is a bifunctor ⊗ : 𝒞×𝒞 → 𝒞, and the tensor unit is a unit object I : 𝒞, such that for all morphisms f, g, h in 𝒞,

(f⊗g)⊗h = f⊗(g⊗h)

and

f = f⊗idI = idI⊗f

Exercise: Prove the interchange law: (g0⊗g1)∘(f0⊗f1) = (g0∘f0)⊗(g1∘f1).

If 𝒞 is a discrete category, i.e., a set, then the strict monoidal category (𝒞, ⊗, I) reduces to a monoidal set. In this case, ⊗ becomes an associative binary operation and I becomes the identity element of 𝒞. This structure corresponds exactly to what we call a monoid. Hence, monoidal set and monoid are the same concept.

Just as a one-object category 𝒞 can be viewed as a monoid (𝒞1, ∘, id∗), we extend this idea to view a one-object 2-category 𝐂 as a strict monoidal category (𝐂v, ∘, idb∗). In this context, the vertical category 𝐂v is equipped with the horizontal composition ∘, which acts as the tensor product, and the identity 1-cell idb∗, which serves as the tensor unit.

The following is an example of a strict monoidal category:

"code/higher_category/Matr.rkt"

#lang typed/racket/base/no-check

(require math/array math/matrix)

(provide 𝐌𝐚𝐭𝐫)

(define (𝐌𝐚𝐭𝐫 . _) (values dom cod ∘ domʰ codʰ ⊗ ? =))

;; 0-cell

(define I #;(identity-matrix 0) (build-simple-array #(0 0) (λ (_) (error ""))))

(define (domʰ m) I)

(define (codʰ m) I)

(: ⊗ (∀ ([a : ℳ] [b : ℳ] [x : ℳ] [y : ℳ]) (→ (× (→ℳ a b) (→ℳ x y)) (→ℳ (⊗ a x) (⊗ b y)))))

(define (⊗ . m*)

(let ([m* (remq* (list I) m*)])

(if (null? m*) I (block-diagonal-matrix m*))))

(define (dom m) (define n (vector-ref (array-shape m) 1)) (if (zero? n) I (identity-matrix n)))

(define (cod m) (define n (vector-ref (array-shape m) 0)) (if (zero? n) I (identity-matrix n)))

(define (∘ m . m*) (apply matrix* m m*))

(define (? m) (and (array? m) (eqv? 2 (array-dims m))))

(define =

(case-λ

[(_) #t]

[(m1 m2) (and (array= m1 m2) #t)]

[(m1 m2 . m*) (and (= m1 m2) (apply = m2 m*))]))

(module+ test

(require "check.rkt" rackunit)

(define (rand m n) (random 1 9))

;; 1-cells

(define F (identity-matrix 1))

(define G (identity-matrix 2))

(define H (identity-matrix 3))

(define K (identity-matrix 4))

(define L (identity-matrix 5))

(define M (identity-matrix 6))

;; 2-cells

(define α0 (build-matrix 2 1 rand))

(define β0 (build-matrix 3 2 rand))

(define α1 (build-matrix 5 4 rand))

(define β1 (build-matrix 6 5 rand))

(define check-𝐌𝐚𝐭𝐫 (check-oo2c 𝐌𝐚𝐭𝐫))

(check-𝐌𝐚𝐭𝐫 F G H K L M α0 β0 α1 β1))

Exercise: Show that every endofunctor category is a strict monoidal category.

4.1.1.1 Strict Symmetric Monoidal Category🔗ℹ

A strict symmetric monoidal category (𝒞, ⊗, I) is a strict monoidal category that ⊗ is symmetric: for all morphisms f, g in 𝒞, f⊗g = g⊗f.

4.1.2 String Diagram🔗ℹ

Traditional diagrams represent 0-cells as nodes, 1-cells as single arrows between these nodes, and 2-cells as double arrows between these single arrows. In contrast, string diagrams provide a more intuitive and geometrical representation:

• 0-cell is represented by a portion of a plane.

• 1-cell is represented by a string separating the plane in two.

• 2-cell is represented by an intersection of strings.

String diagrams are a powerful tool for visualizing relationships between i-cells within a 2-category 𝐂. Below, we illustrate a 2-cell α : F ⇒ G : 𝒞 → 𝒟 : 𝐂, using both a traditional diagram and a corresponding string diagram:

By default, string diagrams are read from right to left and from bottom to top.

We also use special notations in string diagrams:

• The identity 1-cell is represented by a dashed line or may be omitted entirely for simplicity.

• Curved lines or arcs can also be used to represent 1-cells, and their intersection represents a 2-cell.

The following two examples illustrate the special notations used in string diagrams. These string diagrams show equivalent but visually distinct representations of the same structures.

The first one shows a 2-cell α : G∘F ⇒ id𝒞, where F : 𝒞 → 𝒟 : 𝐂 and G : 𝒟 → 𝒞 : 𝐂:

The second one shows two 2-cells α : G∘F ⇒ id𝒞 and β : id𝒟 ⇒ H∘G, where F : 𝒞 → 𝒟 : 𝐂, G : 𝒟 → 𝒞 : 𝐂, and H : 𝒞 → 𝒟 : 𝐂:

The advantage of using string diagrams lies in their simplicity when representing complex structures in a 2-category. Instead of working with layers of nodes and arrows, string diagrams allow us to represent these relationships in a clear, visual manner that highlights how each part of the structure interacts with the others.

Exercise: The following is a string diagram, try to draw the corresponding diagram.

If there are no 2-cells in a string diagram, we can further compress it for simplicity. Specifically:

• 0-cell is represented by a line segment.

• 1-cell is represented by a point separating the line in two.

This compressed representation is not limited to 𝐂b but can also be extended to other 1-categories.

4.1.3 Equivalence🔗ℹ

In a 2-category 𝐂, equivalence is a weaker version of isomorphism. For 1-cells F: 𝒞 → 𝒟 : 𝐂 and G: 𝒟 → 𝒞 : 𝐂, if id𝒞 ≅ G∘F and F∘G ≅ id𝒟, then F and G are both equivalences (often called be weakly invertible).

In this case, both F and G are inverses up to 2-isomorphisms η : id𝒞 ⇒ G∘F and ϵ : F∘G ⇒ id𝒟. G is a pseudo-inverse of F, and F is a pseudo-inverse of G. 𝒞 and 𝒟 are equivalent to each other (𝒞 ≃ 𝒟) if there exists an equivalence between them.

Exercise: Prove that if η and ϵ are identities, then 𝒞 ≅ 𝒟.

Exercise: Prove that ≃ is an equivalence relation over 𝐂0.

Exercise: Prove that every 0-cell is equivalent to itself.

Exercise: Prove that the pseudo-inverse of an equivalence is not unique.

4.1.3.1 Equivalence of Categories🔗ℹ

In a category, we often focus on its "essential structure" by treating isomorphic objects as the same. To formalize this idea, we introduce the concept of a skeleton.

A skeleton of a category 𝒞 is a full subcategory, denoted by sk𝒞, where any two isomorphic objects are equal. A category is called a skeletal category if all its isomorphisms are automorphisms. More strictly, a category is called a gaunt category (stiff category) if all its isomorphisms are identities.

A skeleton sk𝒞 comes with a functor S : 𝒞 → sk𝒞, which is fully faithful, and surjective on objects. This means that S preserves the structure of 𝒞 while collapsing isomorphic objects into a single entity. Conversely, by involving the axiom of choice, we can define an inclusion functor I : sk𝒞 → 𝒞.

Exercise: Prove S∘I = idsk𝒞 and I∘S ≅ id𝒞.

By constructing a skeleton sk𝒞, we capture the "essential structure" of 𝒞. A natural question arises: if sk𝒞 ≅ sk𝒟, what is the relationship between 𝒞 and 𝒟? This relationship is precisely equivalence: since 𝒞 ≃ sk𝒞, sk𝒞 ≅ sk𝒟, and sk𝒟 ≃ 𝒟, it follows by transitivity that 𝒞 ≃ 𝒟.

Conversely, we can also show that if 𝒞 ≃ 𝒟, then their skeletons are isomorphic to each other. Assume we have functors S : 𝒞 → sk𝒞 and T : 𝒟 → sk𝒟, as well as the inclusion functors I : sk𝒞 → 𝒞 and J : sk𝒟 → 𝒟, and equivalences F : 𝒞 → 𝒟 and G : 𝒟 → 𝒞. We can then construct functors TFI : sk𝒞 → sk𝒟 and SGJ : sk𝒟 → sk𝒞.

These satisfy: idsk𝒞 = SI ≅ SGFI ≅ SGJTFI = SGJ∘TFI and TFI∘SGJ = TFISGJ ≅ TFGJ ≅ TJ = idsk𝒟. Thus, sk𝒞 ≃ sk𝒟. Moreover, by definition, all objects in sk𝒞 and sk𝒟 are only isomorphic to themselves, so sk𝒞 ≅ sk𝒟.

This proposition relies on the axiom of choice. To avoid this assumption, F can be required to be split essentially surjective. For further details, see nLab.

Exercise: Prove that a functor F is weakly invertible iff it is fully faithful and essentially surjective.

4.2 Bicategory🔗ℹ

By considering vertical composition, we can examine whether two 1-cells are isomorphic. Since ≅ serves as a weakened form of =, this motivates us to replace structures originally defined by the equality of 1-cells with those defined via isomorphism, thereby obtaining weaker structures.

We apply this idea to the definition of a category. In a category, the composition of morphisms must satisfy the following lows:

• (h∘g)∘f = h∘(g∘f)

• f = f∘ida = idb∘f

A bicategory is also called a weak 2-category, and a 2-category is also called a strict 2-category。

To derive a weaker structure by using ≅, we require vertical composition. The horizontal composition is then weakened, leading to a bicategory, where the horizontal composition of 1-cells must satisfy the following laws:

• (h∘g)∘f ≅ h∘(g∘f)

• f ≅ f∘ida ≅ idb∘f

To formally define a bicategory 𝐁, we proceed as follows:

1. 0-cells

   The collection of 0-cells is denoted as 𝐁0.

2. Hom Categories

   For each pair of 0-cells of a, b in 𝐁, there exists a hom category 𝐁(a, b). The objects in each hom category are called 1-cells, denoted as 𝐁1, and the morphisms are called 2-cells (identity morphisms are called identity 2-cells), denoted as 𝐁2. The vertical composition of 2-cells is given by the composition within each hom category.

3. In practice, the identity 1-cell at a is often denoted simply as ida, omitting explicit reference to the functor.

   Identity 1-cells

   For each 0-cell a in 𝐁, there is an associated identity 1-cell. Specifically, there is a functor of type

   1 → 𝐁(a, a)

   that maps ∗ to the identity 1-cell at a. By convention, this functor is named a.

   

4. Horizontal Composition

   For each triple of 0-cells a, b, c in 𝐁, there is a bifunctor

   ∘abc : 𝐁(b, c)×𝐁(a, b) → 𝐁(a, c)

   called the horizontal composition.

   

5. Associator

   For each quadruple of 0-cells a, b, c, d in 𝐁, there is a natural isomorphism

   αabcd : ∘abd∘(∘bcd×id𝐁(a, b)) ⇒ ∘acd∘(id𝐁(c, d)×∘abc)

   between functors of type

   𝐁(c, d)×𝐁(b, c)×𝐁(a, b) → 𝐁(a, d)

   called the associator.

   

6. Unitors

   For each pair of 0-cells a, b in 𝐁, there are natural isomorphisms

   λab : ∘abb∘(b×id𝐁(a, b)) ⇒ id𝐁(a, b)

   and

   ρab : ∘aab∘(id𝐁(a, b)×a) ⇒ id𝐁(a, b)

   between functors of type

   𝐁(a, b) → 𝐁(a, b)

   called the left unitor and the right unitor, respectively.

   

To ensure the coherence of these natural isomorphisms, a bicategory must satisfy the following two axioms, which guarantee that all formal diagrams — diagrams involving only associators, unitors, their inverses, identities, horizontal composition and vertical composition — are commutative:

1. Pentagon Axiom

   For any five composable 1-cells, the pentagon formal diagram is commutative:

   

2. Triangle Axiom (Unity Axiom)

   For any two composable 1-cells, the triangle formal diagram is commutative:

   

These two axioms can be intuitively understood through string diagrams, where horizontal composition of 1-cells naturally forms binary trees, much like how LISP code inherently represents syntax trees.

Just as LISP represents (list 'h 'g 'f) through (cons 'h (cons 'g (cons 'f null))), a bicategory represents composite 1-cells as right-nested binary trees:

In the binary tree representation:

• An associator performs a tree rotation (rearranging one node while preserving leaf order):

  

• Unitors eliminate identity 1-cells:

  

The two axioms are minimal conditions ensuring all formal diagrams are commutative:

• The pentagon axiom guarantees that different paths of tree rotations yield identical binary tree transformation:

  

• The triangle axiom ensures the left unitor and right unitor produce identical elimination of identity 1-cells:

  

In a strict 2-category, the pentagon axiom and triangle axiom collapse to equalities.

A bicategory can be seen as a weak 2-category where associators and unitors are natural isomorphisms. To recover a strict 2-category, we simply replace these natural isomorphisms with identities. Although bicategories do not explicitly require the interchange law, it emerges automatically when horizontal composition is defined as a bifunctor.