2 Functor🔗ℹ

In this chapter, we introduce the concept of functors. Functors are fundamental in category theory, as they map both objects and morphisms between categories while preserving the structural relationships between them.

To clarify the explanation and show how functors apply to programming, we will use Typed Racket syntax. Specifically, we will opt for #lang typed/racket/no-check instead of #lang racket. This choice allows us to incorporate type annotations for improved code clarity and better illustration of functorial properties.

2.1 Functor🔗ℹ

Functors are sometimes called category homomorphisms.

Just as functions map elements between sets, functors provide a way to map objects and morphisms between categories. This mapping preserves the structural aspects of categories.

For convenience, if a is an object in 𝒞, then F(a) = F0(a); if f is a morphism in 𝒞, then F(f) = F1(f).

Similar to how a category 𝒞 is defined by two collections 𝒞0 and 𝒞1, a functor F from 𝒞 to 𝒟, denoted by F : 𝒞 → 𝒟, is also defined by two functions F0 : 𝒞0 → 𝒟0 and F1 : 𝒞1 → 𝒟1. These functions must satisfy the following properties:

1. Preservation of domains and codomains

   For any morphism f : a → b : 𝒞, there must exist a corresponding morphism F(f) : F(a) → F(b) : 𝒟.

   

2. Preservation of identity morphisms

   For any object a : 𝒞, F(ida) = idF(a).

   

3. Preservation of composable pairs

   If (f, g) is a composable pair in 𝒞, then (F(f), F(g)) is a composable pair in 𝒟, and F(g∘f) = F(g)∘F(f).

   

Exercise: Show that a function between two sets can be viewed as a functor between two discrete categories.

A functor F : 𝒞 → 𝒟 is like a digraph homomorphism that also preserves composable pairs and identity morphisms. To illustrate F, let’s consider a function F2 : 𝒞2 → 𝒟2. Using F2, we can describe F with the following diagram:

The proof is left as an exercise.

We can see that each similarly labeled square in the diagram is a commutative square. Additionally, the commutative squares show the properties of functors.

To verify the properties of functors, we define some check procedures to automate the testing of essential properties a functor preserves:

"code/functor/check.rkt"

#lang racket/base

(require rackunit)

(provide (all-defined-out))

(define (check-ftr 𝒞 𝒟)

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

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

(λ (F)

(λ (a b c f g)

(check-pred ?𝒞 a) (check-pred ?𝒟 (F a))

(check-pred ?𝒞 b) (check-pred ?𝒟 (F b))

(check-pred ?𝒞 c) (check-pred ?𝒟 (F c))

(check-pred ?𝒞 f) (check-pred ?𝒟 (F f))

(check-pred ?𝒞 g) (check-pred ?𝒟 (F g))

;; Preservation of domain and codomain

(check-true (=𝒟 (F a) (dom𝒟 (F f)) (F (dom𝒞 f))))

(check-true (=𝒟 (F b) (cod𝒟 (F f)) (F (cod𝒞 f))))

;; Preservation of identity morphisms

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

(check-true (=𝒟 (F c) (dom𝒟 (F c)) (cod𝒟 (F c))))

;; Preservation of composable pairs

(check-true (=𝒟 (∘𝒟 (F g) (F f)) (F (∘𝒞 g f)))))))

The following example illustrates how to implement functors in Racket:

"code/functor/Set->Rel.rkt"

#lang typed/racket/base/no-check

(require "../category/Set.rkt"

"../category/Rel.rkt"

racket/promise)

(: 𝒮 𝐂𝐚𝐭)

(: dom𝒮 (∀ ([a : 𝒮] [b : 𝒮]) (→ (→𝒮 a b) a)))

(: cod𝒮 (∀ ([a : 𝒮] [b : 𝒮]) (→ (→𝒮 a b) b)))

(: ∘𝒮 (∀ ([a : 𝒮] [b : 𝒮] [c : 𝒮] ... [z : 𝒮]) (→ (× (→𝒮 a b) (→𝒮 b c) ...) (→𝒮 a z))))

(: ?𝒮 (pred (∀ ([a : 𝒮] [b : 𝒮]) (→𝒮 a b))))

(: =𝒮 (∀ ([a : 𝒮] [b : 𝒮] [c : 𝒮] [d : 𝒮] ...) (→ (× (→𝒮 a b) (→𝒮 c d) ...) Boolean)))

(define (𝒮 m) m)

(define-values (dom𝒮 cod𝒮 ∘𝒮 ?𝒮 =𝒮) (𝐒𝐞𝐭))

(: ℛ 𝐂𝐚𝐭)

(: domℛ (∀ ([a : ℛ] [b : ℛ]) (→ (→ℛ a b) a)))

(: codℛ (∀ ([a : ℛ] [b : ℛ]) (→ (→ℛ a b) b)))

(: ∘ℛ (∀ ([a : ℛ] [b : ℛ] [c : ℛ] ... [z : ℛ]) (→ (× (→ℛ a b) (→ℛ b c) ...) (→ℛ a z))))

(: ?ℛ (pred (∀ ([a : ℛ] [b : ℛ]) (→ℛ a b))))

(: =ℛ (∀ ([a : ℛ] [b : ℛ] [c : ℛ] [d : ℛ] ...) (→ (× (→ℛ a b) (→ℛ c d) ...) Boolean)))

(define (ℛ m) m)

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

;; Functors from 𝒮 to ℛ

(: F (∀ ([a : 𝒮] [b : 𝒮]) (→ (→𝒮 a b) (→ℛ (F a) (F b)))))

(define F

(let ()

(define (F.map m) (for/set ([(x y) (in-hash m)]) (cons x y)))

(λ (f)

(define a (dom𝒮 f))

(define b (cod𝒮 f))

(define a.map (function-map a))

(define b.map (function-map b))

(define f.map (function-map f))

(define Fa (relation (lazy Fa) (lazy Fa) (F.map a.map)))

(define Fb (relation (lazy Fb) (lazy Fb) (F.map b.map)))

(define Ff (relation (lazy Fa) (lazy Fb) (F.map f.map)))

Ff)))

(module+ test

(require "check.rkt")

;; Objects in 𝒮

(: a 𝒮) (define a (function (lazy a) (lazy a) #hash([x0 . x0] [x1 . x1])))

(: b 𝒮) (define b (function (lazy b) (lazy b) #hash([y0 . y0] [y1 . y1])))

(: c 𝒮) (define c (function (lazy c) (lazy c) #hash([z0 . z0] [z1 . z1])))

;; Morphisms in 𝒮

(: f (→𝒮 a b)) (define f (function (lazy a) (lazy b) #hash([x0 . y0] [x1 . y0])))

(: g (→𝒮 b c)) (define g (function (lazy b) (lazy c) #hash([y0 . z0] [y1 . z0])))

(define check-𝐒𝐞𝐭→𝐑𝐞𝐥 (check-ftr 𝐒𝐞𝐭 𝐑𝐞𝐥))

(define check-F (check-𝐒𝐞𝐭→𝐑𝐞𝐥 F))

(check-F a b c f g))

See more in nLab.

The functors discussed in this tutorial default to the covariant functors. A contravariant functor from 𝒞 to 𝒟 can be considered as a covariant functor from 𝒞op to 𝒟. For example, matrix-transpose is a classical example of a contravariant functor:

"code/functor/transpose.rkt"

#lang typed/racket/base/no-check

(require "../category/Matr.rkt"

"../category/dual.rkt"

math/matrix)

(: T (∀ ([b : ℳ] [a : ℳ]) (→ (→ℳ a b) (→ℳ (T b) (T a)))))

(define T matrix-transpose)

(module+ test

(require "check.rkt")

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

(define ∘ compose)

;; Objects

(: a ℳ) (define a (identity-matrix 1))

(: b ℳ) (define b (identity-matrix 2))

(: c ℳ) (define c (identity-matrix 3))

(: d ℳ) (define d (identity-matrix 4))

;; Morphisms

(: f (→ℳ a b)) (define f (build-matrix 2 1 rand))

(: g (→ℳ b c)) (define g (build-matrix 3 2 rand))

(: h (→ℳ c d)) (define h (build-matrix 4 3 rand))

(define check-†𝐌𝐚𝐭𝐫→𝐌𝐚𝐭𝐫 (check-ftr (∘ † 𝐌𝐚𝐭𝐫) 𝐌𝐚𝐭𝐫))

(define check-T (check-†𝐌𝐚𝐭𝐫→𝐌𝐚𝐭𝐫 T))

(check-T c b a g f))

A functor F : 𝒞 → 𝒟 preserves a property P of morphisms in 𝒞 if whenever f has P, so does F(f). Conversely, a functor reflects a property P of morphisms in 𝒟 if whenever F(f) has P, so does f.

F may have additional properties:

• Faithful: for every pair of objects a and b in 𝒞, the induced mapping from Hom𝒞(a, b) to Hom𝒟(F(a), F(b)) is injective.

  

• Full: for every pair of objects a and b in 𝒞, the induced mapping from Hom𝒞(a, b) to Hom𝒟(F(a), F(b)) is surjective.

  

• Fully Faithful: for every pair of objects a and b in 𝒞, the induced mapping from Hom𝒞(a, b) to Hom𝒟(F(a), F(b)) is bijective.

  

If a functor is fully faithful, and injective on objects, it is called an embedding.

Exercise: Prove that every faithful functor reflects monomorphisms.

Exercise: Prove that every faithful functor reflects epimorphisms.

Exercise: Let F : 𝒞 → 𝒟 be fully faithful. Prove that if F(a) = F(b), then a ≅ b and Hom𝒞(a, a) ≅ Hom𝒞(a, b) ≅ Hom𝒞(b, a) ≅ Hom𝒞(b, b).

2.1.1 Category of Categories🔗ℹ

Since functors are defined as a kind of function, it is natural to define the composition of functors in the same way as the composition of functions: G∘F(f) = G(F(f)). This allows us to treat functors as morphisms, leading to the construction of the category of categories, denoted as 𝐂𝐚𝐭, which forms a higher-level structure.

Exercise: Prove that the composition of functors is associative.

In practical implementations using Racket, we’ll employ 𝐏𝐫𝐨𝐜 to symbolize 𝐂𝐚𝐭. This is because, in Racket, we implement functors as procedures. Note that since the task of comparing procedure functionality can only be done by the programmer, we’ll avoid using = or just use it as pseudocode.

Although we have given specific Category Examples, these examples are just one way to implement the corresponding concepts. We can define these concepts in other ways as well. These different implementations of the same concept can be seen as equivalent objects in 𝐂𝐚𝐭.

Therefore, in the following sections, when we discuss specific categories, their definitions might differ from the Racket code in the previous sections. For instance, in the Category of Sets, morphisms of 𝐒𝐞𝐭 are defined as hash tables, but essentially they are mappings and might be defined as procedures in later sections.

2.1.1.1 Isomorphism of Categories🔗ℹ

In 𝐒𝐞𝐭, an isomorphism is a function that establishes a one-to-one correspondence between elements of two sets. Similarly, in 𝐂𝐚𝐭, an isomorphism is a functor that establishes a one-to-one correspondence between objects and morphisms in two categories, i.e., an embedding that is surjective on objects.

An endofunctor is an endomorphism in 𝐂𝐚𝐭, while an autofunctor is an automorphism in 𝐂𝐚𝐭.

Exercise: Prove that every invertible functor is an embedding.

In 𝐂𝐚𝐭, a terminal object 1 is a discrete category with exactly one object, and the initial object 0 is the category with no objects and no morphisms.

Exercise: Prove 𝒞 ≅ 1×𝒞 ≅ 𝒞×1 ≅ 0+𝒞 ≅ 𝒞+0.

Exercise: Prove 0 ≅ 0×𝒞 ≅ 𝒞×0.

Exercise: Prove that if there is a functor from 𝒞 to 0, then 𝒞 = 0.

Exercise: For objects 𝒞 and 𝒟 in 𝐂𝐚𝐭. Prove 𝒞×𝒟 ≅ 𝒟×𝒞 and 𝒞+𝒟 ≅ 𝒟+𝒞.

Exercise: For objects 𝒜, ℬ, and 𝒞 in 𝐂𝐚𝐭. Prove the distributive laws: 𝒜×(ℬ+𝒞) ≅ 𝒜×ℬ+𝒜×𝒞 and (𝒜+ℬ)×𝒞 ≅ 𝒜×𝒞+ℬ×𝒞.

Exercise: Show that both 𝒞 and 𝒟 are isomorphic to some quotient categories of 𝒞×𝒟 and some subcategories of 𝒞+𝒟.

2.1.2 Constant Functor🔗ℹ

A constant functor Δd : 𝒞 → 𝒟 is a functor that sends each object in 𝒞 to a fixed object d in 𝒟 and each morphism in 𝒞 to idd in 𝒟.

2.1.3 Opposite Functor🔗ℹ

For a functor F : 𝒞 → 𝒟, there is an opposite functor Fop : 𝒞op → 𝒟op such that Fop0 = F0 and Fop1 = F1.

2.1.4 Essentially Injective Functor🔗ℹ

A functor F : 𝒞 → 𝒟 is essentially injective if it is injective on objects up to isomorphism: ∀a, b ∈ 𝒞0, F(a) ≅ F(b) ⇒ a ≅ b.

Exercise: Prove that a functor is essentially injective iff it is injective on isomorphism classes.

2.1.5 Essentially Surjective Functor🔗ℹ

A functor F : 𝒞 → 𝒟 is essentially surjective if it is surjective on objects up to isomorphism: ∀d ∈ 𝒟0, ∃c ∈ 𝒞0, F(c) ≅ d.

2.1.6 Inclusion Functor🔗ℹ

The inclusion functor I : 𝒟 → 𝒞 is a functor that sends each object and each morphism in 𝒟 to 𝒞.

Exercise: Prove 𝒟 ⊆ 𝒞.

Exercise: Prove that if I is essentially surjective, then 𝒟 is a representative subcategory of 𝒞.

Exercise: Prove that every inclusion functor is a faithful functor.

Exercise: Prove that every inclusion functor from a full subcategory is fully faithful.

2.1.7 Projection Functor🔗ℹ

The projection functor (quotient functor) P : 𝒞 → 𝒞/∼ is a functor that ∀a ∈ 𝒞0, P(a) = [a] and ∀f ∈ 𝒞1, P(f) = [f].

Exercise: For a functor F : 𝒞 → 𝒟 and a congruence relation ∼ that ∀f, g ∈ 𝒞1, f ∼ g ⇒ F(f) = F(g). Prove that there is a unique functor F′ : 𝒞/∼ → 𝒟 for which F′∘P = F.

2.1.8 Forgetful Functor🔗ℹ

A forgetful functor (underlying functor or stripping functor) is a type of functor that forgets some or all of the structure of the objects and the structure-preserving functions in its domain category.

For example, if we forget morphisms in a category, then we get a set. Extending this idea, we get a forgetful functor U : 𝐂𝐚𝐭 → 𝐒𝐞𝐭, which forgets 𝒞1 and F1, but preserves 𝒞0 and F0: U0(𝒞) = 𝒞0 and U1(F) = F0.

Exercise: Try to define a forgetful functor from 𝐌𝐨𝐧 to 𝐒𝐞𝐭∗.

Exercise: Try to define a forgetful functor from 𝐒𝐞𝐭∗ to 𝐒𝐞𝐭.

2.1.9 Free Monoid Functor🔗ℹ

The Kleene star (Kleene closure) A* of a set A is the set of all possible finite-length sequences of elements of A. The free monoid on A is defined as the tuple (A*, ∘, ()), where () is the empty sequence, and ∘ is the operation that concatenates two sequences.

The free monoid functor F : 𝐒𝐞𝐭 → 𝐌𝐨𝐧 maps any set to its corresponding free monoid. All free monoids obtained through F share the same ∘ and (), so we commonly use Kleene stars to represent them.

In Racket, we can represent the Kleene star as a list:

(define-type A* (Listof A))

Here, ∘ and () can be represented by append and null, respectively. Below is an example of defining the free monoid functor F in Racket:

(: F (∀ (A B) (→ (→ A B) (→ A* B*))))

(define F (curry map))

2.1.10 Free Category Functor🔗ℹ

For each node a, there is a unique path of length 0, called the empty path at a.

The free category (path category) of a digraph 𝒢 is a category in which objects are the nodes of 𝒢, and morphisms are paths — that is, sequences of arrows in 𝒢, each connecting one node to the next in sequence.

In any category, we can derive an underlying digraph by abstracting away the composition and identity morphisms, focusing only on the nodes and the direct arrows that connect them. This transformation can be formally captured by a forgetful functor from 𝐂𝐚𝐭 to 𝐃𝐠𝐫, which forgets the category structure and retains only the basic digraph structure.

Exercise: Try to define the procedure make-path, which takes a digraph, a source node, and a Kleene star of arrow names, and returns the corresponding path.

The free category functor F : 𝐃𝐠𝐫 → 𝐂𝐚𝐭 maps each digraph to its corresponding free category.

Exercise: Try to implement F0 that constructs the free category for a given digraph 𝒢.

Since 𝐌𝐨𝐧 can be viewed as 𝐎𝐨𝐜, any set can also be viewed as a digraph with a single node. In this view, each element of the set corresponds to an arrow within this single node digraph. This analogy follows from the fact that we can derive the underlying set of a monoid through a forgetful functor, just as we can derive an underlying digraph from an OOC.

2.1.10.1 Category of Trees🔗ℹ

A rooted tree is a digraph in which the corresponding free category contains an initial object or terminal object, referred to as the root.

Exercise: Prove that a tree is has a unique root.

Trees are often used to represent hierarchical structures, where each node has exactly one incoming or outgoing path (except for the root, which only has an empty path).

The category of trees, denoted by 𝐓𝐫𝐞𝐞, has trees as objects and tree homomorphisms as morphisms

2.1.10.2 Category of Forests🔗ℹ

A rooted forest is a disjoint union of rooted trees.

The category of forests, denoted by 𝐅𝐬𝐭, has forests as objects and forest homomorphisms as morphisms.

Exercise: Prove that ℕ is a terminal object in 𝐅𝐬𝐭.

2.1.11 Composition Functor🔗ℹ

For morphism f : a → b : 𝒞 and g : b → c : 𝒞, there are two kinds of composition functors: f/𝒞 : b/𝒞 → a/𝒞 and 𝒞/g : 𝒞/b → 𝒞/c. f/𝒞 maps an object g in b/𝒞 to the object g∘f in a/𝒞, and 𝒞/g maps an object f in 𝒞/b to the object g∘f in 𝒞/c.

Exercise: Implement a composition functor f/ℳ : b/ℳ → a/ℳ, where ℳ is 𝐌𝐚𝐭𝐫 and f : a → b is a morphism in ℳ.

Exercise: Implement a composition functor ℳ/g : ℳ/b → ℳ/c, where ℳ is 𝐌𝐚𝐭𝐫 and g : b → c is a morphism in ℳ.

2.1.12 (Co)Slice Functor🔗ℹ

For a category 𝒞, the slice functor 𝒞/- maps each morphism g : b → c : 𝒞 to the composition functor 𝒞/g : 𝒞/b → 𝒞/c.

(: 𝒞 𝐂𝐚𝐭)

(: 𝒞/- (∀ ([b : 𝒞] [c : 𝒞]) (→ (→𝒞 b c) (→𝐂𝐚𝐭 𝒞/b 𝒞/c))))

(define (𝒞/- g)

(: 𝒞/g (∀ ([x : 𝒞/b] [y : 𝒞/b]) (→ (→𝒞/b x y) (→𝒞/c (∘𝒞 g x) (∘𝒞 g y)))))

(define 𝒞/g

(match-λ

[`((,x) (,y ,z))

`((,(∘𝒞 g x)) (,(∘𝒞 g y) ,z))]))

𝒞/g)

Exercise: Prove 𝒞/g∘f = 𝒞/g∘𝒞/f.

For a category 𝒞, the coslice functor -/𝒞 maps each morphism f : a → b : 𝒞 to the composition functor f/𝒞 : b/𝒞 → a/𝒞.

(: 𝒞 𝐂𝐚𝐭)

(: -/𝒞 (∀ ([b : 𝒞] [a : 𝒞]) (→ (→𝒞 a b) (→𝐂𝐚𝐭 b/𝒞 a/𝒞))))

(define (-/𝒞 f)

(: f/𝒞 (∀ ([x : b/𝒞] [y : b/𝒞]) (→ (→b/𝒞 x y) (→a/𝒞 (∘𝒞 x f) (∘𝒞 y f)))))

(define f/𝒞

(match-λ

[`((,z ,x) (,y))

`((,z ,(∘𝒞 x f)) (,(∘𝒞 y f)))]))

f/𝒞)

Exercise: Prove g∘f/𝒞 = f/𝒞∘g/𝒞.

2.2 Diagram🔗ℹ

In Commutative Diagram, we introduced the informal idea of a diagram as a collection of objects connected by morphisms, where a commutative diagram ensures that all paths between the same pair of objects result in the same morphism. Now, we formalize this concept.

Let 𝒞 be a category, and let 𝒮 be a small category. A diagram D of shape 𝒮 in 𝒞 is a functor D : 𝒮 → 𝒞. If 𝒮 is a thin category, then the diagram commutes, i.e., it is commutative.

Exercise: Prove that every functor preserves commutative diagrams.

Exercise: Prove that every faithful functor reflects commutative diagrams.

Let 𝒮 be a digraph. A free diagram D is a diagram of shape F(𝒮), where F(𝒮) is the free category of 𝒮. Equivalently, D can be viewed as a graph homomorphism from 𝒮 to U(𝒞), where U(𝒞) is the underlying digraph of 𝒞.

2.3 𝐒𝐞𝐭-Valued Functor🔗ℹ

A 𝐒𝐞𝐭-valued functor on 𝒞 is a functor from 𝒞 to 𝐒𝐞𝐭. Such functors map objects in 𝒞 to sets, and morphisms in 𝒞 to functions between these sets. These functors are central to many areas of category theory.

More generally, given any category 𝒟, a 𝒟-valued presheaf on 𝒞 is a functor from 𝒞op to 𝒟.

One important type of 𝐒𝐞𝐭-valued functor is the presheaf, which is a functor from 𝒞op to 𝐒𝐞𝐭. The name presheaf comes from topology, but the concept applies to arbitrary categories.

𝐒𝐞𝐭-valued functors, including presheaves, have theoretical importance due to the Yoneda Lemma, a fundamental result in category theory that will be introduced in detail in the next chapter.

A related concept is that of a concrete category, which is a category equipped with a faithful 𝐒𝐞𝐭-valued functor. A category is called concretizable iff it admits such a functor.

2.3.1 Category of Elements of a Functor🔗ℹ

Given a functor F : 𝒞 → 𝐒𝐞𝐭, the category of elements of F, denoted by ∫S:𝒞F(S) or ∫𝒞F, is a category where each object represents an element s drawn from some F(S). Each such object can be viewed as a pointed set (F(S), s).

This construction allows us to study the internal structure of a 𝐒𝐞𝐭-valued functor by examining its individual elements and the relationships between them. One useful example of this is viewing a rooted forest as a presheaf on ℕ.

A rooted forest can be interpreted as a presheaf F : ℕop → 𝐒𝐞𝐭, where each set F(n) represents a layer of nodes in the forest. Specifically, F(n) consists of all nodes in the forest such that the length of the path from each node to the root is exactly n.

A rooted tree is a special case of a forest for which F(0) is a singleton set.

The following diagram shows how we can interpret ∫ℕopF as the free category of a forest:

Moreover, a planar forest can be viewed as a functor F : ℕop → 𝐓𝐨𝐬, where each layer is a toset.

2.3.2 Powerset Functor🔗ℹ

The powerset of a set s, denoted by 𝒫(s), is the set of all subsets of s. This concept is central to several powerset functors, which map sets to their corresponding powersets.

"code/function/P.rkt"

#lang typed/racket/base/no-check

(require racket/hash racket/set racket/promise)

(require "../category/Set.rkt")

(provide (all-defined-out))

(: 𝒮 𝐂𝐚𝐭)

(: dom𝒮 (∀ ([a : 𝒮] [b : 𝒮]) (→ (→𝒮 a b) a)))

(: cod𝒮 (∀ ([a : 𝒮] [b : 𝒮]) (→ (→𝒮 a b) b)))

(: ∘𝒮 (∀ ([a : 𝒮] [b : 𝒮] [c : 𝒮] ... [z : 𝒮]) (→ (× (→𝒮 a b) (→𝒮 b c) ...) (→𝒮 a z))))

(: ?𝒮 (pred (∀ ([a : 𝒮] [b : 𝒮]) (→𝒮 a b))))

(: =𝒮 (∀ ([a : 𝒮] [b : 𝒮] [c : 𝒮] [d : 𝒮] ...) (→ (× (→𝒮 a b) (→𝒮 c d) ...) Boolean)))

(define (𝒮 m) m)

(define-values (dom𝒮 cod𝒮 ∘𝒮 ?𝒮 =𝒮) (𝐒𝐞𝐭))

(: combine/key (→ Any Any Any Any))

(define (combine/key k v1 v2) v1)

(define 𝒫

(let ()

(define (𝒫.map s.map)

(for/fold ([𝒫s.map (hash s.map s.map #hash() #hash())])

([(v _) (in-hash s.map)])

(define s0.map (hash-remove s.map v))

(define 𝒫s0.map (𝒫.map s0.map))

(hash-union 𝒫s.map 𝒫s0.map #:combine/key combine/key)))

(λ (s)

(define 𝒫s.map (𝒫.map (function-map s)))

(define 𝒫s (function (lazy 𝒫s) (lazy 𝒫s) 𝒫s.map))

𝒫s)))

Given a function f : a → b, where a0 is a subset of a and b0 is a subset of b, we can define several powerset functors that map a set s to 𝒫(s).

2.3.2.1 Direct Image Functor🔗ℹ

The direct image (existential image) of a0, denoted by f∗(a0), is the subset of b: f∗(a0) ≔ {f(x) | x ∈ a0}.

The direct image functor (existential image functor) 𝒫∗ takes f to f∗: 𝒫∗(f) = f∗.

"code/functor/P_*.rkt"

#lang typed/racket/base/no-check

(require racket/hash racket/set racket/promise)

(require "../category/Set.rkt"

"../function/P.rkt")

(: 𝒫_∗ (∀ ([a : 𝒮] [b : 𝒮]) (→ (→𝒮 a b) (→𝒮 (𝒫 a) (𝒫 b)))))

(provide 𝒫_∗)

(define (𝒫_∗ f)

(define f.map (function-map f))

(define a (dom𝒮 f))

(define b (cod𝒮 f))

(define 𝒫a (𝒫 a))

(define 𝒫b (𝒫 b))

(define f_∗.map

(for/hash ([(a0.map _) (in-hash (function-map 𝒫a))])

(define b0.map

(for/fold ([b0.map #hash()])

([(x _) (in-hash a0.map)])

(define y (hash-ref f.map x))

(hash-set b0.map y y)))

(values a0.map b0.map)))

(define f_∗ (function (lazy 𝒫a) (lazy 𝒫b) f_∗.map))

f_∗)

(module+ test

(require "check.rkt")

;; Objects

(: a 𝒮) (define a (function (lazy a) (lazy a) #hash([x0 . x0] [x1 . x1])))

(: b 𝒮) (define b (function (lazy b) (lazy b) #hash([y0 . y0] [y1 . y1])))

(: c 𝒮) (define c (function (lazy c) (lazy c) #hash([z0 . z0] [z1 . z1])))

;; Morphisms

(: f (→𝒮 a b)) (define f (function (lazy a) (lazy b) #hash([x0 . y0] [x1 . y0])))

(: g (→𝒮 b c)) (define g (function (lazy b) (lazy c) #hash([y0 . z0] [y1 . z0])))

(define check-𝐒𝐞𝐭→𝐒𝐞𝐭 (check-ftr 𝐒𝐞𝐭 𝐒𝐞𝐭))

(define check-𝒫_∗ (check-𝐒𝐞𝐭→𝐒𝐞𝐭 𝒫_∗))

(check-𝒫_∗ a b c f g))