1 Category🔗ℹ

Welcome to the first chapter of our Category Theory in Programming tutorial! Here, we delve into the foundational concepts of category theory, focusing on morphisms as the central entities of study. This chapter sets the stage for understanding how these entities interact within the structured universe of categories, using Racket programming language as our exploration tool.

1.1 Category🔗ℹ

In the abstract landscape of mathematics, category theory provides a unified framework that allows us to analyze and integrate concepts across diverse fields. At the core of this exploration are morphisms, which we treat not just as connections or processes, but as fundamental entities in their own right.

This tutorial does not distinguish small category and large category. For more information on small and large category, please refer to Small Category and Large Category.

A category 𝒞 is defined by two collections: 𝒞0 of objects and 𝒞1 of morphisms. Think of 𝒞 as a digraph, where objects are nodes, and morphisms are arrows connecting these nodes. For a morphism f from an object a to an object b in a category 𝒞, denoted by f : a → b : 𝒞, its domain (source) is a, and its codomain (target) is b: dom𝒞(f) = a and cod𝒞(f) = b.

Our approach to category theory places morphisms at the core, viewing a category not just as a network of objects linked by morphisms, but as a universe where morphisms themselves are the primary focus. In this universe, objects serve more as structural markers than active participants, and morphisms are entities that can represent transformations, operations, or even concrete entities like numbers, lists, strings, and pairs, as long as they adhere to the composition rules:

1. Existence of composition

   For morphisms f and g in 𝒞, the composite g∘f is defined when cod𝒞(f) = dom𝒞(g), and in such cases, we have dom𝒞(g∘f) = dom𝒞(f) and cod𝒞(g∘f) = cod𝒞(g). This composition can also be written as f⨾g to highlight the flow from f to g.

   

2. Associativity of composition

   Note that a composable pair consists of not only a pair of morphisms, but also the domains and codomains of them. See more in nLab.

   For composable pairs (f, g) and (g, h) in 𝒞, composition is associative: (h∘g)∘f = h∘(g∘f), denoted by h∘g∘f.

   

3. Existence of identity morphisms

   Every object has an associated identity morphism. For an object a : 𝒞, its identity morphism is denoted by ida or 1a, and a = dom𝒞(ida) = cod𝒞(ida).

   

4. Composition and identity morphisms

   For a morphism f : a → b : 𝒞, f = f∘ida = idb∘f.

   

Let 𝒞2 be the collection of composable pairs in 𝒞. We can describe 𝒞 with the following diagram:

In traditional category theory, categories are often named after their objects.

In this tutorial, we intentionally use morphisms to label categories. This approach emphasizes the role of morphisms as the central focus.

Nevertheless, classic category names will still be given precedence and used whenever applicable in this tutorial.

In traditional category theory, a distinction is often made between objects and identity morphisms. However, in this tutorial, we adopt a unique perspective by using identity morphisms to directly represent objects. There is no strict demarcation between objects and their associated identity morphisms; they are treated interchangeably (a = ida).

Remember, while it may seem that objects take a secondary role, their presence as identity morphisms is essential for facilitating the dynamic interplay of morphisms, which are the focal point of our study.

We’ve laid the groundwork for understanding the fundamental principles of category theory. If you’re eager to see how these abstract concepts translate into practical programming examples, feel free to jump to Mapping Category to Programming. There, we’ll explore how the ideas of objects, morphisms, and compositions come to life in the Racket programming environment, providing concrete examples.

1.1.1 Discrete Category🔗ℹ

A discrete category is a category where the only morphisms are the identity morphisms. In other words, every object is only connected to itself via its identity morphism. Since a set is defined by a collection of elements, this means that a discrete category can be viewed as the category version of a set: the objects of the discrete category correspond to the elements of the set.

Beyond sets, there are a few related terms that are commonly used:

• Collection: A more informal term used to describe a bunch of things, without assuming they necessarily form a formal structure, such as a set. This term is often used to avoid the strict assumptions of set theory.

• Family: An indexed collection.

• Class: A collection of mathematical objects defined by a common property that all its members share.

1.1.2 One-Object Category🔗ℹ

A monoid (S, ∘, s) is a set S equipped with an associative binary operation ∘ and an identity element s.

A monoid can be viewed as a one-object category (OOC). In OOC, there is only a single object, usually denoted by ∗, and morphisms are defined within the context of ∗.

The monoid structure becomes evident when we consider the collection of all morphisms within the OOC as the set S, the identity morphism id∗ as the monoid identity element s, and the composition operation as the monoid operation ∘. Thus, OOCs provide a categorical perspective on monoids.

1.1.3 Thin Category🔗ℹ

A preordered set (proset) (S, ≤) is a set S equipped with a binary relation ≤ over S that is reflexive and transitive. ≤ is called a preorder on S.

A proset can be viewed as a thin category in which any parallel morphisms are equal.

The proset structure becomes evident when we consider the objects as the elements of S, and a morphism from a to b exists iff a ≤ b. There is exactly one such morphism for any comparable pair a and b.

A partially ordered set (ordered set, or poset) (S, ≤) is a special preordered set, in which ≤ is antisymmetric. ≤ is called a partial order on S.

The poset can be viewd as a special thin category, where for any objects a and b, if there are morphisms a ≤ b and b ≤ a, then a = b, and these morphisms are the same identity morphism.

A totally ordered set (toset) (S, ≤) is a special ordered set, in which ≤ is total. ≤ is called a total order on S.

The toset can be viewd as a special thin category, where for any objects a and b, there must be exactly one morphism between them: a ≤ b or b ≤ a.

1.1.4 Cartesian Product🔗ℹ

Given two sets A0 and A1, the Cartesian product of them, denoted by A0×A1 or ∏i=0, 1Ai, is the set of all ordered lists: ∏i=0, 1Ai = A0×A1 ≔ {(a0, a1) | a0 ∈ A0, a1 ∈ A1}. This set is called a product set.

1.1.5 Disjoint Union🔗ℹ

Given two sets A0 and A1, the disjoint union (tagged union) of them, denoted by A0+A1 or ∐i=0, 1Ai, is the set of all tagged pairs: ∐i=0, 1Ai = A0+A1 ≔ ∪i=0, 1{(a, i) | a ∈ Ai}. This set is called a sum set.

If A0∩A1 = {}, then A0∪A1 can also be viewed as the disjoint union of A0 and A1. A tagged union is just one way to implement a disjoint union, using natural numbers as tags to distinguish identical elements from different sets.

1.1.6 Hom Set🔗ℹ

If the morphisms from a to x do not constitute a set, we use the term hom class instead of hom set.

For objects a and x in 𝒞, the hom set (external hom) of them, denoted by Hom𝒞(a, x) or 𝒞(a, x), is the set of all morphisms from a to x: Hom𝒞(a, x) ≔ {f ∈ 𝒞1 | dom𝒞(f) = a ∧ cod𝒞(f) = x}. If 𝒞(a, x) is an object in 𝒞, it is called the internal hom [a, x] or [a → x] (exponential set xa).

For morphisms f : a → x : 𝒞, i : b → a : 𝒞 and j : x → y : 𝒞, we can define a hom function Hom𝒞(i, j) : Hom𝒞(a, x) → Hom𝒞(b, y), where Hom𝒞(i, j)(f) ≔ j∘f∘i.

Additionally, we can define two other hom functions:

1. Hom𝒞(a, j) ≔ Hom𝒞(ida, j), where Hom𝒞(a, j)(f) = j∘f.

   

2. Hom𝒞(i, x) ≔ Hom𝒞(i, idx), where Hom𝒞(i, x)(f) = f∘i.

   

1.1.7 Relation🔗ℹ

A relation over some sets is a subset of the Cartesian product of them.

1.1.7.1 Binary Relation🔗ℹ

A binary relation from a set S to a set T is a relation over S and T.

The diagonal relation (equality relation) over a set S, denoted by ΔS, is the binary relation over S: {(x, x) | x ∈ S}.

Here’re some properties that a binary relation ∼ over a set S may have:

• Symmetry: ∼ is symmetric if ∀x, y ∈ S, x ∼ y ⇒ y ∼ x.

• Antisymmetry: ∼ is antisymmetric if ∀x, y ∈ S, x ∼ y ∧ y ∼ x ⇒ x = y.

• Reflexivity: ∼ is reflexive if ∀x ∈ S, x ∼ x.

• Transitivity: ∼ is transitive if ∀x, y, z ∈ S, x ∼ y ∧ y ∼ z ⇒ x ∼ z.

• Totality: ∼ is total if ∀x, y ∈ S, x ∼ y ∨ y ∼ x.

A function f : S → T can be viewed as the binary relation: {(x, f(x)) | x ∈ S}. The image of f, denoted by im(f), is the subset of T: {f(x) | x ∈ S}.

f may have additional properties:

• Injective: f is an injection if it maps distinct elements of S to distinct elements of T. Formally, ∀x, y ∈ S, f(x) = f(y) ⇒ x = y.

  

• Surjective: f is a surjection if every element of T is the image of some element in S. Formally, ∀x ∈ T, ∃a ∈ S, x = f(a).

  

• Bijective: f is a bijection if it is both injective and surjective, establishing a one-to-one correspondence between the elements of S and T.

  

1.1.7.2 Equivalence Relation🔗ℹ

An equivalence relation ∼ over S is a binary relation that is reflexive, symmetric, and transitive. ∼ partitions S into disjoint classes, known as equivalence classes, where all elements within an equivalence class are related to each other. A setoid (extensional set) (S, ∼) is a set S equipped with an equivalence relation ∼.

For example, given a setoid (S, ∼) and an element x ∈ S, the equivalence class of x under ∼ is the set of all elements in S that are related to x. This is denoted by [x], where [x] ≔ {y ∈ S | x ∼ y}. Every element of S belongs to exactly one equivalence class.

Exercise: Prove x ∼ y ⇔ [x] = [y].

1.1.7.3 Congruence Relation🔗ℹ

A congruence relation ∼ on a category 𝒞 is an equivalence relation on the morphisms of 𝒞 that is compatible with the composition of morphisms. Formally, ∼ satisfies the following properties:

1. ∀a, b ∈ 𝒞0, a ∼ b ⇒ ida ∼ idb.

2. ∀f, g ∈ 𝒞1, f ∼ g ⇒ dom𝒞(f) ∼ dom𝒞(g) ∧ cod𝒞(f) ∼ cod𝒞(g).

3. ∀f, g ∈ Hom𝒞(b, c), ∀h ∈ Hom𝒞(a, b), ∀k ∈ Hom𝒞(c, d), f ∼ g ⇒ f∘h ∼ g∘h ∧ k∘f ∼ k∘g.

   

Exercise: Prove ∀a, b ∈ 𝒞0, ida ∼ idb ⇒ a ∼ b.

Exercise: Show that we can replace the second properties with: ∀f1, f2 ∈ Hom𝒞(a, b), ∀g1, g2 ∈ Hom𝒞(b, c), f1 ∼ f2 ∧ g1 ∼ g2 ⇒ g1∘f1 ∼ g2∘f2.

Exercise: Let ∼ and ∽ be congruence relations. Prove that ∼ ∩ ∽ is also a congruence relation.

A congruence class is an equivalence class under a congruence relation.

1.1.8 Commutative Diagram🔗ℹ

Informally, a diagram comprises various objects connected by various morphisms. When the morphisms with the same domain and codomain are the same one, the diagram is a commutative diagram.

Commutative diagrams serve as a powerful language for expressing equations.

1.1.8.1 Commutative Triangle🔗ℹ

A commutative triangle is a commutative diagram that has the shape of a triangle.

The equation h = g∘f can be pictured as a commutative triangle like this:

h is saied to factor through any (and all) of f, g, and b.

1.1.8.2 Commutative Square🔗ℹ

A commutative square is a commutative diagram that has the shape of a square.

The equation k∘f = g∘h can be pictured as a commutative square like this:

If there is a morphism l making h = l∘f and k = g∘l, then l is a lift (diagonal fill-in or filler) in the commutative square:

If a lift exists in any commutative square involving f and g, then we say that f is weakly orthogonal to g, or that (f, g) has the lifting property, denoted by f↓g or f⧄g. In this case, f has the left lifting property with respect to g, and g has the right lifting property with respect to f. If the lift is unique, we say that f is orthogonal to g, denoted by f⊥g.

From experience, if two morphisms f and g satisfy f⧄g, then f and g often possess opposite properties. This relationship reflects the complementary nature of their roles in a commutative square, where the lifting property typically holds due to these contrasting characteristics.

For a class 𝒞 of morphisms, the right weak orthogonal class (right Quillen negation) is denoted by 𝒞⧄, where 𝒞⧄ ≔ {g | f⧄g ∀f ∈ 𝒞}, and the left weak orthogonal class (left Quillen negation) is denoted by ⧄𝒞, where ⧄𝒞 ≔ {f | f⧄g ∀g ∈ 𝒞}. Similarly, the right orthogonal class is denoted by 𝒞⊥ or 𝒞↓, where 𝒞⊥ ≔ {g | f⊥g ∀f ∈ 𝒞}, and the left orthogonal class is denoted by ⊥𝒞 or 𝒞↑, where ⊥𝒞 ≔ {f | f⊥g ∀g ∈ 𝒞}.

Exercise: Prove 𝒞↓↑↓ = 𝒞↓ and 𝒞↑↓↑ = 𝒞↑.

1.1.8.3 Commutative Cube🔗ℹ

A commutative cube is a commutative diagram that has the shape of a cube.

1.2 Mapping Category to Programming🔗ℹ

In this section, we’ll explore how category theory concepts can be mapped to practical programming constructs.

Just as car, cdr, cons, pair?, and equal? provide an abstraction for pairs in Racket, we introduce the notions of dom, cod, ∘, ?, and = (representing domain, codomain, compose, predicate, and equal) to abstract over categories.

We stipulate that (∘) returns ∗, (∘ m) returns m, and (= m) returns #t in Racket.

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

"code/category/check.rkt"

#lang racket/base

(require rackunit)

(provide (all-defined-out))

(define (check-cat 𝒞)

(define-values (dom𝒞 cod𝒞 ∘𝒞 ?𝒞 =𝒞) (𝒞))

(λ (a b c d f g h)

(check-pred ?𝒞 a)

(check-pred ?𝒞 b)

(check-pred ?𝒞 c)

(check-pred ?𝒞 d)

(check-pred ?𝒞 f)

(check-pred ?𝒞 g)

(check-pred ?𝒞 h)

;; Existence of composition

(check-true (=𝒞 b (cod𝒞 f) (dom𝒞 g)))

(check-true (=𝒞 a (dom𝒞 (∘𝒞 g f)) (dom𝒞 f)))

(check-true (=𝒞 c (cod𝒞 (∘𝒞 g f)) (cod𝒞 g)))

;; Associativity of composition

(check-true (=𝒞 (∘𝒞 h g f) (∘𝒞 (∘𝒞 h g) f) (∘𝒞 h (∘𝒞 g f))))

;; Existence of identity morphisms

(check-true (=𝒞 a (dom𝒞 a) (cod𝒞 a)))

;; Composition and identity morphisms

(check-true (=𝒞 f (∘𝒞 f (dom𝒞 f)) (∘𝒞 (cod𝒞 f) f)))))

(define (check-ooc 𝒞)

(define-values (dom𝒞 cod𝒞 ∘𝒞 ?𝒞 =𝒞) (𝒞))

(define ∗ (∘𝒞))

(check-pred ?𝒞 ∗)

(check-true (=𝒞 ∗ (dom𝒞 ∗) (cod𝒞 ∗)))

(define check-𝒞 (check-cat 𝒞))

(λ (f g h) (check-𝒞 ∗ ∗ ∗ ∗ f g h)))

1.2.1 Category Examples🔗ℹ

Let’s see how these abstractions can be applied to create and manipulate categories in the context of programming.

1.2.1.1 Category of Natural Numbers🔗ℹ

The category of natural numbers, denoted as 𝐍𝐚𝐭, is an example of OOC. In 𝐍𝐚𝐭, morphisms are natural numbers, and the identity morphism of the single object ∗ is 0:

Remember that objects serve as identity morphisms.

"code/category/Nat.rkt"

#lang racket/base

(provide 𝐍𝐚𝐭)

(define (𝐍𝐚𝐭 . _) (values dom cod ∘ ? =))

(define (dom _) 0)

(define (cod _) 0)

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

(define (? m) (exact-nonnegative-integer? m))

(module+ test

(require "check.rkt")

;; Morphisms

(define f 1)

(define g 2)

(define h 3)

(define check-𝐍𝐚𝐭 (check-ooc 𝐍𝐚𝐭))

(check-𝐍𝐚𝐭 f g h))

1.2.1.2 Category of Lists🔗ℹ

The category of lists, denoted as 𝐋𝐢𝐬𝐭, is also an OOC. In 𝐋𝐢𝐬𝐭, morphisms are lists, and the identity morphism of the single object ∗ is null:

"code/category/List.rkt"

#lang racket/base

(provide 𝐋𝐢𝐬𝐭)

(define (𝐋𝐢𝐬𝐭 . _) (values dom cod ∘ ? =))

(define (dom _) '())

(define (cod _) '())

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

(define (? m) (list? m))

(define =

(case-λ

[(_) #t]

[(m1 m2) (equal? m1 m2)]

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

(module+ test

(require "check.rkt")

;; Morphisms

(define f '(1 2 3))

(define g '(a b c))

(define h '(A B C))

(define check-𝐋𝐢𝐬𝐭 (check-ooc 𝐋𝐢𝐬𝐭))

(check-𝐋𝐢𝐬𝐭 f g h))

1.2.1.3 Category of Strings🔗ℹ

The category of strings, denoted as 𝐒𝐭𝐫, is also an OOC.

Exercise: Using the example code provided above as a reference, implement 𝐒𝐭𝐫.

1.2.1.4 Category of Relations🔗ℹ

The category of relations, denoted as 𝐑𝐞𝐥, where morphisms are binary relations, and identity morphisms are diagonal relations:

"code/category/Rel.rkt"

#lang racket/base

(require racket/set racket/match racket/promise)

(provide (struct-out relation))

(struct relation (dom cod rel*))

(provide 𝐑𝐞𝐥)

(define (𝐑𝐞𝐥 . _) (values dom cod ∘ ? =))

(define (dom m) (force (relation-dom m)))

(define (cod m) (force (relation-cod m)))

(define ∘

(case-λ

[(m) m]

[(m1 m2)

(define r1* (relation-rel* m1))

(define r2* (relation-rel* m2))

(define r*

(set-remove

(for*/set ([r2 (in-set r2*)]

[r1 (in-set r1*)])

(match* (r2 r1)

[(`(,a . ,b) `(,b . ,c)) `(,a . ,c)]

[(_ _) #f]))

#f))

(relation (relation-dom m2) (relation-cod m1) r*)]

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

(define (? m) (relation? m))

(define =

(case-λ

[(_) #t]

[(m1 m2)

(and

(equal? (relation-rel*      m1)

(relation-rel*      m2))

(equal? (relation-rel* (dom m1))

(relation-rel* (dom m2)))

(equal? (relation-rel* (cod m1))

(relation-rel* (cod m2))))]

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

(module+ test

(require "check.rkt")

;; Objects

(define a (relation (lazy a) (lazy a) (set '(a0 . a0) '(a1 . a1) '(a2 . a2))))

(define b (relation (lazy b) (lazy b) (set '(b0 . b0) '(b1 . b1) '(b2 . b2))))

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

;; Morphisms

(define f (relation (lazy a) (lazy b) (set '(a0 . b0) '(a0 . b1) '(a2 . b0))))

(define g (relation (lazy b) (lazy c) (set '(b0 . c0) '(b0 . c1) '(b2 . c0))))

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

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

(check-𝐑𝐞𝐥 a b c d f g h))

1.2.1.5 Category of Pairs🔗ℹ

The category of pairs, denoted as 𝐏𝐚𝐢𝐫, where morphisms are pairs:

"code/category/Pair.rkt"

#lang racket/base

(require racket/match)

(provide 𝐏𝐚𝐢𝐫)

(define (𝐏𝐚𝐢𝐫 . _) (values dom cod ∘ ? =))

(define (dom m) (define o (car m)) (cons o o))

(define (cod m) (define o (cdr m)) (cons o o))

(define ∘

(case-λ

[(m) m]

[(m1 m2) (match* (m2 m1) [(`(,a . ,b) `(,b . ,c)) `(,a . ,c)])]

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

(define (? m) (pair? m))

(define =

(case-λ

[(_) #t]

[(m1 m2) (equal? m1 m2)]

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

(module+ test

(require "check.rkt")

;; Objects

(define a '(a . a))

(define b '(b . b))

(define c '(c . c))

(define d '(d . d))

;; Morphisms

(define f '(a . b))

(define g '(b . c))

(define h '(c . d))

(define check-𝐏𝐚𝐢𝐫 (check-cat 𝐏𝐚𝐢𝐫))

(check-𝐏𝐚𝐢𝐫 a b c d f g h))

Exercise: Prove that a thin category is a subcategory of 𝐏𝐚𝐢𝐫.

Exercise: Implement the toset ℕ as a thin category, where objects are natural numbers.

1.2.1.6 Category of Matrices🔗ℹ

The category of matrices, denoted as 𝐌𝐚𝐭𝐫, is a fascinating example that combines linear algebra with category theory. In 𝐌𝐚𝐭𝐫, each m×n matrix is considered a morphism, its domain is the n-order identity matrix, and its codomain is the m-order identity matrix:

"code/category/Matr.rkt"

#lang racket/base

(require math/matrix)

(provide 𝐌𝐚𝐭𝐫)

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

(define (dom m) (identity-matrix (matrix-num-cols m)))

(define (cod m) (identity-matrix (matrix-num-rows m)))

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

(define (? m) (matrix? m))

(define =

(case-λ

[(_) #t]

[(m1 m2) (matrix= m1 m2)]

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

(module+ test

(require "check.rkt")

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

;; Objects

(define a (identity-matrix 1))

(define b (identity-matrix 2))

(define c (identity-matrix 3))

(define d (identity-matrix 4))

;; Morphisms

(define f (build-matrix 2 1 rand))

(define g (build-matrix 3 2 rand))

(define h (build-matrix 4 3 rand))

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

(check-𝐌𝐚𝐭𝐫 a b c d f g h))

1.2.1.7 Category of Sets🔗ℹ

The category of sets, denoted as 𝐒𝐞𝐭, where morphisms are functions:

"code/category/Set.rkt"

#lang racket/base

(require racket/hash racket/promise)

(provide (struct-out function))

(struct function (dom cod map))

(provide 𝐒𝐞𝐭)

(define (𝐒𝐞𝐭 . _) (values dom cod ∘ ? =))

(define (dom m) (force (function-dom m)))

(define (cod m) (force (function-cod m)))

(define ∘

(case-λ

[(m) m]

[(m1 m2)

(define m1.map (function-map m1))

(define m2.map (function-map m2))

(define m.map

(for/hash ([(k2 v2) (in-hash m2.map)])

(define v1 (hash-ref m1.map v2))

(values k2 v1)))

(define m (function (function-dom m2) (function-cod m1) m.map))

m]

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

(define (? m) (function? m))

(define =

(case-λ

[(_) #t]

[(m1 m2)

(and

(equal? (function-map      m1)

(function-map      m2))

(equal? (function-map (dom m1))

(function-map (dom m2)))

(equal? (function-map (cod m1))

(function-map (cod m2))))]

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

(module+ test

(require "check.rkt")

;; Objects

(define a (function (lazy a) (lazy a) #hash([a . a] [  0  .   0 ] [  1  .   1 ])))

(define b (function (lazy b) (lazy b) #hash([b . b] [ |0| .  |0|] [ |1| .  |1|])))

(define c (function (lazy c) (lazy c) #hash([c . c] [ "0" .  "0"] [ "1" .  "1"])))

(define d (function (lazy d) (lazy d) #hash([d . d] [#"0" . #"0"] [#"1" . #"1"])))

;; Morphisms

(define f (function (lazy a) (lazy b) #hash([a . b] [  0  .  |0|] [  1  .  |0|])))

(define g (function (lazy b) (lazy c) #hash([b . c] [ |0| .  "0"] [ |1| .  "0"])))

(define h (function (lazy c) (lazy d) #hash([c . d] [ "0" . #"0"] [ "1" . #"0"])))

(define check-𝐒𝐞𝐭 (check-cat 𝐒𝐞𝐭))

(check-𝐒𝐞𝐭 a b c d f g h))