Graphs are to categories as lists are to monoids
—the HTML is quite messy and no attempt at all has been made to clean it up; the previous link also directs to a PDF version of this article. Moreover, this article has just been put on pause. My interest has now shifted to the science of programming and so I am now writing articles on that. In retrospect, this article is quite long and more of a pamphlet than a blog post! I would do well to avoid this approach in future posts.
Assuming familiarity with the Agda programming language, we motivate the need for basic concepts of category theory with the aim of discussing adjunctions with a running example of a detailed construction and proof of a free functor.
Introduction
Lists give free monoids 𝓁 A = (List A, ++, []) — a monoid 𝒮 = (S, ⊕, 0₊) is a triple consisting of a set with a binary operation on it that is associative and has a unit; see a previous post for a more formal definition. That it is ‘free’ means that to define a structure-preserving map between monoids (List A, ++, []) ⟶ (S, ⊕, 0₊) it suffices to only provide a map between their carriers List A → S —freedom means that plain old maps between types freely, at no cost or effort, give rise to maps that preserve monoid structure. Moreover, the converse also holds and in-fact we have a bijection
(𝓁 A ⟶ 𝒮) ≅ (A ⟶ 𝒰 𝒮)where we write 𝒰 (S, ⊕, 0₊) = S for the operation that gives us the 𝒰nderlying carrier of a monoid.
Loosely put, one says we have an ‘adjunction’, written 𝓁 ⊣ 𝒰.
Observe that natural numbers ℕ ≅ List Unit are a monoid whose operation is commutative, by using different kinds of elements A (and, importantly, still not imposing any equations), we lose commutativity with List A. Then by generalizing further to binary trees BinTree A, we lose associtivity and identity are are only left with a set and an operation on it —a structure called a ‘magma’.
This is the order that one usually learns about these inductively built structures. One might be curious as to what the next step up is in this hierarchy of generalisations. It is a non-inductive type called a ‘graph’ and in this note we investigate them by comparison to lists. Just as we shifted structures in the hierarchy, we will move to a setting called a ‘category’ —such are more structured than magmas but less restrictive than monoids.
Since the Agda prelude is so simple, the core language doesn’t even come with booleans or numbers by default —they must be imported from the standard library. This is a pleasant feature. As a result, Agda code tends to begin with a host of imports.
module PathCat where
open import Level using (Level) renaming (zero to ℓ₀ ; suc to ℓsuc ; _⊔_ to _⊍_)
-- numbers
open import Data.Fin
using (Fin ; toℕ ; fromℕ ; fromℕ≤ ; reduce≥ ; inject≤)
renaming (_<_ to _f<_ ; zero to fzero ; suc to fsuc)
open import Data.Nat hiding (fold)
open import Relation.Binary using (module DecTotalOrder)
open DecTotalOrder Data.Nat.decTotalOrder using () renaming (refl to ≤-refl)
-- Z-notation for sums
open import Data.Product using (Σ ; proj₁ ; proj₂ ; _×_ ; _,_)
Σ∶• : {a b : Level} (A : Set a) (B : A → Set b) → Set (a ⊍ b)
Σ∶• = Σ
infix -666 Σ∶•
syntax Σ∶• A (λ x → B) = Σ x ∶ A • B
-- equalities
open import Relation.Binary.PropositionalEquality using (_≗_ ; _≡_)
renaming(sym to ≡-sym ; refl to ≡-refl ; trans to _⟨≡≡⟩_ ; cong to ≡-cong ; cong₂ to ≡-cong₂
; subst to ≡-subst ; subst₂ to ≡-subst₂ ; setoid to ≡-setoid)Notice that we renamed transitivity to be an infix combinator.
Let us make equational-style proofs available for any type. This is similar to what was discussed in a previous post but much better.
module _ {i} {S : Set i} where
open import Relation.Binary.EqReasoning (≡-setoid S) public
-- synonym for readability
definition : ∀{a} {A : Set a} {x : A} → x ≡ x
definition = ≡-reflGraph definitions
A ‘graph’ is just a parallel-pair of maps,
record Graph₀ : Set₁ where
field
V : Set
E : Set
src : E → V
tgt : E → VThis of-course captures the usual notion of a set of nodes V and a set of directed and labelled edges E where an edge e begins at src e and concludes at tgt e.
What is good about this definition is that it can be phrased in any category: V and E are any two objects and src, tgt are a parallel pair of morphisms between them. How wonderful! We can study notion of graphs in arbitrary categories! —this idea will be made clearer when categories and functors are formally introduced.
However, the notion of structure-preserving map between graphs, or ‘graph-map’ for short, then becomes
record _𝒢⟶₀_ (G H : Graph₀) : Set₁ where
open Graph₀
field
vertex : V(G) → V(H)
edge : E(G) → E(H)
src-preservation : ∀ e → src(H) (edge e) ≡ vertex (src(G) e)
tgt-preservation : ∀ e → tgt(H) (edge e) ≡ vertex (tgt(G) e)This is a bit problematic in that we have two proof obligations and at a first glance it is not at all clear their motivation besides ‘’structure-preserving’’.
However, our main is in graphs in usual type theory, and as such we can use a definition that is equivalent in this domain: a graph is a type V of vertices and a ‘type’ v ⟶ v' of edges for each pair of vertices v , v'.
-- 'small graphs' , since we are not using levels
record Graph : Set₁ where
field
V : Set
_⟶_ : V → V → SetNow the notion of graph-map, and the meaning of structure-preserving, come to the forefront:
record GraphMap (G H : Graph) : Set₁ where
private
open Graph using (V)
_⟶g_ = Graph._⟶_ G
_⟶h_ = Graph._⟶_ H
field
ver : V(G) → V(H) -- vertex morphism
edge : {x y : V(G)} → (x ⟶g y) → (ver x ⟶h ver y) -- arrow preservation
open GraphMapNote that edge essentially says that mor shifts, or translates, types x ⟶g y into types ver x ⟶h ver y.
While equivalent, this two-piece definition is preferable over the four-piece one given earlier since it means less proof-obligation and less constructions in general, but the same expressiblity. Yay!
Before move on, let us give an example of a simple chain-graph. For clarity, we present it in both variations.
-- embedding, `j < n ⇒ j < suc n`
'_ : ∀{n} → Fin n → Fin (suc n)
' j = inject≤ j (≤-step ≤-refl) where open import Data.Nat.Properties using (≤-step)
-- this' an example of a 'forgetful functor', keep reading!
[_]₀ : ℕ → Graph₀
[ n ]₀ = record { V = Fin (suc n) -- `≈ {0, 1, ..., n - 1, n}`
; E = Fin n -- `≈ {0, 1, ..., n - 1}`
; src = λ j → ' j
; tgt = λ j → fsuc j
}That is, we have (n+1) vertices named 0, 1, …, n and n-edges named 0, 1, …, n-1 with one typing-axiom being j : j ⟶ (j+1). Alternatively,
[_] : ℕ → Graph
[ n ] = record {V = Fin (suc n) ; _⟶_ = λ x y → fsuc x ≡ ' y }Signatures
A signature consists of sort symbols and function symbols each of which is associated source-sorts and a target-sort. A model or algebra of a language is an interpreation of the sort symbols as sets and function symbols as functions between those sets —later you may note that instead of sets and functions we may use the objects and morphisms of a fixed category instead, and so get a model in that category.
Formally, one sorted signatures are defined:
open import Data.Vec using (Vec) renaming (_∷_ to _,,_ ; [] to nil) -- , already in use for products :/
-- one sorted
record Signature : Set where
field
𝒩 : ℕ -- how many there are
ar : Vec ℕ 𝒩 -- their arities: lookup i ar == arity of i-th function symbol
open Signature {{...}} -- `𝒩` now refers to the number of function symbols in a signatureFor example, the signature of monoids consists of a single sort symbol C (which can be interpretted as the carrier of the monoid) and two function symbols m , u (which can be interpreted as the monoid multiplication and unit) with source-target sort lists ((),C) , ((C,C), C) —some would notate this by u :→ C , m : C × C → C.
MonSig : Signature
MonSig = record { 𝒩 = 2 ; ar = 0 ,, 2 ,, nil }
-- unit `u : X⁰ → X` and multiplication `m : X² → X`Generalising on monoids by typing the multiplication we obtain the signature of categories: it consists of three sort symbols O, A, C (which can be interepreted as objects, arrows, and composable pairs of arrows) and four function symbols ⨾ , src, tgt, id with source-target sort lists (C,A) , (A,O) , (A,O) , (O,A) —notice that only a language of symboll has been declared without any properties besides those of typing. If we discard C, ⨾, id we then obtain the signature of graphs. Without knowing what categories are, we have seen that their signatures are similar to both the graph and monoid signatures and so expect their logicas to also be similar.
A signature can be visualised in the plane by associting a dot for each sort symbol and an arrow for each function symbols such that the arrow has a tail from each sort in the associated function symbols source sorts list and the end of the arrow is the target sort of the sort symbol. That is, a signature can be visualed as a hyper-graph.
A signature whose function symbols each have only one sort symbol for source-sorts is called a ‘graph signature’ since it corresponds to —or can be visualised as— a graph.
Then a model of a graph (signature) 𝒢 is an interpreation/realisation of the graph’s vertices as sets and the graph’s edges as functions between said sets.
A model of 𝒢 is nothing more than a graph morphism 𝒢 ⟶ 𝒮e𝓉𝒢𝓇𝒶𝓅𝒽, where 𝒮e𝓉𝒢𝓇𝒶𝓅𝒽 is the graph with vertices sets and edges functions.
Notice that a graph is precicely a model of the graph • ⇉ • of two vertices and two edges from the first to the second.
In this section we introduce the notion of a ‘’poor-man’s category’’ along with the notion of structure preserving transformations and structure preserving transformations between such the most important pieces of the fundamentals of category theory; as such, we discuss them at length. Afterwards, we relate this section back to our motivating discussion of graphs.
Strict Categories
A category, like a monoid, is a a few types and operations for which some equations hold. However, to discuss equations a notion of equality is needed and rather than enforce one outright it is best to let it be given. This is a ‘set’ in constructive mathematics: a type with an Equivalence relation on it —also called a setoid or an E-set. However, then the structure must have a few added axioms: the operations must be congruences, i.e., preserve the equivalence relation, and a structure-preserving map must also be a congruence.
For our purposes our we will use propositional equality and point-wise propositional equality, and as such most of the proofs fall out of the fact that propositional equality is an equivalence. However, this setoid structure becomes a bit of a noise and the issues of equivalences will be a distraction from the prime focus. Instead, for our two cases where we use point-wise propositional, we will postulate two forms of extensionality. Without question this is not a general approach —then again, our aim is not to develope a library for category theory, which has already been done so elegantly by Kahl who calls it the RATH-Agda project.
module _ where -- category definitions
record Category {i j : Level} : Set (ℓsuc (i ⊍ j)) where
infixr 10 _⨾_
field
Obj : Set i
_⟶_ : Obj → Obj → Set j
_⨾_ : ∀{A B C : Obj} → A ⟶ B → B ⟶ C → A ⟶ C
assoc : ∀{A B C D} {f : A ⟶ B}{g : B ⟶ C} {h : C ⟶ D} → (f ⨾ g) ⨾ h ≡ f ⨾ (g ⨾ h)
Id : ∀{A : Obj} → A ⟶ A
leftId : ∀ {A B} {f : A ⟶ B} → Id ⨾ f ≡ f
rightId : ∀ {A B} {f : A ⟶ B} → f ⨾ Id ≡ f
open Category using (Obj) public
open Category {{...}} hiding (Obj) -- don't want this to be public, since --> also notates edgesHowever, similar to nearly everything else in this document, we can leave the setoid-approach as an excercise for the reader, which of course has solutions being in the literate source.
Moreover, lest you’re not convinced that my usage of extensionality is at all acceptable, then note that others have used it to simplify their presentations; e.g., Relative monads formalised. Such ‘appeal to authority’ is for the lazy reader who dares not think for him or herself, otherwise one ought to read up on the evils of using equality instead of equivalence relations so as to understand when one thing is really another.
The diligent reader may be interest to know that Maarten Fokkinga has written a very theory using the calculational approach}; I highly recommend it!
In place of strict equality, one uses categorical isomorphism instead.
record Iso {i} {j} (𝒞 : Category {i} {j}) (A B : Obj 𝒞) : Set j where
field
to : A ⟶ B
from : B ⟶ A
lid : to ⨾ from ≡ Id
rid : from ⨾ to ≡ Id
syntax Iso 𝒞 A B = A ≅ B within 𝒞Let us give some elementary examples of the notion of a category to exhibit its ubiquity.
The collection of small (level 0) types and functions between them and usual function composition with usual identity form a category and this is not at all difficult to see:
instance
𝒮e𝓉 : ∀ {i} → Category {ℓsuc i} {i} -- this is a 'big' category
𝒮e𝓉 {i} = record {
Obj = Set i
; _⟶_ = λ A B → (A → B)
; _⨾_ = λ f g → (λ x → g (f x))
; assoc = ≡-refl
; Id = λ x → x
; leftId = ≡-refl
; rightId = ≡-refl
}Sadly, this category is traditionally used to motivate constructions in arbitrary categories and as such people usually thing of objects in an arbitrary category as nothing more than sets with extra datum —which is completely false.
Recall that a type, or set, is nothing more than a specified collection of values.
Every set is also a category: there is an object for each element, the only morphisms are (formal) identities, and composition is constantly the identity. Some define a set to be a category with only identity morphisms; also called a ‘discrete category’ when one wants to distance themself from set theory ;) —less loosely, a discrete category over a type S has Obj = S and (x ⟶ y) = (x ≡ y).
Discrete categories are quite an important space for hott people … that’s right, attractive people are interested in these things.
Observe that all arrows are invertible! —due to the symmetry of equality.
Recall that a monoid (M, ⊕, e) is a type M with an associative operation ⊕ : M × M → M that has a unit e.
Every monoid is also a category: there is one object, call it ★, the morphisms are the monoid elements, and composition is the monoid operation. Some even define a monoid to be a one object category. —less loosely, for a monoid (M, ⊕, e) we take Obj = {★} , _⟶_ = M.
In fact, some would define a monoid to be a one-object category!
Recall that a preordered set, or preset, is a type P with a relation ≤ on it that satisfies ‘’indirect inequality from above’‘: ∀ x , y • x ≤ y ⇔ (∀ z • y ≤ z ⇒ x ≤ z) —equivalently, if it satisfies’‘indirect equality from below’‘: ∀ x , y • x ≤ y ⇔ (∀ z • z ≤ x ⇒ z ≤ y). If we also have ∀ x , y • x ≤ y ∧ y ≤ x ⇒ x = y, then we say (P, ≤) is a ’poset’ or an ‘ordered set’.
Every (pre)ordered set is also a category: the objects are the elements, the morphisms are the order-relations, identities are the relfexitivity of ≤, and composition is transitivity of ≤.
Traditionally, classically, the relation ≤ is precicely a function P × P ⟶ 𝔹 = {true, flase} and thus there is at-most one morphism between any two objects, and categories with this property
In the constructive setting, the relation ≤ is typed P × P → Set and then for a preset (P, ≤) we take Obj = P, _⟶_ = a ≤ b and insist on ‘proof-irrelevance’ ∀ {a b} (p q : a ≤ b) → p ≡ q so that there is at most one morphism between any two objects. The restriction is not needed if we were using actual categories-with-setoids since then we would
Observe that in the case we have a poset, every isomorphism is an equality: ∀ x, y • x ≅ y ⇔ x ≡ y Again, hott people like this; so much so, that they want it, more-or-less, to be a foundational axiom!
Poset categories are a wonderful and natural motivator for many constructions and definitions in category theory. This idea is so broad-reaching that it would not be an exaggeration to think of categories as coherently constructive lattices!
Equivalence relations are relations that are symmetric, reflexive, and transitive. Alternatively, they are preorder categories where every morphism is invertible —this is the symmetry property. But categories whose morphisms are invertible are groupoids!
Hence, groupoids can be thought of as generalized equivalence relations. Better yet, as “constructive” equivalence relations: there might be more than one morphism/construction witnessing the equivalence of two items.
Some insist that a “true set” is a type endowed with an equivalence relation, that is a setoid. However, since groupoids generalize equivalence relations, others might insist on a true set to be a “groupoid”. However, in the constructive setting of dependent-type theory, these notions coincide!
It’s been said that the aforementioned categories should be consulted whenever one learns a new concept of category theory. Indeed, these examples show that a category is a generalisation of a system of processes, a system of compositionality, and an ordered system.
Functors
Now the notion of structure-preserving maps is just that of graphs but with attention to the algebraic portions as well.
record Functor {i j k l} (𝒞 : Category {i} {j}) (𝒟 : Category {k} {l}) : Set (ℓsuc (i ⊍ j ⊍ k ⊍ l)) where
field
-- usual graph homomorphism structure
obj : Obj 𝒞 → Obj 𝒟 -- object map
mor : ∀{x y : Obj 𝒞} → x ⟶ y → obj x ⟶ obj y -- morphism preservation
-- interaction with new algebraic structure
id : ∀{x : Obj 𝒞} → mor (Id {A = x}) ≡ Id -- identities preservation
comp : ∀{x y z} {f : x ⟶ y} {g : y ⟶ z} → mor (f ⨾ g) ≡ mor f ⨾ mor g -- composition preservation
open Functor using (obj ; mor) publicFor a functor F, it is common practice to denote both obj F and mor F by F and this is usually not an issue since we can use type inference to deduce which is meant. However, in the Agda formalization we will continue to use the names mor , obj.
A functor can be thought of as endowing an object with some form of structure —since categories are intrinsically structureless in category theory— and so the morphism component of a functor can be thought of as preserving relations: f : a ⟶ b ⇒ F f : F a ⟶ F b can be read as, ‘’if a is related to b (as witnessed by f) then their structured images are also related (as witness by F f)’’.
While we’re close to the definition, let’s introduce some synonyms for readability
module _ {i j k l} {𝒞 : Category {i} {j}} {𝒟 : Category {k} {l}} {{F : Functor 𝒞 𝒟}} where
functors-preserve-composition = Functor.comp F
functors-preserve-identities = Functor.id FWe make these as synonyms rather than names in the record since we do not want to use such lengthy identifiers when realizing functor instances. The reason we do not make these synonyms in the record but rather in a public dummy module is to make the functor in question found from the ambient context (the {{...}}).
While we’re making synonyms for readability, let’s make another:
_even-under_ : ∀ {a b} {A : Set a} {B : Set b} {x y} → x ≡ y → (f : A → B) → f x ≡ f y
_even-under_ = λ eq f → ≡-cong f eqAn example usage is the proof ≡-cong (mor G) (id F) : mor G (mor F Id) ≡ mor G Id can be written more clearly as functors-preserve-identities even-under (mor G), while longer it is also self-documenting.
In informal mathematics a functor F = (obj , mor, preservation proofs) is usually presented as ‘’F = (F₀, F₁) is a functor (exercise to reader)’’.
“endo”morphism is a morphism with the same source and target, an “auto”morphism is an isomorphism with the same source and target.
Say “co”functor as short for “co”ntravariant functor. Notice that the composition of cofunctors is a covaraint functor —cf the multiplication of negative numbers is a positive functor.
A functor among monoids (as categories) is just a monoid homomorphism: (M, ⊕, e) ⟶ (N, ⊗, d) = Σ h ∶ M → N • ∀ x,y • h(x ⊕ y) = h x ⊗ h y ∧ h e = d; that is an identity and multiplication preserving function of the carriers. Ny induction, h preserves all finite multiplications: h (⊕ i ∶ 1..n • xᵢ) = (⊗ i ∶ 1..n • h xᵢ) where (★ i ∶ 1..n • yᵢ) ≔ e ★ y₁ ★ y₂ ⋯ ★ yₙ. More generally, functors preserve finite compositions: F (⨾ i ∶ 1..n • fᵢ) = (⨾ i ∶ 1..n • F fᵢ) Cool beans :-)
A functor among poset categories is an order-preserving function.
A functor among discrete categories is just a function of the associated sets.
Two examples of functors from a poset (category) to a monoid (category). monus : (ℕ, ≤) ⟶ (ℕ,+, 0) is a functor defined on morphisms by i ≤ j ⇒ monus(i,j) ≔ j - i and then the functor laws become i - i = 0 and (k - j) + (j - i) = k - i. div : (ℕ⁺, ≤) → (ℚ, ×, 1) is defined on morphisms by i ≤ j → div(i,j) ≔ j / i and the functor laws become i / i = 1 and (k / j) × (j / i) = k / i.
Hey, these two seem alarmingly similar! What gives! Well, they’re both functors from posets to monoids ;) Also, they are instances of ‘residuated po-monoids’. Non-commutative monoids may have not have a general inverse operation, but instead might have left- and right- inverse operations known as residuals —we’ll mention this word again when discussing adjunctions and kan extensions. Alternatively, they’re are instances of ‘(Kopka) Difference-posets’.
The four postulates of the apocalypse
Categories have objects and morphisms between them, functors are morphisms between categories, and then we can go up another level and consider morphisms between functors. These ‘level 2 morphisms’ are pretty cool, so let’s touch on them briefly.
Using posets as our guide, We extend the ordering to monotone functions f , g pointwise f ≤̇ g ≔ (∀ x • f x ≤ g x) and with posets as our guide, we extend the notion of morphism between functors to be a ‘witness’ of these orderings η : ∀ {X} → F X ⟶ G X. However, then for any morphism f : A ⟶ B we have two ways to get from F A to G B via F f ⨾ η {B} and η {A} ⨾ G f and rather than choose one or the other, we request that they are identical —similar to the case of associtivity.
NatTrans : ∀ {i j i' j'} {𝒞 : Category {i} {j}} {𝒟 : Category {i'} {j'}} (F G : Functor 𝒞 𝒟) → Set (j' ⊍ i ⊍ j)
NatTrans {𝒞 = 𝒞} F G =
Σ η ∶ (∀ {X : Obj 𝒞} → obj F X ⟶ obj G X) • (∀ {A B} {f : A ⟶ B} → mor F f ⨾ η {B} ≡ η {A} ⨾ mor G f)Another way to remember it: η : F ⟶̇ G starts at F and ends at G, so the naturaliry also starts with F and ends with G: F f ⨾ η {B} = η {A} ⨾ G f :-)
It is at this junction that aforemenioed problem with our definition of category comes to light: funnction equality is extensional and as such we cannot prove it. Right now we have two function-like structures for which we will postulate a form of extensionality,
-- function extensionality
postulate extensionality : ∀ {i j} {A : Set i} {B : A → Set j} {f g : (a : A) → B a}
→ (∀ {a} → f a ≡ g a) → f ≡ g
-- functor extensionality
postulate funcext : ∀ {i j k l} {𝒞 : Category {i} {j} } {𝒟 : Category {k} {l} }
{F G : Functor 𝒞 𝒟} (oeq : ∀ {o} → obj F o ≡ obj G o)
→ (∀ {X Y} {f : X ⟶ Y} → mor G f ≡ ≡-subst₂ _⟶_ oeq oeq (mor F f))
→ F ≡ G
-- graph map extensionality
postulate graphmapext : {G H : Graph } {f g : GraphMap G H} (veq : ∀ {v} → ver f v ≡ ver g v)
→ (∀ {x y} {e : Graph._⟶_ G x y} → edge g e ≡ ≡-subst₂ (Graph._⟶_ H) veq veq (edge f e))
→ f ≡ g
-- natural transformation extensionality
postulate nattransext : ∀ {i j i' j'} {𝒞 : Category {i} {j} } {𝒟 : Category {i'} {j'} } {F G : Functor 𝒞 𝒟} (η γ : NatTrans F G)
→ (∀ {X} → proj₁ η {X} ≡ proj₁ γ {X}) -- this is not enough to regain `η,γ`
→ η ≡ γNatural transformations are too cool to end discussing so briefly and so we go on to discuss their usage is mathematics later on.
A very big 𝒞𝒶𝓉
With the notions of categories, functors, and extensionality in-hand we can now discus the notion of the category of small categories and the category of small graphs. Afterwards we give another example of a functor, say how every category can be construed as a graph.
instance
𝒞𝒶𝓉 : ∀ {i j} → Category {ℓsuc (i ⊍ j)} {ℓsuc (i ⊍ j)}
𝒞𝒶𝓉 {i} {j} = record {
Obj = Category {i} {j}
; _⟶_ = Functor
; _⨾_ = λ F G → record {
obj = obj F ⨾ obj G -- this compositon lives in `𝒮e𝓉`
; mor = mor F ⨾ mor G
; id = λ {x} → begin
(mor F ⨾ mor G) (Id {A = x})
≡⟨ definition {- of function composition -} ⟩
mor G (mor F (Id {A = x}))
≡⟨ functors-preserve-identities even-under (mor G) ⟩
mor G (Id {A = obj F x})
≡⟨ functors-preserve-identities {- and function composition -} ⟩
Id {A = (obj F ⨾ obj G) x}
∎
; comp = λ {x y z f g} → begin
(mor F ⨾ mor G) (f ⨾ g)
≡⟨ definition {- of function composition -} ⟩
mor G (mor F (f ⨾ g))
≡⟨ functors-preserve-composition even-under (mor G) ⟩
mor G (mor F f ⨾ mor F g)
≡⟨ functors-preserve-composition {- and function composition -}⟩
(mor F ⨾ mor G) f ⨾ (mor F ⨾ mor G) g
∎
}
; assoc = λ {a b c d f g h} → funcext ≡-refl ≡-refl
; Id = record { obj = Id ; mor = Id ; id = ≡-refl ; comp = ≡-refl }
; leftId = funcext ≡-refl ≡-refl
; rightId = funcext ≡-refl ≡-refl }Some things to note,
We could have written id = ≡-cong (mor G) (id F) ⟨≡≡⟩ id G, but this is not terribly clear what is going on. Especially since we introduced categories not too long ago, we choose to elaborate the detail.
Likewise, comp = (≡-cong (mor G) (comp F)) ⟨≡≡⟩ (comp G).
assoc is trivial since function composition is, by definition, associative. Likewise leftId, rightId hold since functional identity is, by definition, unit of function composition.
The definition of composition immediately gives us that obj , mor distributes over composition: obj (F ⨾ G) = obj F ⨾ obj G and mor (F ⨾ G) = mor F ⨾ mor G. 𝒞𝒶𝓉 is a category of kind (ℓsuc m, ℓsuc m), where m = i ⊍ j, and its objects are categories of kind (i , j) and so it is not an object of itself. Thank-you Russel and friends! ( You may proceed to snicker at the paradoxical and size issues encountered by those who use set theory. ) —then again, I’ve never actually learned, nor even attempted to learn, any ‘’formal set theory’’; what I do know of set theory is usually couched in the language of type theory, I heart LADM!
In a nearly identical way, just ignoring the algebraic datum, we can show that Graphs with GraphMaps form a graph
𝒢𝓇𝒶𝓅𝒽 : Category
𝒢𝓇𝒶𝓅𝒽 = {! exercise !}𝒞𝒶𝓉s are 𝒢𝓇𝒶𝓅𝒽s
Let’s formalize what we meant earlier when we said graphs are categories but ignoring the algebraic data.
Given a category, we ignore the algebraic structure to obtain a graph,
𝒰₀ : Category → Graph
𝒰₀ 𝒞 = record { V = Obj 𝒞 ; _⟶_ = Category._⟶_ 𝒞 }Likewise, given a functor we ‘forget’ the property that the map of morphisms needs to preserve all finite compositions to obtain a graph map:
𝒰₁ : {𝒞 𝒟 : Category} → 𝒞 ⟶ 𝒟 → 𝒰₀ 𝒞 ⟶ 𝒰₀ 𝒟
𝒰₁ F = record { ver = obj F ; edge = mor F }This says that 𝒰₁ turns ver, edge into obj , mor, 𝒰₁ ⨾ ver ≡ obj and 𝒰₁ ⨾ edge ≡ mor, reassuring us that 𝒰₁ acts as a bridge between the graph structures: ver , edge of graphs and obj , mor of categories.
Putting this together, we obtain a functor.
-- underlying/forgetful functor: every category is a graph
𝒰 : Functor 𝒞𝒶𝓉 𝒢𝓇𝒶𝓅𝒽
𝒰 = record { obj = 𝒰₀ ; mor = 𝒰₁ ; id = ≡-refl ; comp = ≡-refl }We forget about the extra algebraic structure of a category and of a functor to arrive at a graph and graph-map, clearly such ‘forgetfullness’ preserves identities and composition since it does not affect them at all!
Those familiar with category theory may exclaim that just as I have mentioned the names ‘underlying functor’ and ‘forgetful functor’ I ought to mention ‘stripping functor’ as it is just as valid since it brings about connotations of ‘stripping away’ extra structure. I’m assuming the latter is less popular due to its usage for poor mathematical jokes and puns.
Before we move on, the curious might wonder if ‘’categories are graphs’‘then what is the analgoue to’‘X are hypergraphs’’, it is multicategories.
The remainder of this part of these notes is to build-up the material needed to realize the notion of ‘forgetful’.
Natural Transformations
Recall, that a natural transformation η : F ⟶ G is a family ∀ {X : Obj 𝒞} → F X ⟶ G X that satisfies the naturality condition: ∀ {A B} {f : A ⟶ B} → F f ⨾ η {B} ≡ η {A} ⨾ G f. Let us look at this from a few different angles; in particular, what does the adjective ‘natural’ actually mean? It’s been discussed on many forums and we collect a few of the key points here.
Given two functors F , G, for any object x we obtain two objects F x, G x and so a morphism from F to G ought to map such F x to G x. That is, a morphsim of functors is a family η : ∀ {x : Obj} → F x ⟶ G x. Now for any f : a → b there are two ways to form a morphism F a → G b: F f ⨾ η {b} and η {a} ⨾ G f. Rather than make a choice each time we want such a morphism, we eliminate the choice all together by insisting that they are identical. This is the naturality condition.
This is similar to when we are given three morphisms f : a → b , g : b → c , h : c → d, then there are two ways to form a morphism a → d: (f ⨾ g) ⨾ h and f ⨾ (g ⨾ h). Rather than make a choice each time we want such a morphism, we eliminate the choice all together by insisting that they are identical. This is the associativity condition for categories.
Notice that if there’s no morphism F x ⟶ G x for some x, they by definition there’s no natural transformation F ⟶̇ G.
= “the X which requires no arbitrary choices” = “the canonical/standard X”`
That is,
it is a natural construction/choice
=
distinct people would arrive at the same construction;
(no arbitrary choice or cleverness needed)
=
there is actually no choice, (ie only one possiility), and so
two people are expected to arrive at the same 'choice'Thus, if a construction every involves having to decide between distinct routes, then chances are the result is not formally natural.
Some would even say: “natural” = “God-given”.
“natural” = “resonable or expected in the ambient context” ; sometimes this ‘inution’ is developed from working in a field for some time. Sometimes it just “feels” natural.
“natural solution” = “has properties of all other solutions”
[To consider: is a natural solution then just an initial solution? That is, an intial transformation?]
A natural transformation can be thought of as a polymorphic function
Recall that a ‘monomorphic’ operation makes no use of type variables in its signature, whereas a ‘polymorphic’ operation uses type variables in its signature.
Inspecting type parameters or not leads to the distinction of ad hoc plymorphism vs. parametric polymorphism —the later is the kind of polymorphism employed in functional language like Haskell and friends ans so such functions are natural transformations by default! Theorems for free!
For example,
size : ∀ {X} → List X → 𝒦 ℕ X -- where `𝒦 x y ≔ Id {x}` for morphisms and `𝒦 x y ≔ x` for objects
size [x₁, …, xₙ] = nis a polymorphic function and so naturality follows and is easily shown. So we have always have and so size : List ⟶̇ 𝒦.
On the other hand, the polymorphic function
whyme : ∀ {X} → List X → 𝒦 Int X
whyme {X} [x₁,…,xₙ] = If X = ℕ then 1729 else nis not natural: the needed equation F f ⨾ η {B} = η {A} ⨾ G f for any f : A → B breaks as witnessed by f = (λ x → 0) : ℝ → ℕ and any list with length n ≠ 1729, and this is easily shown.
One might exclaim, ‘’hey! this only works ’cuz you’re using Ramanujan’s taxi-cab number! 1729 is the smallest number expressible as a sum of 2 cubes in 2 ways: 1729 = 12³ + 1³ = 10³ + 9 ³.’’ I assure you that this is not the reason that naturality breaks, and I commend you on your keen observation.
Notice that it is natural if we exclude the type inspected, ℕ. That is, if we only consider f : A → B with A ≠ ℕ ≠ B. In general, is it the case that a transformation can be made natural by excluding the types that were inspected?
Before we move on, obverse that a solution in h to the absorptive-equation F f ⨾ h = h is precisely a natural transformation from F to a diagonal functor. where (x ∈ Σ y ∶ Y • P y) = (Σ y ∶ Y • y ≡ x ∧ P y).
In particular, since g ⨾ (λ _ → e) = (λ x → (λ _ → e) (g x) ) = (λ x → e) that is g ⨾ K e = K e, we have that Is the converse also true? If h ∈ F ⟶̇ 𝒦 X then h = K e for some e?
The idea that a natural transformation cannot make reference to the type variable at all can be seen by yet another example.
data 𝟙 : Set where ★ : 𝟙
-- a choice function: for any type X, it yields an argument of that type
postulate ε : (X : Set) → X
nay : ∀ {X} → X → X
nay {X} _ = ε XNow nautrality Id f ⨾ nay {B} = nay {A} ⨾ Id f breaks as witnessed by f = (λ _ → εℕ + 1) : 𝟙 → ℕ.
From this we may hazard the following: if we have natural transformations ηᵢ : ∀ {X : Objᵢ} → F X ⟶ G X where the Objᵢ partition the objects available —ie, Obj = Σ i • Objᵢ— then the transformation η {(i, X)} = ηᵢ is generally unnatural since it clearly makes choices, for each partition.
A family of morphisms is ‘natural in x’ precisely when it is defined no it is uniform! With this view, the naturality condition is thought of as a ‘simultaneity’
The idea of naturality as uniformly-definable is pursued by Hodges and Shelah.
Recall that a functor can be thought of as endowing an object with structure. Then a transformation can be thought of as a restructuring operation and naturality means that it doesn’t matter whether we restructure or modify first, as long as we do both.
It may help to think of ‘’there’s a natural transformation from F to G’‘to mean’‘there’s an obvious/standard/canconical way to transform F structure into G structure’’.
Likewise, ‘’F is naturally isomorphic to G’‘may be read’‘F is obviously isomorphic to G’’.
Sometimes we can show ‘’F X is isomorphic to G X, if we make a choice dependent on X’’ and so the isomorphism is not obvious, since a choice must be made.
I think Richard Bird refers to the naturality condition as a promotion law where the functors involved are thought of as (list) constructions.
The nomenclature is used ‘’to express the idea than operation on a compund structure can be ’promoted’ into its componenets’.
Reading F f ⨾ η {B} = η {A} ⨾ G f from left to right: mapping f over the result of handling a complicated strucure is the same as mapping f over the complex dataum than handling the result.
Lists give many examples of natural transformations by considering a categorical approach to the theory of lists.
The naturality condition can be seen as a rewrite rule that let’s us replace a complicated or inefficient side with a simplier or more efficient yet equivalent expression. I think I first learned this view of equations at the insistence of
Given two functors F,G : 𝒞 ⟶ 𝒟 let us construe them as only graph homomorphisms. Then each is a model of the graph 𝒰₀ 𝒞 —each intereprets the nodes and edges of 𝒰₀ 𝒞 as actual objects and morphisms of 𝒟— and a natrual transformation is then nothing more than a morphism of models.
models were introduced?}
In the setting of types and functions, η : F ⟶̇ G means we have η (F f x) = G f (η x) which when read left-to-right says that η is defined by pattern-matching on its argument to obtain something of the form F f x then it is defined recursively by examining x and then applying G f to the result —of course there’s some base case f definitions as well.
Alternatively, the input to η is of the form F … and its output is of the form G ….
A functor among poset categories is an order-preserving function and a natural transformation f ⟶ g is a proof that f ≤ g pointwise: ∀ x • f x ≤ g x —all the other pieces for a natural transformation are automatic from the definition of poset category.
A functor among monoids (as categories) is just a monoid homomorphism: A natural transformation (f, prf) ⟶ (g, prf') is a point n : N with ∀ x ∶ M • f x ⊗ n = n ⊗ g x, a ‘conjugation’ by n that takes f to g.
Recall from the introduction 𝒰(S, ⊕, e) = S was the underlying functor from monoids to sets. Let 𝒰 × 𝒰 be the functor that for objects M ↦ 𝒰 M × 𝒰 M and for morphisms h ↦ λ (x,y) → (h x, h y). Then the monoid multiplication (of each monoid) is a natural transformation 𝒰 × 𝒰 ⟶ 𝒰, where naturality says that for any monoid homomorphism h, the application of 𝒰 h to the (monoid) multiplication of two elements is the same as the (monoid) multiplication of the 𝒰 h-images of the two elements, and this is evident from the homomorphism condition.
Extending to finite products, 𝒱 ≔ Σ n ∶ ℕ • ∏ i ∶ 1..n • 𝒰, the natural transformation 𝒱 ⟶̇ 𝒰 is usually called fold, reduce, or cata and 𝒱 is known as the free monoid functor with notations A* = List A = 𝒱 A.
Loosely put,
𝒱₀ : Monoid → Set
𝒱₀ M = Σ n ∶ ℕ • ∏ i : 1..n • 𝒰 M -- finite sequences of elements from M
𝒱₁ : ∀ {M N : Monoid} → (M ⟶ N) → 𝒱₀ M → 𝒱₀ N
𝒱₁ (h , prf) = λ (n , x₁, …, xₙ) → (n , h x₁ , … , h xₙ)
fold : ∀ {M : Monoid} → 𝒱₀ M → 𝒰₀ M
fold {(M, ⊕, e)} = λ (n , x₁, …, xₙ) → x₁ ⊕ ⋯ ⊕ xₙNow for any monoid homomorphism h, applying induction, yields
h₀(x₁ ⊕ ⋯ ⊕ xₙ) = h₀ x₁ ⊕ ⋯ ⊕ h₀ xₙ where h₀ = 𝒰 (h₀, prf) = 𝒰 hwhich is just naturality
𝒰 h ∘ fold {M} = fold {N} ∘ 𝒱 htransformation. }
This is mentioned in the Barr-wells-ctcs category theory text, citing [Linton,1969b], [Linton, 1969a].
For example, src, tgt —from the graph signature— give natural transformations V ⟶ E from the vertex functor to the edge functor …
Recall that V(G) is essentially ℙ₀ ⟶ G where ℙₙ is the graph of n edges on n+1 vertices 0..n with typing i : i-1 ⟶ i, which I like to call ‘the path graph of length n’; and in particular ℙ₀ is the the graph of just one dot, called 0, and no edges. —earlier I used the notation [n], but I’m using P since I like the view point of paths.
What does it mean that ‘V(G) is essentially ℙ₀ ⟶ G’? It means that the vertices functor —𝒱 : Graph ⟶ Set takes objects G ↦ V(G) and morphisms h ↦ ver h— can be represented as the hom functor (ℙ₀ ⟶_), that is to say 𝒱 ≅ (ℙ₀ ⟶ _) within Func Graph Set —notice that we arrived at this expression by quote-unqoute eta-reducing ‘V(G) is essentially ℙ₀ ⟶ G’ ;)
More generally, we have the functor ℙₙ ⟶ _ which yields all paths of length n for a given graph.
Observe that we also have an edges functor. Recall the ‘untyped edges’, or arrows, A(G) ≔ Σ x ∶ V(G) • Σ y ∶ V(G) • (x ⟶ y), then (arrows) 𝒜 : Graph ⟶ Set takes objects G ↦ A(G) and morphisms h ↦ λ (x,y,e) → (ver h x, ver h y, edge h e).
Functor Categories
With a notion of morphisms between functors, one is led inexorably to ask whether functors as objects and natural transformations as morphisms constitute a category? They do! However, we leave their definition to the reader —as usual, if the reader is ever so desperate for solutions, they can be found as comments in the unruliness that is the source file.
Func : ∀ {i j i' j'} (𝒞 : Category {i} {j}) (𝒟 : Category {i'} {j'}) → Category
Func 𝒞 𝒟 = {! exercise !}A hint: the identity natural transformation is the obvious way to get from F X to F X, for any X given F —well the only way to do so, without assuming anything else about the functor F, is simply Id {F X}. This is the ‘natural’ choice, any other choice would be ‘unnatural’ as it would require some ‘cleverness’. Another hint: the obvious way to define η ⨾ γ to get F X ⟶ H X from F X ⟶ G X ⟶ H X is composition of morphisms in the category! That is, pointwise composition. Nothing ‘clever’, just using the obvious candidates!
This is a good exercise as it will show you that there is an identity functor and that composition of functors is again a functor. Consequently, functors are in abundance: given any two, we can form new ones by composition.
It is a common construction that when a type Y is endowed with some structure, then we can endow the function space X → Y, where X is any type, with the same structure and we do so ‘pointwise’. This idea is formalized by functor categories. Alternatively, one can say we have ‘categorified’ the idea; where functors and possibly adding some coherence laws.
There are people who adhere to something called ‘set theory’ which is essentialy type theory but ignoring types, loosely put they work only with the datatype
data SET : Set where
Elem : ∀ {A : Set} → A → SETSuch heathens delegate types-of-types into ‘classes’ of ‘small’ and ‘big’ sets and it’s not uniform enough for me. Anyhow, such people would say that functor categories ‘’cannot be constructed (as sets)’‘unless one of the categories involved is’‘small’’. Such shenanigans is ignored due to the hierarchy of types we are using :-)
We must admit that at times the usage of a single type, a ‘uni-typed theory’ if you will can be used when one wants to relise types in an extrinsic fashion rather than think of data as intrinsically typed. Everything has its place … nonetheless, I prefer (multi)typed settings!
Let 𝟙 ≔ [ • ] be the discrete category of one object (and only the identity arrow on it). Then 𝒞 ≅ Func 𝟙 𝒞.
For example, let 𝟚₀ ≔ [• •] be the discrete category of two objects. Then square category can be defined 𝒞 ⊗ 𝒞 ∶≅ Func 𝟚₀ 𝒞. The subscript 0 is commonly used for matters associated with objects and the name 𝟚₀ is suggestive of the category of 2 objects only.
More generally, if 𝒩 is the discrete category of n objects, then the n-fold product category is defined (∏ i ∶ 1..n • 𝒞) ∶≅ Func 𝒩 𝒞.
We can add an arrow to 𝟚₀ to obtain another category…
Let 𝟚 ≔ • ⟶ • be the category of two objects, call them 0 and 1, with one arrow between them. Then a functor 𝟚 ⟶ 𝒞 is precisely a morphism of 𝒞 and a natural transformation f ⟶ g boils down to just a pair of morphisms (h,k) with h ⨾ g = f ⨾ k. Hence, ‘the arrow category of 𝒞’ is $≔ Func 𝟚 𝒞: the category with objects being 𝒞-morphisms and morphisms being ‘commutative squares’.
as such it is common to write 𝒳 ^ 𝒴 ≔ Func 𝒳 𝒴.
can make probes to discover its structure. The objects are just functors 𝟙 ⟶ 𝒞 and the morphisms are just functors 𝟚 ⟶ 𝒞.
The ‘’category of presheaves of 𝒞’’ is the category PSh 𝒞 ≔ Func (𝒞 ᵒᵖ) 𝒮e𝓉.
This is a pretty awesome category since it allows nearly all constructions in 𝒮e𝓉 to be realised! Such as subsets, truth values, and even powersets! All these extra goodies make it a ‘’topos’‘aka’‘power allegory’’ —the first is a category that has all finite limits and a notion of powerset while the second, besides the power part, looks like a totally different beast; the exhilaration!
The ‘slice category’ of 𝒞 ‘over’ B : Obj 𝒞 is the category 𝒞 / B ≔ Σ F ∶ Func 𝟚 𝒞 • (F 1 = B). That is, the category of objects being 𝒞-morphisms with target B and morphisms f ⟶ g being (h,k) with h ⨾ g = f ⨾ k but a natural choice for k : B ⟶ B is Id and so we can use morphism type (f ⟶' g) ≔ Σ h : src f ⟶ src g • h ⨾ g = f. This is seen by the observation (h, k) ∈ f ⟶ g ⇔ h ∈ (f ⨾ k) ⟶' g; of course a formal justification is obtained by showing _⟶_ ≅ _⟶'_ within Func (𝒞 ᵒᵖ ⊗ 𝒞) 𝒮e𝓉…which I have not done and so may be spouting gibberish!
Just as the type Σ x ∶ X • P x can be included in the type X, by forgetting the second component, so too the category Σ F ∶ 𝟚 ⟶ 𝒞 • F 1 ≈ B can be included into the category 𝒞 and we say it is a ‘subcategory’ of 𝒞.
The notation Σ o ∶ Obj 𝒞 • P o defines the subcategory of 𝒞 obtained by deleting all objects not satisfying P and deleting all morphisms incident to such objects; i.e., the category 𝒟 with
This is the largest/best/universal subcategory of 𝒞 whose objects satisfy P. Formalize this via a universal property ;)
Func S 𝒮e𝓉 ≅ 𝒮e𝓉 / S, where S in the left is construed as a discrete category and in the right is construed as an object of 𝒮e𝓉.
This is because a functor from a discrete category need only be a function of objects since there are no non-identity morphisms. Then a functor f : S ⟶ Set yields an S-targeted function (Σ s ∶ S • f s) → S : (λ (s , X) → s). Conversely a function g : X → S yields a functor S ⟶ Set : (λ s → (Σ x ∶ X • g x ≡ s)).
Because of this example, 𝒞 / B can be thought of as ‘𝒞-objects indexed by B’.
In a similar spirit, we can identify natural transformations as functors!
A functor N : 𝒞 ⟶ 𝒟 ^ 𝟚 gives, for each object C : Obj 𝒞 an object in 𝒟 ^ 𝟚 which is precisely an arrow in 𝒟, type it as N C : FC ⟶ GC i.e., FC = N C 0 , GC = N C 1, and for each arrow f : A ⟶ B in 𝒞 we obtain an arrow N f : N A ⟶ N B in 𝒟 ^ 𝟚 which is precisely a commutative square in 𝒟, that is a pair of 𝒟-arrows (Ff , Gf) = Nf with N A ⨾ Gf = Ff ⨾ N B.
Extended the notation Fx of the previous paragraph to a functor 𝒞 ⟶ 𝒟 by F x ≔ Fx; likewise for G. The object and morphism mappings are clear, but what about functoriality? We prove it for both F, G together.
Identity:
(F Id , G Id)
≡⟨ definition of F and G ⟩
N Id
≡⟨ N is a functor ⟩
Id in 𝒟 ^ 𝟚
≡⟨ identity in arrow categories ⟩
(Id , Id)Composition:
( F (f ⨾ g) , G (f ⨾ g) )
≡⟨ definition of F and G ⟩
N (f ⨾ g)
≡⟨ N is a functor ⟩
N f ⨾ N g
≡⟨ definition of F and G ⟩
(Ff, Gf) ⨾ (Fg , Gg)
≡⟨ composition in arrow categories ⟩
(Ff ⨾ Fg , Gf ⨾ Gg)
≡⟨ definition of F and G as notation ⟩
(F f ⨾ F g , G f ⨾ G g)Sweet!
Conversely, given a natural transformation η : F ⟶ G we define a functor N : 𝒞 ⟶ 𝒟 ^ 𝟚 by sending objects C to η {C} : F C ⟶ G C, which is an object is 𝒟 ^ 𝟚, and sending morphisms f : A ⟶ B to pairs (G f , F f), which is a morphism in 𝒟 ^ 𝟚 due to naturality of η: η {A} ⨾ G f = F f ⨾ η {B}. It remains to show that N preserves identities and composition.
Now it remains to show that these two processes are inverses and the isomorphism claim is complete. Woah!
Similarly, we can show Func (𝟚 ⊗ 𝒞) 𝒟 ≅ (Σ F₀ , F₁ ∶ 𝒞 ⟶ 𝒟 • NatTrans F₁ F₂) by showing the ‘’the universal property of exponentiation’’ 𝒳 ⟶ (𝒵 ^ 𝒴) ≅ (𝒳 ⊗ 𝒴 ⟶ 𝒵, or more directly: to/from direction obtained by setting H i = Fᵢ on objects and likewise for morphisms but with H(Id, 1) = η where 1 : 0 ⟶ 1 is the non-identity arrow of 𝟚.
(Spoilers! Alternatively: Arr (Func 𝒞 𝒟) ≅ 𝟚 ⟶ 𝒞 ^ 𝒟 ≅ 𝒞 × 𝟚 ⟶ 𝒟 since 𝒞𝒶𝓉 has exponentials, and so the objects are isomorphic; i.e., natural transformations correspond to functors 𝒞×𝟚⟶𝒟)
Why are we mentioning this alternative statement? Trivia knowledge of-course! On a less relevant note, if you’re familiar with the theory of stretching-without-tearing, formally known as topology and it’s pretty awesome, then you might’ve heard of paths and deformations of paths are known as homotopies and are just continuous functions X × I ⟶ Y for topological spaces X and Y and I = [0,1] is the unit interval. Letting 𝒥 = 𝟚 be the ‘categorical interval’ we have that functors 𝒞 × 𝒥 ⟶ 𝒟 are, by the trivia-relevant result, the same as natural transformations. That is, natural transformations extend the notion of homotopies, or path-deformations.
On mathoverflow, the above is recast succinctly as: a natural transformation from F to G is a functor, targeting an arrow category, whose ‘source’ is F and whose ‘target’ is G. (F ⟶̇ G : 𝒞 ⟶ 𝒟) ≅ Σ η ∶ 𝒞 ⟶ Arr 𝒟 • Src ∘ η = F ∧ Tgt ∘ η = G Where, the projection functors
Src, Tgt : Arr 𝒟 ⟶ 𝒟
Src (A₁ , A₂ , f) = A₁
Src (f , g , h₁ , h₂ , proofs) = h₁with Tgt returning the other indexed items.
We give an example of a functor by building on our graphs from before. After showing that graphs correspond to certain functors, we then mention that the notion of graph-map is nothing more than the the associated natural transformations!
module graphs-as-functors whereLet us construct our formal graph category, which contains the ingredients for a graph and a category and nothing more than the equations needed of a category. The main ingredients of a two-sorted graph are two sort-symbols E, V, along with two function-symbols s, t from E to V —this is also called ‘the signature of graphs’. To make this into a category, we need function-symbols id and a composition for which it is a unit.
-- formal objects
data 𝒢₀ : Set where E V : 𝒢₀
-- formal arrows
data 𝒢₁ : 𝒢₀ → 𝒢₀ → Set where
s t : 𝒢₁ E V
id : ∀ {o} → 𝒢₁ o o
-- (forward) composition
fcmp : ∀ {a b c} → 𝒢₁ a b → 𝒢₁ b c → 𝒢₁ a c
fcmp f id = f
fcmp id f = fPutting it all together,
instance
𝒢 : Category
𝒢 = record
{ Obj = 𝒢₀
; _⟶_ = 𝒢₁
; _⨾_ = fcmp
; assoc = λ {a b c d f g h} → fcmp-assoc f g h
; Id = id
; leftId = left-id
; rightId = right-id
}
where
-- exercises: prove associativity, left and right unit lawsNow we can show that every graph G gives rise to a functor: a semantics of 𝒢 in 𝒮e𝓉.
toFunc : Graph → Functor 𝒢 𝒮e𝓉
toFunc G = record { obj = ⟦_⟧₀ ; mor = ⟦_⟧₁ ; id = ≡-refl ; comp = λ {x y z f g} → fcmp-⨾ {x} {y} {z} {f} {g} }
where
⟦_⟧₀ : Obj 𝒢 → Obj 𝒮e𝓉
⟦ 𝒢₀.V ⟧₀ = Graph.V G
⟦ 𝒢₀.E ⟧₀ = Σ x ∶ Graph.V G • Σ y ∶ Graph.V G • Graph._⟶_ G x y
⟦_⟧₁ : ∀ {x y : Obj 𝒢} → x ⟶ y → ⟦ x ⟧₀ ⟶ ⟦ y ⟧₀
⟦ s ⟧₁ (src , tgt , edg) = src
⟦ t ⟧₁ (src , tgt , edg) = tgt
⟦ id ⟧₁ x = x
-- exercise: `fcmp` is realised as functional composition
fcmp-⨾ : ∀{x y z} {f : 𝒢₁ x y} {g : 𝒢₁ y z} → ⟦ fcmp f g ⟧₁ ≡ ⟦ f ⟧₁ ⨾ ⟦ g ⟧₁Conversely, every such functor gives a graph:
fromFunc : Functor 𝒢 𝒮e𝓉 → Graph
fromFunc F = record {
V = obj F 𝒢₀.V
; _⟶_ = λ x y → Σ e ∶ obj F 𝒢₀.E • src e ≡ x × tgt e ≡ y -- the type of edges whose source is x and target is y
}
where tgt src : obj F 𝒢₀.E → obj F 𝒢₀.V
src = mor F 𝒢₁.s
tgt = mor F 𝒢₁.tIt is to be noted that we can define ‘’graphs over 𝒞’’ to be the category Func 𝒢 𝒞. Some consequences are as follows: notion of graph in any category, the notion of graph-map is the specialisation of natural transformation (!), and most importantly: all the power of functor categories is avaiable for the study of graphs.
In some circles, you may hear people saying an ‘algebra over the signature of graphs’ is an interpretation domain (𝒞) and an operation (Functor 𝒢 𝒞) interpreting the symbols.
We no longer make use of this two-sorted approach to graphs.
A few categorical constructions
We briefly take a pause to look at the theory of category theory. In particular, we show a pair of constructions to get new categories from old ones, interpret these constructions from the view of previously mentioned categories, and discuss how to define the morphism type _⟶_ on morphisms themselves, thereby yielding a functor.
Opposite
The ‘dual’ or ‘opposite’ category 𝒞 ᵒᵖ is the category constructed from 𝒞 by reversing arrows: (A ⟶ B) ≔ (B ⟶ A) and then necessairly (f ⨾ g) ≔ g ⨾ f. A contravariant functor, or cofunctor, is a functor F from an opposite category and so there is a reversal of compostions: F(f ⨾ g) = F g ⨾ F f.
_ᵒᵖ : ∀ {i j} → Category {i} {j} → Category
𝒞 ᵒᵖ = {! exercise !}Notice that 𝒞 ᵒᵖ ᵒᵖ = 𝒞 and 𝒞 ᵒᵖ ≅ 𝒞 –one may have an intuitive idea of what this isomorphsim means, but formally it is only meaningful in the context of an ambient category; keep reading ;)
– we must admit that for categories, the notion of isomorphism is considered less useful than that of equivalence which weakens the condition of the to-from functors being inverses to just being naturaly isomorphic to identites. See evil.
Some interpretations: 𝒮e𝓉 ᵒᵖ is usual sets and functions but with ‘backwards composition’: agda infix 10 _∘_ _∘_ : ∀ {i j } {{r : Category {i} {j}}} {A B C : Obj r} → B ⟶ C → A ⟶ B → A ⟶ C f ∘ g = g ⨾ f Indeed, we have g ⨾ f within 𝒞 = f ∘ g within 𝒞 ᵒᵖ; which is how these composition operators are usually related in informal mathematics (without mention of the ambient categories of-course).
On a more serious note, the opposite of 𝒮e𝓉 is clearly 𝓉e𝒮 haha —technically for the purposes of this pun we identify the words ‘opposite’ and ‘reverse’.
For a discrete category, its opposite is itself. For a monoid (viewed as a category), its opposite is itself if the monoid operation is commutative, otherwise it is the ‘dual monoid’. For a poset (viewed as a category), its opposite is the ‘dual poset’: (P, ⊑)ᵒᵖ = (P, ⊒).
In particular, the ‘least upper bound’, or ‘supremum’ in (P, ⊑) of two elements x,y is an element s with the ‘universal property’: ∀ z • x ⊑ z ∧ y ⊑ z ≡ s ⊑ z. However, switching ⊑ with ⊒ gives us the notion of ‘infimum’, ‘greatest upper bound’! So any theorems about supremums automatically hold for infimums since the infifum is nothing more than the supremum in the dual category of the poset.
It is not difficult to see that this idea of ‘2 for the price of 1’ for theorems holds for all categories.
What about the category of functors and natural transformations?
Speaking of functors, we can change the type of a functor by ᵒᵖ-ing its source and target, while leaving it alone,
-- this only changes type
opify : ∀ {i j i' j'} {𝒞 : Category {i} {j}} {𝒟 : Category {i'} {j'}} → Functor 𝒞 𝒟 → Functor (𝒞 ᵒᵖ) (𝒟 ᵒᵖ)
opify F = record { obj = obj F ; mor = mor F ; id = Functor.id F ; comp = Functor.comp F }‘’Category Theory is the opium of the people!’’ — Karl Marx might say it had cats existed in his time
This two definitions seem to indicate that we have some form of opposite-functor … ;) —keep reading!
opify seems to show that Functor 𝒞 𝒟 ≡ Functor (𝒞 ᵒᵖ) (𝒟 ᵒᵖ), or alternatively a functor can have ‘two different types’ —this is akin to using the integers as reals without writing out the inclusion formally, leaving it implicit; however, in the Agda mechanization everything must be made explicit —the type system doesn’t let you get away with such things. Professor Maarten Fokkinga has informed me that the formalization allowing multiple-types is called a pre-category.
With 𝒞𝒶𝓉 in-hand, we can formalise the opposite, or ∂ual, functor:
∂ : ∀ {i j} → 𝒞𝒶𝓉 {i} {j} ⟶ 𝒞𝒶𝓉
∂ = record { obj = _ᵒᵖ ; mor = opify ; id = ≡-refl ; comp = ≡-refl }Conjecture: assuming categories are equipped with a contravariant invultionary functor that is identity on objects, we can show that the identity functor is naturally isomorphic to the opposite functor.
ah-yeah : ∀ {i j}
-- identity on objects cofunctor
→ (_˘ : {{𝒞 : Obj (𝒞𝒶𝓉 {i} {j})}} → ∀ {x y : Obj 𝒞} → x ⟶ y → y ⟶ x)
→ (Id˘ : ∀ {𝒞} {x : Obj 𝒞} → (Category.Id 𝒞 {x}) ˘ ≡ Category.Id 𝒞 {x})
→ (⨾-˘ : ∀ {𝒞} {x y z : Obj 𝒞} {f : x ⟶ y} {g : y ⟶ z} → (f ⨾ g)˘ ≡ g ˘ ⨾ f ˘)
-- which is involutionary
→ (˘˘ : ∀ {𝒞} {x y : Obj 𝒞} {f : x ⟶ y} → (f ˘) ˘ ≡ f)
-- which is respected by other functors
→ (respect : ∀ {𝒞 𝒟} {F : 𝒞 ⟶ 𝒟} {x y : Obj 𝒞} {f : x ⟶ y} → mor F (f ˘) ≡ (mor F f)˘)
-- then
→ ∂ ≅ Id within Func (𝒞𝒶𝓉) 𝒞𝒶𝓉 ah-yeah = {! exercise !}Some things to note. Categories whose morphisms are all isomorphisms are called ‘groupoids’ —groups are just one-object groupoids. Consequently, restricted to groupoids the opposite functor is naturally isomorphic to the identity functor!
In fact, the group case was the motivator for me to conjecture the theorem, which took a while to prove since I hadn’t a clue what I needed to assume. Here we’d use a ˘ ≔ a ⁻¹.
Consider the category Rel whose objects are sets and whose morphisms are ‘typed-relations’ (S, R, T), where R is a relation from set S to set T, and composition is just relational composition —the notion of ‘untyped’, or multi-typed, morphisms is formalized as pre-categories; see Fokkinga. Then we can define an endofunctor by taking -˘ to be relational converse: x (R ˘) y ⇔ y R x. Consequently, restricted to the category Rel we have that the opposite functor is naturally isomorphic to the identity functor.
The above items are instance of a more general concept, of course.
A category with an involutionary contravariant endofunctor that is the identity on objects —and the functor is denoted as a superscript suffix by †, *, ˘, respectively. The dagger notation probably comes from the hilbert space setting while the converse notation comes from the relation algebra setting. As far as I know, the first two names are more widely known. A dagger category bridges the gap between arbitrary categories and groupoids.
Just as matrices with matrix multiplication do not form a monoid but rather a category, we have that not all matrices are invertible but they all admit transposition and so we have a dagger category. In the same vein, relations admit converse and so give rise to a category with converse.
Besides relations and groupoids, other examples include discrete categories with the dagger being the identity functor every monoid with an anti-involution is trivially a dagger category; e.g., lists with involution being reverse.
commutative monoids are anti-involutive monoids with antiinvolution being identity
Spoilers!! Just as the category of categories is carestian closed, so too is the category of dagger categories and dagger preserving functors (cf respect above).
Products
For any two categories 𝒞 and 𝒟 we can construct their ‘product’ category 𝒞 ⊗ 𝒟 whose objects and morphisms are pairs with components from 𝒞 and 𝒟: Obj (𝒞 ⊗ 𝒟) = Obj 𝒞 × Obj 𝒟 and (A , X) ⟶ (B , Y) = (A ⟶ B) × (X ⟶ Y).
-- we cannot overload symbols in Agda and so using `⊗` in-place of more common `×`.
_⊗_ : ∀ {i j i' j'} → Category {i} {j} → Category {i'} {j'} → Category
𝒞 ⊗ 𝒟 = {! exercise !}Observe that in weaker languages a category is specified by its objects, morphisms, and composition —the proof obligations are delegated to comments, if they are realized at all. In such settings, one would need to prove that this construction actually reduces a full-fledged category. Even worse, this proof may be a distance away in some documentation. With dependent types, our proof obligation is nothing more than another component of the program, a piece of the category type.
In a similar fashion we can show that the sum of two categories is again a category and in general we have the same for quantified variants: 𝒬 𝒞 ∶ Family • 𝒞 where 𝒬 ∈ { ∏ , Σ }. For the empty family, the empty sum yields the category 𝟘 with no objects and the empty sum yields the category 𝟙 of one object. One can then show the usual ‘laws of arithmetic’ —i.e., an commutative monoid— hold in this setting: letting ★ ∈ {+,×}, we have associtivity A ★ (B ★ C) ≅ (A ★ B) ★ C, symmetry A ★ B ≅ B ★ A, unit 𝟙 × A ≅ 𝟘 + A ≅ A, and zero 𝟘 × A ≅ 𝟘. These notions can be defined for any category though the objects may or may not exist — in 𝒮e𝓉 and 𝒢𝓇𝒶𝓅𝒽, for example, they do exist ;) —and these associated arithmetical laws also hold.
Question: what of the distributively law, A × (B + C) ≅ (A × B) + (A × C), does it hold in the mentioned cases? Let 𝒫𝒮e𝓉 be the category of sets with a distinguished point, i.e., Σ S : Obj 𝒮e𝓉 • S, and functions that preserve the ‘point’, one can then show —if he or she so desires, and is not lazy— that this category has notions of product and sum but distributively fails.
Some interpretations: For discrete categories, this is the usual Cartesian product. For monoid (or poset) categories, this says that the product of two monoids (or posets) is again a monoid (respectively poset. This follows since the product does not affect the number of objects and so the product is again a one-object category, i.e., a monoid (poset respectively).
As expected, we have projections,
Fst : ∀ {i j i' j'} {𝒞 : Category {i} {j}} {𝒟 : Category {i'} {j'}} → Functor (𝒞 ⊗ 𝒟) 𝒞
Fst = record { obj = proj₁ ; mor = proj₁ ; id = ≡-refl ; comp = ≡-refl }
Snd : ∀ {i j i' j'} {𝒞 : Category {i} {j}} {𝒟 : Category {i'} {j'}} → Functor (𝒞 ⊗ 𝒟) 𝒟
Snd = record { obj = proj₂ ; mor = proj₂ ; id = ≡-refl ; comp = ≡-refl }For types we have (𝒳 × 𝒴 ⟶ 𝒵) ≅ (𝒳 ⟶ 𝒵 ^ 𝒴) ≅ (𝒴 ⟶ 𝒵 ^ 𝒳), and categories are essentially types endowed with nifty structure, and so we expect it to hold in that context as well.
-- Everyone usually proves currying in the first argument,
-- let's rebel and do so for the second argument
curry₂ : ∀ {ix jx iy jy iz jz}
{𝒳 : Category {ix} {jx}} {𝒴 : Category {iy} {jy}} {𝒵 : Category {iz} {jz}}
→ Functor (𝒳 ⊗ 𝒴) 𝒵 → Functor 𝒴 (Func 𝒳 𝒵)
curry₂ = {! exercise !}Pointwise extensions and the hom functor
Just as addition can be extended to number-valued functions pointwise f + g ≔ λ x → f x + g x, we can do the same thing with functors.
-- for bifunctor `_⊕_` and functors `F, G` we have a functor `x ↦ F x ⊕ G x`
pointwise : ∀ {ic jc id jd ix jx iy jy}
{𝒞 : Category {ic} {jc}} {𝒟 : Category {id} {jd}} {𝒳 : Category {ix} {jx}} {𝒴 : Category {iy} {jy}}
→ Functor (𝒳 ⊗ 𝒴) 𝒟 → Functor 𝒞 𝒳 → Functor 𝒞 𝒴
→ Functor 𝒞 𝒟
pointwise = {! exercise !}Since p ≡ (proj₁ p , proj₂ p), we have that the pointwise extension along the projections is the orginal operation.
exempli-gratia : ∀ {𝒞 𝒟 𝒳 𝒴 : Category {ℓ₀} {ℓ₀}} (⊕ : Functor (𝒳 ⊗ 𝒴) 𝒟)
→ let _⟨⊕⟩_ = pointwise ⊕
in
Fst ⟨⊕⟩ Snd ≡ ⊕
exempli-gratia Bi = funcext (≡-cong (obj Bi) ≡-refl) (≡-cong (mor Bi) ≡-refl)An example bifunctor is obtained by extending the –> to morphisms: given f : A ⟶ B , g : C ⟶ D we define (f ⟶ g) : (B ⟶ C) → (A ⟶ C) by λ h → f ⨾ h ⨾ g as this is the only way to define it so as to meet the type requirements.
Hom : ∀ {i j} {𝒞 : Category {i} {j} } → Functor (𝒞 ᵒᵖ ⊗ 𝒞) 𝒮e𝓉
-- hence contravariant in 'first arg' and covaraint in 'second arg'
Hom {i} {j} {𝒞} = record {
obj = λ AB → let (A , B) = AB in A ⟶ B
; mor = λ fg → let (f , g) = fg in λ h → f ⨾ h ⨾ g
; id = λ {AB} → let (A , B) = AB in extensionality (λ {h} → begin
Id ⨾ h ⨾ Id
≡⟨ leftId ⟩
h ⨾ Id
≡⟨ rightId ⟩
h
∎)
; comp = λ {x y z fg fg'} → let (f , g) = fg ; (f' , g') = fg' in extensionality (λ {h} → begin
(f' ⨾ f) ⨾ h ⨾ (g ⨾ g')
≡⟨ assoc ⟩
f' ⨾ (f ⨾ (h ⨾ (g ⨾ g')))
≡⟨ ⨾-cong₂ (≡-sym assoc) ⟩
f' ⨾ ((f ⨾ h) ⨾ (g ⨾ g'))
≡⟨ ⨾-cong₂ (≡-sym assoc) ⟩
f' ⨾ ((f ⨾ h) ⨾ g) ⨾ g'
≡⟨ ⨾-cong₂ (≡-cong₂ _⨾_ assoc ≡-refl) ⟩
f' ⨾ (f ⨾ h ⨾ g) ⨾ g'
∎)}
where
⨾-cong₂ : ∀ {A B C : Obj 𝒞} {f : A ⟶ B} {g g' : B ⟶ C} → g ≡ g' → f ⨾ g ≡ f ⨾ g'
⨾-cong₂ = ≡-cong₂ _⨾_ ≡-reflThe naming probably comes from the algebra/monoid case where the functors are monoid homomorphisms. Some prefer to use the name Mor, short for morphisms, and that’s cool too. While Haskell programmers might call this the Reader functor.
Usual notation for this functor is Hom, but I like Fokkinga’s much better. He uses (_⟶_) and writes (f ⟶ g) = λ h • f ⨾ h ⨾ g —the first argument of Hom is the first argument of the composition and the last argument to Hom is the last argument of the resulting composition :-)
Simplicity 𝒰nderlies complexity
‘’One way is to make it so 𝒮imple that there are obviously no deficiencies, and the other way is to make it so 𝒞omplicated that there are no obvious deficiencies. The first method is far more difficult. It demands the same skill, devotion, insight, and even inspiration as the discovery of the simple physical laws which 𝒰nderlie the complex phenomena of nature.’’ —C.A.R. Hoare
In this section we discuss what it means to be a ‘forgetful functor’?
The modifier ‘forgetful’ is meaningful when there’s a notion of extra structure. Indeed any functor F : 𝒞 ⟶ 𝒮 can be thought of as forgetful by construing the objects of 𝒞 as objects of 𝒮 with extra structure.
Being forgetful: from injections to faithful functors
A common example from set theory is the ‘inclusion’ of a subset A of B, the injection ι : A ↪ B : a ↦ a —it is essentially a form of ‘type casting’: a ∈ A and ι a = a ∈ B. Such injections ‘forget’ the property that the argument is actually a member of a specified subset. Indeed, construing sets as categories then functions becomes functors and inclusions are then forgetful functors!
Since a functor consists of two maps and some properties, we can speak about properties of the functor and about properties of either of its maps. The common definitions are a functor F is faithful if its operation on morphisms is injective, and it isfullif morphisms starting and ending atFare a result∀ x,y ∶ Obj • ∀ g ∶ F₀ x ⟶ F₀ y • ∃ f ∶ x ⟶ y • F₁ f = g`.
Now we can generalize the previous example. Every faithful functor F : 𝒞 ⟶ 𝒟 can be construed as forgetful: the 𝒞-maps can be embedded into the 𝒟-maps, since F is faithful, and so can be thought of as a special sub-collection of the 𝒟-maps; then F ‘forgets’ the property of being in this special sub-collection.
Are faithful functors in abundance? Well any functor forgetting only axioms (and/or structure) is faithful:
suppose 𝒞 consists of 𝒟 objects satisfying some axioms and 𝒟 maps preserving this structure: that is, pairs of an object/morphism with a proof that it satisfies the axioms/preserves-structure. Then F : 𝒞 ⟶ 𝒟 forgets only axioms means F (f, proof) = f. Now given, F (f , prf) = F (g , prf) ⇔ f ≡ g ⇔ (f , prf) = (g , prf) – equality does not (extensionally) depend on proof components. Hence, faithful :-)
(Likewise for forgetting extra structure).
Of course we’re not saying all forgetful functors are necessarily faithful. A simple counterexample is the absolute value function: given a real number x it’s absolute value ∣x∣ is obtained by totally ignoring its sign —of course x and ∣x∣ are equidistant from the 0 and equidistant-from-0 is an equivalence relation and so the the two are isomorphic in some sense.
Motivated by this, given a set S it’s size is denoted ∣ S ∣ which totally forgets about the elements of the set —of course it can be shown that two sets are isomorphic precisely if they are equinumerous.
I assume it is with these as motivators, some people write ∣·∣ for a forgetful functor.
Of basis vectors
If you’ve ever studied abstract algebra —the math with vector spaces— then you may recall that a collection of vectors B is called a ‘basis’ if every vector can be written as a linear combination of these vectors: for any vector v, there are scalars c₁, …, cₙ and vectors b₁, …, bₙ in B with v = c₁·b₁ + ⋯ + cₙ·bₙ. That is, a basis is a collection of ‘building blocks’ for the vector space. Then any function f between basis sets immediately lifts to a linear transformation (think vector space morphism) F as follows: given a vector v, since we have a basis, we can express it as c₁·b₁ + ⋯ + cₙ·bₙ, now define F v ≔ c₁·(f b₁) + ⋯ + cₙ·(f bₙ). Sweet! To define a complicated linear transformation of vector spaces, it more than suffices to define a plain old simple function of basis sets. Moreover, by definition, such F maps basis vectors to basis vectors: f = ι ⨾ F where ι : B ↪ V is the inclusion that realises basis vectors as just usual vectors in the vector space. Slogan: vector space maps are determined by where they send their basis, and basis-vectors are preserved.
In the case of (List A, ++, []) we may consider A to be a ‘basis’ of the monoid —indeed, every list can be written as a linear combination of elements of A, given list [x₁, …, xₙ] : List A we have [x₁, …, xₙ] = x₁ + ⋯ + xₙ where x + y ≔ [x] ++ [y]. As similar reasoning as above, or if you have familarity with foldr/reduce, we have a slogan: monoid homomorphisms from lists are determined by where they send their basis and basis-vectors are preserved.
Now the general case, suppose F ⊣ U is a free-forgetful adjunction with U : 𝒞 ⟶ 𝒮; that is, given a simple-object S there’s simple-map ι : S ⟶ U(F S) —a way to realise ‘basis vectors’— such that for any complicated-object C and simple-maps φ : S ⟶ U C, there is a unique complicated-map Φ : F S ⟶ C that preserves the basis vectors: φ = ι ⨾ U Φ. By analogy to the previous two cases, we may consdier U X to be a ‘basis’, and make the slogan: complicated-maps from free objects are determined by where they send their basis and ‘basis vectors’ are preserved.
[
In more categorical lingo, one says ι is the ‘insertion of generators’.
Question: does the way we took ι in the previous graph show that it is a natural transformation ι : Id ⟶ F ⨾ U ? —the naturality just says that a ‘homomorphism’ F f on the free object is completely detemined by what f does to the generators.
]
Of adjunctions
An adjunction L ⊣ U, where the Lower adjoint is from 𝒮 to 𝒞 and the Upper adjoint is in the opposite direction, lends itself to an elemntary interpretation if we consider 𝒞 to be some universe of 𝒞omplicated items of study, while 𝒮 to be a universe of 𝒮imple items of study. Then adjointness implies that given a simple-object S and a complicated-object C, a simple-map X ⟶ U C corresponds to a complicated-map L S ⟶ C. To work with complicated-maps it is more than enough to work with simple-maps!
now we say F : 𝒞 ⟶ 𝒟 is adjoint to G : 𝒟 ⟶ 𝒞, written F ⊣ G, iff (F ∘ X ⟶₁ Y) ≅ (X ⟶₁ G ∘ Y) (in FUNC)
_⊣₀_ : ∀ {i j} {𝒞 𝒟 : Category {i} {j}} → Functor 𝒞 𝒟 → Functor 𝒟 𝒞 → Set (i ⊍ j)
_⊣₀_ {𝒞 = 𝒞} {𝒟} F G =
(F ′ ∘ X ⟶ₙₐₜ Y) ≅ (X ⟶ₙₐₜ G ∘ Y) within Func (𝒞 ᵒᵖ ⊗ 𝒟) 𝒮e𝓉
where
X = Fst ; Y = Snd ; _′ = opify -- only changes types
infix 5 _⟶ₙₐₜ_
_⟶ₙₐₜ_ : ∀ {i j} {𝒜 : Category {i} {j}} →
Functor (𝒞 ᵒᵖ ⊗ 𝒟) (𝒜 ᵒᵖ) → Functor (𝒞 ᵒᵖ ⊗ 𝒟) 𝒜 → Functor (𝒞 ᵒᵖ ⊗ 𝒟) 𝒮e𝓉
_⟶ₙₐₜ_ = λ {i j 𝒜} → pointwise (Hom {i} {j} {𝒜})Note that if we use the built-in rewrite mechanism by adding {𝒞 𝒟 : Category {ℓ₀} {ℓ₀}} → Functor (𝒞 ᵒᵖ) (𝒟 ᵒᵖ) ≡ Functor 𝒞 𝒟 as a rewrite rule, then might can get away without using opify.
We want to say for any objects X, Y, the collection of morphisms (F A ⟶ B) is isomorphic to the collection (A ⟶ G B) and naturally so in A and B.
Unfolding it, we have
record _⊣_ {i j i' j'} {𝒞 : Category {i} {j}} {𝒟 : Category {i'} {j'}} (F : Functor 𝒞 𝒟) (G : Functor 𝒟 𝒞)
: Set (j' ⊍ i' ⊍ j ⊍ i) where
field
⌊_⌋ : ∀ {X Y} → obj F X ⟶ Y → X ⟶ obj G Y -- left-adjunct , `L ≈ ⌊`
⌈_⌉ : ∀ {X Y} → X ⟶ obj G Y → obj F X ⟶ Y -- right-adjunct, `r ≈ ⌈`
lid : ∀ {X Y} {d : obj F X ⟶ Y} → ⌈ ⌊ d ⌋ ⌉ ≡ d
rid : ∀ {X Y} {c : X ⟶ obj G Y} → ⌊ ⌈ c ⌉ ⌋ ≡ c
lfusion : ∀ {A B C D} {f : A ⟶ B} {ψ : obj F B ⟶ C} {g : C ⟶ D}
→ ⌊ mor F f ⨾ ψ ⨾ g ⌋ ≡ f ⨾ ⌊ ψ ⌋ ⨾ mor G g
rfusion : ∀ {A B C D} {f : A ⟶ B} {ψ : B ⟶ obj G C} {g : C ⟶ D}
→ ⌈ f ⨾ ψ ⨾ mor G g ⌉ ≡ mor F f ⨾ ⌈ ψ ⌉ ⨾ gThis is easier for verifying an adjunction, while the former is easier for remembering and understanding what an adjunction actually it.
Hom : {𝒞 : Category {ℓ₀} {ℓ₀} } → Functor (𝒞 ᵒᵖ ⊗ 𝒞) 𝒮e𝓉
Y : ∀ {𝒞 𝒟} → Functor (𝒞 ⊗ 𝒟) 𝒟
X : ∀ {𝒞 𝒟} → Functor (𝒞 ⊗ 𝒟) 𝒞
pointwise : ∀ {𝒞 𝒳 𝒴 : Category {ℓ₀} {ℓ₀}} {i j} {𝒟 : Category {i} {j}}
(_⊕_ : Functor (𝒳 ⊗ 𝒴) 𝒟) (F : Functor 𝒞 𝒳) (G : Functor 𝒞 𝒴) → Functor 𝒞 𝒟
Hom {𝒜} : 𝒜 ᵒᵖ ⊗ 𝒜 ⟶ 𝒮e𝓉
F : 𝒞 ᵒᵖ ⟶ 𝒟
X : 𝒞 ᵒᵖ × 𝒟 ⟶ 𝒞 ᵒᵖ
X ⨾ F : 𝒞 ᵒᵖ × 𝒟 ⟶ 𝒟
Y : 𝒞 ᵒᵖ × 𝒟 ⟶ 𝒟As the slogan goes ‘adjunctions are everywhere’. They can be said to capture the notions of optimization and efficiency, but also that of simplicity.
For example, the supremum of a function is defined to be an upper bound of its image set and the least such bound. Formally, this definition carries a few quantifiers and so a bit length. More elegantly, we can say the supremum operation is left-adjoint to the constant function: sup ⊣ K which means ∀ z • sup f ≤ z ⇔ f ≤ K z where K x y = x and the ≤ on the right is point-wise. This formulation of supremum is not only shorter to write but easier to use in calculational proofs.
For the efficiency bit, recall that it is efficient to specify a 𝒮imple-map, then use the adjuction, to obtain a 𝒞omplicated-map. Recall in the last paragraph how we define the super complicated notion of supremum of a function in terms of the most elementary constant function!
Adjunctions over poset categories are called ‘Galois connections’ and a good wealth of material on them can be found in nearly any writing by Backhouse et al, while a very accessible introduction is by Aarts, and there is also an Agda mechanisation by Kahl et al.
Regarding forgetful functors: generally, but not always, forgetful functors are faithful and have left adjoints —because the notion of ‘forget’ ought to have a corresponding notion of ‘free’. An exception to this is the category of fields, which has a forgetful functor to the category of sets with no left adjoint. [Source: wikipedia]
adjunction examples
Another awesome thing about adjunctions L ⊣ U is that they give us ‘representable functors’, aka ‘the best kind of functors’, when terminal objects exist. An object 𝟙 is ‘terminal’ if for any object A there is a unique morphism ! {A} : A ⟶ 𝟙. In 𝒮e𝓉 we have (A ⟶ 𝟙) ≅ 𝟙 and (𝟙 ⟶ A) ≅ A. Specializing the adjunction, where U : 𝒞 ⟶ 𝒮e𝓉, to a given set A and 𝟙 we obtain (L 𝟙 ⟶ A) ≅ (𝟙 ⟶ U A) ≅ U A and so one says ‘U is represented by L 𝟙’. In particular, if 𝒞 is built on 𝒮e𝓉 by adding some structure and we are interested in the utilising the elements of an object A then it suffices to utilise the maps L 𝟙 ⟶ A.
In the case of a free-forgetful adjunction, this says that a forgetful functor is represented by the free object with generator 𝟙.
For example, for monoids we have 𝟙 ≔ ({*}, ⊕, *), x ⊕ y ≔ ⋆ is the one-point monoid. Then every monoi-homomorpgism from 𝟙 just picks out an element of the carrier of a monoid and so (𝟙 ⟶ M) ≅ 𝒰 M where 𝒰 is the forgetful functors for monoids mentioned in the introduction.
Concluding remarks
A final note about free objects —arising from an adjoint to a forgetful functor.
‘’The free object is generic’’: the only truths provable for the free object are precisely those that hold for every complicated-object.
(Begin squinting eyes)
This follows from the definition of adjunction which says we can construct a unique morphism between complicated-objects from a simple-map and by naturality we may transport any proof for the free object to any complicated object.
(Feel ‘free’ to stop squinting your eyes)
For futher reading consider reading the adjoint article at the combic book library and for more on the adjective forgetful see ncatlab or mathworld A nice list of common free objects can be found here.
⟦ Challenge; true or false: for forgetful U : 𝒞 ⟶ 𝒮e𝓉 a free functor exists when 𝒞 is a monad over 𝒮e𝓉? ⟧
You might be asking, ‘musa, when am I ever going to encounter this in daily life? In a popular setting?’ This concept is everywhere, even inclusions as mentioned earlier are an instance. For the second question, enjoy this lovely group –they use the words ‘forgetful functors’ ;)
The remainder of this document can be seen as one fully-worked out example of constructing a free functor for the forgetful 𝒰 defined above.
Path definition
We can now define a ‘path’ of length n of a graph G to be a graph-map [ n ] ⟶ G.
Path₀ : ℕ → Graph₀ → Set (ℓsuc ℓ₀)
Path₀ n G = [ n ]₀ 𝒢⟶₀ GUnfolding the definition of graph-morphisms, this just says that a path of length n BACKEND-ERROR BACKEND-ERROR
The definition is pretty slick! However, as the name suggests, perhaps we can concatenate paths and it’s not at all clear how to do this for the vertex- and edge- morphisms of the graph-maps involved, whereas it’s immediately clear how to do this with sequences: we just concatenate the sequences and ensure the result is coherent.
Since the vertices can be obtained from the edges via src and tgt, we can dispense with them and use the definition as outlined above by
open import Data.Vec using (Vec ; lookup)
record Path₁ (n : ℕ) (G : Graph₀) : Set (ℓsuc ℓ₀) where
open Graph₀
field
edges : Vec (E G) (suc n)
coherency : {i : Fin n} → tgt G (lookup (' i) edges) ≡ src G (lookup (fsuc i) edges)That is, edges BACKEND-ERROR
Great, we’ve cut the definition of Path₀ in half but that fact that we get a raw list of edges and then need coherency to ensure that it is a well-formed path is still not terribly lovely. After all, we’re in Agda, we’re among kings, we should be able to form the list in such a way that the end result is a path. Let’s do that!
Enough of this repetition, let us fix a graph G,
module Path-definition-2 (G : Graph₀) where
open Graph₀ G
mutual
data Path₂ : Set where
_! : V → Path₂
cons : (v : V) (e : E) (ps : Path₂) (s : v ≡ src e) (t : tgt e ≡ head₂ ps) → Path₂
head₂ : Path₂ → V
head₂ (v !) = v
head₂ (cons v e p s t) = vDefining paths for the parallel-pair approach to graphs leaves us with the need to carry proofs around, and this is a tad too clunky in this case.
module Path-definition-3 (G : Graph) where
open Graph G
-- handy dandy syntax
infixr 5 cons
syntax cons v ps e = v ⟶[ e ]⟶ ps -- v goes, by e, onto path ps
-- we want well-formed paths
mutual
data Path₃ : Set where
_! : (v : V) → Path₃
cons : (v : V) (ps : Path₃) (e : v ⟶ head₃ ps) → Path₃
head₃ : Path₃ → V
head₃ (v !) = v
head₃ (v ⟶[ e ]⟶ ps) = v
-- motivation for the syntax declaration above
example : (v₁ v₂ v₃ : V) (e₁ : v₁ ⟶ v₂) (e₂ : v₂ ⟶ v₃) → Path₃
example v₁ v₂ v₃ e₁ e₂ = v₁ ⟶[ e₁ ]⟶ v₂ ⟶[ e₂ ]⟶ v₃ !
end₃ : Path₃ → V
end₃ (v !) = v
end₃ (v ⟶[ e ]⟶ ps) = end₃ ps
-- typed paths
field
path : Path₃
start : head₃ path ≡ x
finish : end₃ path ≡ yThis seems great, but there’s always room for improvement:
- since the
consconstructors third argument depends on its first, we must use a syntax declaration to get the desired look. Such atheistic is not only pleasing but reminiscent of diagrammatic paths; moreover, it’s guaranteed to be an actual path and not just an alternating lists of vertices and edges. Using the clunkyPath₂, we’d writeagda v₁ ⟶[ v₁≈se₁ , e₁ , te₁≈v₂ ]⟶ v₂ ⟶[ v₂≈se₂ , e₂ , te₂≈v₃ ]⟶ v₃ ! where syntax cons v e ps s t = v ⟶[ s , e , t ]⟶ psyuck!
Finally, the syntax-declaration does not make the emacs agda-mode auto-case using the syntax, and so I have to write it out by hand, each time I want to use the syntax.
Again since
consthird argument depends on the second argument, we need a mutual definition to extract the item of the dependence. Perhaps if we embed this item at the type level we may avoid the need of an auxiliary mutually-defined function.By defining what the start and finish of a path, we can assign types to it. However, this approach is reminiscent of the parallel-pair approach to graphs, as in
Graph₀, which we argued is less preferable to the typed-approach to graphs. Perhaps defining paths with types by default, we can reap the benefits and simplicity of the typed-approach to graphs. ```agda module TypedPaths (G : Graph) where
open Graph G hiding(V) open Graph using (V)
data ⇝ : V G → V G → Set where ! : ∀ x → x ⇝ x ⟶[_]⟶_ : ∀ x {y ω} (e : x ⟶ y) (ps : y ⇝ ω) → x ⇝ ω ```
Show that graphmaps preserve paths: (f : G ⟶ H) → x ⇝ y → fᵥ x ⇝ fᵥ y; this is nothing more than type-preservation for f to be a functor 𝒫G ⟶ 𝒫H ;)
a connected b ≡ (a ⇝ b) ⊎ (b ⇝ a) -- path between a and b; not 'from a to b'.this is an equivalence relation whose equivelnce classes are called the connected components. Call this collection 𝒦G. For any category 𝒞, define 𝒦 𝒞 ≔ 𝒦 (𝒰₀ 𝒞) which is a subcategory of 𝒞. Phrase the connected components subcategory using a universal property, thereby avoiding the need for quotient types.
Since graphmaps preserve paths, every graph map can be extended to connected components, 𝒦f : 𝒦G ⟶ 𝒦H : (connected componenet of x) ↦ (connected comopnent of fᵥ x).
Hence, we have a functor 𝒦 : Graph ⟶ Set.
Then there is a natural transformation 𝒱 ⟶ 𝒦, where V is the vertices functor.
Proof.
Such a transformation means we can realise vertices as connected components and this suggests taking βG : 𝒱G → 𝒦G which takes a vertix to the connected-component βlock that contains it. Then given graph map f : G ⟶ H,
𝒱 f ⨾ βG
≡ λ a → the block containing fᵥ a
≡ λ a → 𝒦f (the block containg a)
≡ βH ⨾ 𝒦fyeah!
Moreover, if we let 𝒟 : Set → Cat be the free category functor that associates each set with the discrete category over it, then we have 𝒦 is the assoicated forgetful functor.
Proof.
given a set map f : S ⟶ 𝒦 C, this assigns a connected component for each s of S. Let R c be a choice of Representative for an equivalence block, then f can be made iinto a functor by sending each s, now construed as an object, to the C-object R (f s).
given a functor F : 𝒟 S ⟶ C, define a set-map that sends each s to the connected component that contains it, ie β.
now verify the needed laws.
I saw this someplace on stack exchange for the adjoint to the free category functor. Anyhow, should consider the intution(?) behind this construction since it’s not immediately clear why the connected components, that or cuz is nearly 6 in the morning and i am needs of sleep.
One might think that since we can write
src : {x y : V G} (e : x ⟶ y) → V G
src {x} {y} e = xwe can again ignore vertices and it suffices to just keep a coherent list of edges. Then what is an empty path at a vertex? This’ enough to keep vertices around —moreover, the ensuing terms look like diagrammatic paths! Cool!
One more thing, a handy-dandy combinator for forming certain equality proofs of paths.
⟶-≡ : ∀{x y ω} {e : x ⟶ y} {ps qs : y ⇝ ω} → ps ≡ qs → (x ⟶[ e ]⟶ ps) ≡ (x ⟶[ e ]⟶ qs)
⟶-≡ {x} {y} {ω} {e} {ps} {qs} eq = ≡-cong (λ r → x ⟶[ e ]⟶ r) eqLess usefully, we leave as excercises
edges : ∀ {x ω} (p : x ⇝ ω) → List (Σ s ∶ V G • Σ t ∶ V G • s ⟶ t)
edges = {! exercise !}
path-eq : ∀ {x y} {p q : x ⇝ y} → edges p ≡ edges q → p ≡ q
path-eq = {! exercise !}Given time, path-eq could be rewritten so as to be more easily applicable. For now, two path equality proofs occur in the document and both are realised by quick-and-easy induction.
category of paths over a graph
Now we turn back to the problem of concatenating two paths.
infixr 5 _++_
_++_ : ∀{x y z} → x ⇝ y → y ⇝ z → x ⇝ z
x ! ++ q = q -- left unit
(x ⟶[ e ]⟶ p) ++ q = x ⟶[ e ]⟶ (p ++ q) -- mutual-associativityNotice that the the base case indicate that ! forms a left-unit for ++, while the inductive case says that path-formation associates with path concatenation.
If we had not typed our paths, as in Path₂, we would need to carry around a proof that paths are compatible for concatenation:
concatenate : (p q : Path) (coh : end p ≡ head q) → Path
syntax concatenate p q compatibility = p ++[ compatibility ] qEven worse, to show p ++[ c ] q ≡ p ++[ c' ] q we need to invoke proof-irrelevance of identity proofs to obtain c ≡ c', each time we want such an equality! Moving the proof obligation to the type level removes this need.
As can be seen, being type-less is a terrible ordeal.
Just as the first clause of CONCAT AND BANG
leftId : ∀ {x y} {p : x ⇝ y} → x ! ++ p ≡ p
leftId = ≡-reflIs it also a right identity?
rightId : ∀ {x y} {p : x ⇝ y} → p ++ y ! ≡ p
rightId {x} {.x} {.x !} = ≡-refl
rightId {x} {y } {.x ⟶[ e ]⟶ ps} = ≡-cong (λ q → x ⟶[ e ]⟶ q) rightIdIs this operation associative?
assoc : ∀{x y z ω} {p : x ⇝ y} {q : y ⇝ z} {r : z ⇝ ω} → (p ++ q) ++ r ≡ p ++ (q ++ r)
assoc {x} {p = .x !} = ≡-refl
assoc {x} {p = .x ⟶[ e ]⟶ ps} {q} {r} = ≡-cong (λ s → x ⟶[ e ]⟶ s) (assoc {p = ps})Hence, we’ve shown that the paths over a graph constitute a category! Let’s call it 𝒫 G.
The 𝒫ath to freedom
In the last section, we showed that the paths over a graph make a category,
𝒫₀ : Graph → Category
𝒫₀ G = let open TypedPaths G in
record
{ Obj = Graph.V G
; _⟶_ = _⇝_
; _⨾_ = _++_
; assoc = λ {x y z ω p q r} → assoc {p = p}
; Id = λ {x} → x !
; leftId = leftId
; rightId = rightId
}Can we make 𝒫 into a functor by definining on morphisms? That is, to lift graph-maps to category-maps, i.e., functors.
𝒫₁ : ∀{G H} → GraphMap G H → Functor (𝒫₀ G) (𝒫₀ H)
𝒫₁ {G} {H} f = record { obj = ver f ; mor = mo ; id = ≡-refl ; comp = λ {x} {y} {z} {p} → comp {p = p} }
where
open TypedPaths {{...}} public
mo : {x y : Graph.V G} → x ⇝ y → (ver f x) ⇝ (ver f y)
mo (x !) = ver f x !
mo (x ⟶[ e ]⟶ p) = ver f x ⟶[ edge f e ]⟶ mo p
comp : {x y z : Graph.V G} {p : x ⇝ y} {q : y ⇝ z} → mo (p ++ q) ≡ mo p ++ mo q
comp {x} {p = .x !} = ≡-refl -- since ! is left unit of ++
comp {x} {p = .x ⟶[ e ]⟶ ps} = ⟶-≡ (comp {p = ps})Sweet!
With these two together, we have that 𝒫 is a functor.
𝒫 : Functor 𝒢𝓇𝒶𝓅𝒽 𝒞𝒶𝓉
𝒫 = record { obj = 𝒫₀ ; mor = 𝒫₁ ; id = λ {G} → funcext ≡-refl (idm {G}) ; comp = funcext ≡-refl compmor }
where
open TypedPaths {{...}} public
idm : ∀ {G} {x y} {p : x ⇝ y} → mor (Category.Id 𝒞𝒶𝓉 {𝒫₀ G}) p ≡ mor (𝒫₁ (Category.Id 𝒢𝓇𝒶𝓅𝒽)) p
idm {G} {x} {p = .x !} = ≡-refl
idm {G} {x} {p = .x ⟶[ e ]⟶ ps} = ⟶-≡ (idm {p = ps})
open Category {{...}}
compmor : ∀ {G H K} {f : G ⟶ H} {g : H ⟶ K} {x y} {p : x ⇝ y} → mor (𝒫₁ f ⨾ 𝒫₁ g) p ≡ mor(𝒫₁ (f ⨾ g)) p
compmor {x = x} {p = .x !} = ≡-refl
compmor {x = x} {p = .x ⟶[ e ]⟶ ps} = ⟶-≡ (compmor {p = ps})Free at last
⟦ ‘’Free at last, free at last, thank God almighty we are free at last.’’ – Martin Luther King Jr.
⟧
Recall why lists give the ‘free monoid’: we can embed a type A into List A by the map BACKEND-ERROR and we can lift any map f : A ⟶ B to a monoid map BACKEND-ERROR —i.e., [a₁, …, aₖ] ↦ f a₁ ⊕ ⋯ ⊕ f aₖ— such that ∀ a • f a ≡ foldr f e [ a ] and this lifted map is unique.
Likewise, let us show that 𝒫G is the ‘free category’ over the graph G. This amounts to saying that there is a way, say graph-map ι, to embed G into 𝒫G, and a way to lift any graph-map f : G 𝒢⟶ 𝒰₀ 𝒞 to a functor lift f : Functor 𝒫G 𝒞 such that f ≡ ι ⨾ 𝒰₁ (lift f) and uniquely so.
Let’s begin!
module freedom (G : Obj 𝒢𝓇𝒶𝓅𝒽) {𝒞 : Category {ℓ₀} {ℓ₀} } where
open TypedPaths G using (_! ; _⟶[_]⟶_ ; _⇝_ ; _++_)
open Category {{...}}Defining the needed operations
The only obvious, and most natural, way to embed a graph into its ‘graph of paths’ is to send vertices to vertices and edges to paths of length 1.
ι : G ⟶ 𝒰₀ (𝒫₀ G)
ι = record { ver = Id ; edge = λ {x} {y} e → x ⟶[ e ]⟶ y ! }Given a graph map f, following the list-analagoue of [a₁, …, aₖ] ↦ f a₁ ⊕ ⋯ ⊕ f aₖ we attempt to lift the map onto paths by taking edges e₁, …, eₖ to a morphism e₁' ⨾ ⋯ ⨾ eₖ' where eᵢ' = edge f eᵢ. Of course, we then need to verify that this construction is indeed functorial.
lift : G ⟶ 𝒰₀ 𝒞 → 𝒫₀ G ⟶ 𝒞
lift f = record {
obj = λ v → ver f v -- this is the only way to obtain an object of `𝒞`; hope it works!
; mor = toMap ; id = ≡-refl ; comp = λ {x y z p q} → proof {x} {y} {z} {p} {q}
}
where
toMap : ∀ {x y} → x ⇝ y → ver f x ⟶ ver f y
toMap (y !) = Id
toMap (x ⟶[ e ]⟶ p) = edge f e ⨾ toMap p
proof : ∀{x y z} {p : x ⇝ y} {q : y ⇝ z} → toMap (p ++ q) ≡ toMap p ⨾ toMap q
proof {p = ._ !} = ≡-sym leftId
proof {p = ._ ⟶[ e ]⟶ ps} = ≡-cong (λ m → edge f e ⨾ m) (proof {p = ps}) ⟨≡≡⟩ ≡-sym assocNow we have the embedding and the lifting, it remains to show that the aforementioned property holds and so does uniqueness.
Realizing the proof-obligations
property : ∀{f : G ⟶ 𝒰₀ 𝒞} → f ≡ (ι ⨾ 𝒰₁ (lift f))
property {f} = graphmapext
-- proving `∀ {v} → ver f v ≡ ver (ι ⨾ 𝒰₁ (lift f)) v` by starting at the complicated side and simplifying
(λ {v} → ≡-sym (begin
ver (ι ⨾ 𝒰₁ (lift f)) v
≡⟨ definition {- of `ver` on composition -}⟩
(ver ι ⨾ ver (𝒰₁ (lift f))) v
≡⟨ definition {- of `𝒰₁` says `ver (𝒰₁ F) = obj F` -}⟩
(ver ι ⨾ obj (lift f)) v
≡⟨ definition {- of `lift` says `obj (lift f) = ver f` -}⟩
(ver ι ⨾ ver f) v
≡⟨ definition {- of `ι` on vertices is idenity -}⟩
ver f v
∎))
-- proving `edge (ι ⨾g 𝒰₁ (lift f)) e ≡ edge f e`
(λ {x} {y} {e} → begin
edge (ι ⨾ 𝒰₁ (lift f)) e
≡⟨ definition {- of `edge` on composition -} ⟩
(edge ι ⨾ edge (𝒰₁ (lift f))) e
≡⟨ definition {- of `𝒰` says `edge (𝒰₁ F) = mor F` -} ⟩
(edge ι ⨾ mor (lift f)) e
≡⟨ definition {- chasing gives `mor (lift f) (edge ι e) = edge f e ⨾ Id` -} ⟩
edge f e ⨾ Id
≡⟨ rightId ⟩
edge f e
∎)Observe that we simply chased definitions and as such (≡-refl , rightId) suffices as a proof, but it’s not terribly clear why, for human consumption and so we choose to elaborate with the detail.
Finally, it remains to show uniqueness,
uniqueness : ∀{f : G ⟶ 𝒰₀ 𝒞} {F : 𝒫₀ G ⟶ 𝒞} → f ≡ (ι ⨾ 𝒰₁ F) → lift f ≡ F
uniqueness {.(ι ⨾ 𝒰₁ F)} {F} ≡-refl = funcext ≡-refl (≡-sym pf)
where
pf : ∀{x y} {p : x ⇝ y} → mor (lift (ι ⨾ 𝒰₁ F)) p ≡ mor F p
pf {x} {.x} {p = .x !} = ≡-sym (Functor.id F)
pf {x} {y} {p = .x ⟶[ e ]⟶ ps} = begin
mor (lift (ι ⨾ 𝒰₁ F)) (x ⟶[ e ]⟶ ps)
≡⟨ definition {- of `mor` on `lift`, the inductive clause -} ⟩
edge (ι ⨾ 𝒰₁ F) e ⨾ mor (lift (ι ⨾ 𝒰₁ F)) ps
≡⟨ ≡-cong₂ _⨾_ ≡-refl (pf {p = ps}) ⟩ -- inductive step
edge (ι ⨾ 𝒰₁ F) e ⨾ mor F ps
≡⟨ definition {- of `edge` says it preserves composition -} ⟩
(edge ι ⨾ edge (𝒰₁ F)) e ⨾ mor F ps
≡⟨ ≡-refl ⟩ {- definition of `𝒰` gives `edge (𝒰₁ F) = mor F`-}
(edge ι ⨾ mor F) e ⨾ mor F ps
≡⟨ definition {- of functional composition (`𝒮et`) -} ⟩
mor F (edge ι e) ⨾ mor F ps
≡⟨ ≡-sym (Functor.comp F) {- i.e., functors preserve composition -} ⟩
mor F (edge ι e ++ ps)
≡⟨ definition {- of embedding and concatenation -} ⟩
mor F (x ⟶[ e ]⟶ ps)
∎Another freedom proof
However, saying each graph-map gives rise to exactly one unique functor is tantamount to saying the type GraphMap G (𝒰₀ 𝒞) is isomorphic to Functor (𝒫₀ G) 𝒞, that is (𝒫₀ G ⟶ 𝒞) ≅ (G ⟶ 𝒰₀ 𝒞) —observe that this says we can ‘move’ 𝒫₀ from the left to the right of an arrow at the cost of it (and the arrow) changing.
A few healthy excercises,
lift˘ : Functor 𝒫G 𝒞 → GraphMap G (𝒰₀ 𝒞)
lift˘ F = ι ⨾g 𝒰₁ F -- i.e., `obj F , (mor F ∘ edge ι)`
rid : ∀{f : GraphMap G (𝒰₀ 𝒞)} → ∀{x y} {e : x ⟶g y} → lift˘ (lift f) ≡ f
rid = {! exercise !}
lid : ∀{F : Functor 𝒫G 𝒞} → lift (lift˘ F) ≡ F
lid = {! exercise !}One can of course obtain these proofs from the other ones without recourse to definitions, however for comprehension one would do well to prove them from first principles. The worked out solutions are available in the literate source file of this document.
We can then given an alternate proof of uniqueness ∀{f h}→ f ≡ (ι ⨾ 𝒰₁ h) → lift f ≡ h.
uniqueness' : ∀{f h}→ f ≡ (ι ⨾ 𝒰₁ h) → lift f ≡ h
uniqueness' {f} {h} f≈ι⨾𝒰₁h = begin
lift f
≡⟨ ≡-cong lift f≈ι⨾𝒰₁h ⟩
lift (ι ⨾ 𝒰₁ h)
≡⟨ definition {- of `lift˘` -} ⟩
lift (lift˘ h)
≡⟨ lid ⟩
h
∎𝒫 ⊣ 𝒰
That is, 𝒫 ⊣ 𝒰 and say 𝒫 is a ‘free-functor’ since it is left-adjoint to a forgetful-functor.
We have
lift : G ⟶ 𝒰₀ 𝒞 → 𝒫G ⟶ 𝒞
lift˘ : 𝒫G ⟶ 𝒞 → G ⟶ 𝒰₀ 𝒞and we proved them to be inverses hence (𝒫G ⟶ 𝒞) ≅ (G ⟶ 𝒰₀ 𝒞).
To realise 𝒫 ⊣ 𝒰 it remains to exhibit ‘naturality’: for every graph map g and functor F, for appropriate functor k we have lift˘ (𝒫 g ⨾ k ⨾ F) ≈ g ⨾ lift˘ k ⨾ 𝒰 F in the category of graphs.
module _ {G H : Graph} {𝒞 𝒟 : Category {ℓ₀} {ℓ₀}} (g : GraphMap G H) (F : Functor 𝒞 𝒟) where
private
lift˘ = λ {A} {C} B → freedom.lift˘ A {C} B
lift = λ {A} {C} B → freedom.lift A {C} B
open Category {{...}}
naturality˘ : ∀ {K : Functor (𝒫₀ H) 𝒞} → lift˘ (𝒫₁ g ⨾ K ⨾ F) ≡ (g ⨾ lift˘ K ⨾ 𝒰₁ F)
naturality˘ = graphmapext ≡-refl ≡-reflThat was easier than assumed! haha —much harder to formalize but so easy to prove lolz It says we can ‘shunt’ lift˘ into certain compositions at the cost of replacing functor instances.
Just we needed to prove two inverse laws for lift and lift˘, we need two naturality proofs.
naturality : ∀ {k : GraphMap H (𝒰₀ 𝒞)} → lift (g ⨾ k ⨾ 𝒰₁ F) ≡ (𝒫₁ g ⨾ lift k ⨾ F)
naturality {k} = funcext ≡-refl (λ {x y p} → proof {x} {y} {p})
where
open TypedPaths {{...}}
proof : ∀ {x y} {p : x ⇝ y} → mor (𝒫₁ g ⨾ lift {H} {𝒞} k ⨾ F) p ≡ mor (lift {G} {𝒟} (g ⨾ k ⨾ 𝒰₁ F)) p
proof {x} {p = .x !} = functors-preserve-identities
proof {x} {p = .x ⟶[ e ]⟶ ps} = begin
mor (𝒫₁ g ⨾ lift {H} {𝒞} k ⨾ F) (x ⟶[ e ]⟶ ps)
≡⟨ definition ⟩
(mor (𝒫₁ g) ⨾ mor (lift {H} {𝒞} k) ⨾ mor F) (x ⟶[ e ]⟶ ps)
≡⟨ definition {- of function composition and `𝒫₁ ⨾ mor` -} ⟩
mor F (mor (lift {H} {𝒞} k) (mor (𝒫₁ g) (x ⟶[ e ]⟶ ps)))
≡⟨ definition ⟩
mor F (mor (lift {H} {𝒞} k) (ver g x ⟶[ edge g e ]⟶ mor (𝒫₁ g) ps))
≡⟨ definition {-of `lift ⨾ mor` on inductive case for paths -} ⟩
mor F (edge k (edge g e) ⨾ mor (lift {H} {𝒞} k) (mor (𝒫₁ g) ps))
≡⟨ functors-preserve-composition ⟩
mor F (edge k (edge g e)) ⨾ mor F (mor (lift {H} {𝒞} k) (mor (𝒫₁ g) ps))
≡⟨ definition {- of function composition -} ⟩
(edge g ⨾ edge k ⨾ mor F) e ⨾ (mor (𝒫₁ g) ⨾ mor (lift {H} {𝒞} k) ⨾ mor F) ps
≡⟨ {- `𝒰₁ ⨾ edge = mor` and edge and mor are functorial by -} definition ⟩
edge (g ⨾ k ⨾ 𝒰₁ F) e ⨾ mor (𝒫₁ g ⨾ lift {H} {𝒞} k ⨾ F) ps
≡⟨ {-inductive hypothesis: -} ≡-cong₂ _⨾_ ≡-refl (proof {p = ps}) ⟩
edge (g ⨾ k ⨾ 𝒰₁ F) e ⨾ mor (lift {G} {𝒟} (g ⨾ k ⨾ 𝒰₁ F)) ps
≡⟨ definition {-of `lift ⨾ mor` on inductive case for paths -}⟩
mor (lift {G} {𝒟} (g ⨾ k ⨾ 𝒰₁ F)) (x ⟶[ e ]⟶ ps)
∎Fokkinga [Theorem A.4], among others, would call these laws ‘fusion’ instead since they inform us how to compose, or ‘fuse’, a morphism with a lift˘ed morphism: taking F to be the identity and remembering that functors preserve identities, we have that g ⨾ lift˘ K ≡ lift˘( 𝒫₁ g ⨾ K) –we can push a morphism into a lift˘ at the cost of introducing a 𝒫₁; dually for lifted morphisms.
Formally,
𝒫⊣𝒰 : 𝒫 ⊣ 𝒰
𝒫⊣𝒰 = record{
⌊_⌋ = lift˘
; ⌈_⌉ = lift
; lid = lid
; rid = λ {G 𝒞 c} → rid {G} {𝒞} {c}
; lfusion = λ {G H 𝒞 𝒟 f F K} → naturality˘ {G} {H} {𝒞} {𝒟} f K {F}
; rfusion = λ {G H 𝒞 𝒟 f k F} → naturality {G} {H} {𝒞} {𝒟} f F {k} }
where
module _ {G : Graph} {𝒞 : Category} where open freedom G {𝒞} publicfold over paths
Observe that for the freedom proof we recalled that ists determine a form of quantification, ‘folding’: given an operation ⊕, we may form [x₁, …, xₖ] ↦ x₁ ⊕ ⋯ ⊕ xₖ. Then used that to define our operation lift, whose core was essentially,
module folding (G : Graph) where
open TypedPaths G
open Graph G
fold : {X : Set} (v : V → X) (f : ∀ x {y} (e : x ⟶ y) → X → X) → (∀ {a b} → a ⇝ b → X)
fold v f (b !) = v b
fold v f (x ⟶[ e ]⟶ ps) = f x e (fold v f ps) For example, what is the length of a path?
length : ∀{x y} → x ⇝ y → ℕ
length = fold (λ _ → 0) -- single walks are length 0
(λ _ _ n → 1 + n) -- edges are one more than the length of the remaining walkLet’s verify that this is actually what we intend by the length of a path.
length-! : ∀{x} → length (x !) ≡ 0
length-! = ≡-refl -- true by definition of `length`: the first argument to the `fold`
length-ind : ∀ {x y ω} {e : x ⟶ y} {ps : y ⇝ ω} → length (x ⟶[ e ]⟶ ps) ≡ 1 + length ps
length-ind = ≡-refl -- true by definition of `length`: the second-argument to the `fold`Generalzing on length, suppose we have a ‘cost function’ c that assigns a cost of traversing an edge. Then we can ask what is the total cost of a path:
path-cost : (c : ∀{x y}(e : x ⟶ y) → ℕ) → ∀{x y}(ps : x ⇝ y) → ℕ
path-cost c = fold (λ _ → 0) -- no cost on an empty path
(λ x e n → c e + n) -- cost of current edge plus cost of remainder of pathNow, we have BACKEND-ERROR
Under suitable conditions, list fold distributes over list concatenation, can we find an analogue for paths?
fold-++ : ∀{X : Set} {v : V → X} {g : ∀ x {y} (e : x ⟶ y) → X}
→ (_⊕_ : X → X → X)
→ ∀{x y z : V} {p : x ⇝ y} {q : y ⇝ z}
→ (unitl : ∀{x y} → y ≡ v x ⊕ y) -- image of `v` is left unit of `⊕`
→ (assoc : ∀ {x y z} → x ⊕ (y ⊕ z) ≡ (x ⊕ y) ⊕ z ) -- `⊕` is associative
→ let f : ∀ x {y} (e : x ⟶ y) → X → X
f = λ x e ps → g x e ⊕ ps
in
fold v f (p ++ q) ≡ fold v f p ⊕ fold v f q
fold-++ {g = g} _⊕_ {x = x} {p = .x !} unitl assoc = unitl
fold-++ {g = g} _⊕_ {x = x} {p = .x ⟶[ e ]⟶ ps} unitl assoc =
≡-cong (λ exp → g x e ⊕ exp) (fold-++ _⊕_ {p = ps} unitl assoc) ⟨≡≡⟩ assocCompare this with the proof-obligation of lift.
Lists are special kinds of paths
We called our path concatenation BACKEND-ERROR
How do we interpret a list over A as graph? Well the vertices can be any element of A and an edge x ⟶ y merely indicates that ‘’the item after x in the list is the element y’’, so we want it to be always true; or always inhabited without distinction of the inhabitant: so use a unit type.
module lists (A : Set) where
open import Data.Unit
listGraph : Graph
listGraph = record { V = A ; _⟶_ = λ a a' → ⊤ }I haven’t a clue if this works, you read my reasoning above.
The only thing we can do is test our hypothesis by looking at the typed paths over this graph. In particular, we attempt to show every non-empty list of A’s corresponds to a path. Since a typed path needs a priori the start and end vertes, let us construe List A ≅ Σ n ∶ ℕ • Fin n → A –later note that Path G ≅ Σ n ∶ ℕ • [n] 𝒢⟶ G–.
open TypedPaths listGraph
open folding listGraph
-- every non-empty list of 'A's corresonds to a path!
toPath : ∀{n} (list : Fin (suc n) → A) → list fzero ⇝ list ( fromℕ n )
toPath {zero} list = list fzero !
toPath {suc n} list = list fzero ⟶[ tt ]⟶ toPath {n} (λ i → list(fsuc i))
-- note that `list : Fin (suc (suc n)) → A` while `suc ⨾ list : Fin (suc n) → A`
-- if ` list ≈ [x , y , z] ` then
-- `fsuc ⨾ list ≈ [y , z ] `
-- `fsuc ⨾ fsuc ⨾ list = [z] `Hm! Look at that, first guess and it worked! Sweet.
Now let’s realize the list fold as an instance of path fold,
-- list type former
List = λ (X : Set) → Σ n ∶ ℕ • (Fin n → X)
-- usual list folding
foldr : ∀{B : Set} (f : A → B → B) (e : B) → List A → B
foldr f e (zero , l) = e
foldr f e (suc n , l) = fold (λ a → f a e) (λ a _ rem → f a rem) (toPath l)
-- example
listLength : List A → ℕ -- result should clearly be `proj₁` of the list, anyhow:
listLength = foldr (λ a rem → 1 + rem) -- non-empty list has length 1 more than the remainder
0 -- empty list has length 0
-- let's prepare for a more useful example
-- empty list
[] : ∀{X : Set} → List X
[] = 0 , λ ()
-- cons for lists
_∷_ : ∀{X : Set} → X → List X → List X
_∷_ {X} x (n , l) = 1 + n , cons x l
where
-- `cons a l ≡ λ i : Fin (1 + n) → if i ≈ 0 then a else l i`
cons : ∀{n} → X → (Fin n → X) → (Fin (suc n) → X)
cons x l fzero = x
cons x l (fsuc i) = l i
map : ∀ {B} (f : A → B) → List A → List B
map f = foldr (λ a rem → f a ∷ rem) [] -- looks like the usual map don't it ;)
-- list concatenation
_++ℓ_ : List A → List A → List A
l ++ℓ r = foldr _∷_ r l -- fold over `l` by cons its elements infront of `r`
-- Exercise: write path concatenation as a path-fold.This note took longer to write than I had initally assumed; perhaps I should have taken into account Hofstadter’s Law, which says: “It always takes longer than you expect, even when you take into account Hofstadter’s Law.”.
[insert url to GEB]
old imports
open import Data.Empty using (⊥-elim)
open import Relation.Nullary
open import Data.Nat.Properties using (≰⇒> ; <-trans ; m≤m+n ; _+-mono_ ; ≤-step ; ≤⇒pred≤)
open import Relation.Binary.PropositionalEquality.Core using () renaming (subst to ≡-subst)
open import Data.Nat.Properties.Simple using (+-comm ; +-right-identity ; +-suc)
open import Data.Fin.Properties using (bounded ; toℕ-fromℕ≤ ; inject≤-lemma)Can we turn any relation into a category? Well we know that preorder relations yield categories, so let’s consider transforming arbitrary relations to preorders.
Suppose we have a relation R : X → X → Set and we want it to be a preorder such as ≤ : ℕ → ℕ → Set. Then we need it to be reflexive and transitivie; that is, ∀ x ∶ X • R x x, ∀ x y ∶ X • R x y → R y x, and ∀ x y z ∶ X • R x y → R y z → R x z are provable, respectively.
(As it stands, this relation is precicely a graph! If we want a relation in the traditional sense of ordered pairs, then we want a simple-graph.
simple : ∀ {x y} (p q : R x y) → p ≡ q -- at most one edge between any two pair)
[[
above when defined poset category, or rather after hom is defined,
mention how intervals a..b are realised in the cat, say via hom??
]]
Then, ≤R is a total order.
data _≤R : X → X → Set where
embed : ∀ {x y} → R x y → x ≤R y -- existing edges
refl : ∀ {x} → x ≤R x -- empty path
trans : ∀ {x y z} → x ≤R y → y ≤R z → x ≤R z -- path concatenationObserve that embed says that the order ≤R contains R.
(≤R is also known as the “reachiability poset of R” ??)
Usual definition is ≤R ≔ R* = λ x y → Σ n ∶ ℕ • Rⁿ x y where R⁰ x y = (x ≡ y) and Rⁿ⁺¹ x y ≡ Σ i • R x y ∧ Rⁿ i y; the reflexive transitive closure of R. While this is more compact, the Agda version is easier to work with and it is equivalent since embed corresponds to n=1, refl corresponds to n = 0, and trans corresponds to the ‘multiplication’ operation since Rⁿ⁺¹ x y ⇔ Σ a,b ∶ ℕ • a + b ≡ n ∧ Σ i • Rᵃ x i ∧ Rᵇ i y —or so I claim!
For example, if R = { (1,2) , (3,4) } then
≤R =
{
(1,2) , (3,2), -- embed
(1,1), (2,2), (3,3), -- refl
-- trans gives no new pairs
}An example algorithm for finding the transitive closure is Warshall’s algorithm.
Notice that if R reflexive or transitive, then we do not have uniqunenss of proofs for ≤R. In particular, suppose R is reflexive and such proofs are constructed by r_. Then a proof of x ≤R x can be obtained in two ways: refl {x} or embed (r x).
Now the resulting category can be thought of as the free-category on R; what’s the associated adjunctin to this claim o mine? That is, functors from this free cat correspond to relational homomorphisms?? Consider consulting Schmidt and Strohnelin.
Is this is the least preorder relation on R?
suppose ⊑ is a reflexive relation that contains R, then
given p : x ≤R y --ignoring transitivity
there are two cases.
Case p = embed q. Then q yields a proof of x ⊑ y since ⊑ contians R and q is an R proof.
Case p = refl {x}. Then x ⊑ x holds since ⊑ is relfexive.
Hence, ≤R (ignoring transitivity) is the least reflexive relation contianing R.
Suppose ⊑ is also transitive.
Then the only remaining case is
Case p = trans q r, where q : x ≤R y, r : y ≤R z, Then by induction we have proofs
x ⊑ y ⊑ z, but ⊑ is transitive and so we have a proof of x ⊑ z.
Thus, ≤R is the least preorder containing R!! Woah! Awesome!Every preorder can be obtained as the closure of its Hasse/covers relation: ∀ R preorder • R ≅ ≤[ R ] ≅ ≤[ Covers R ] (in the category of relations and relation homomorphisms), where Covers R x y ≡ x ≠ y ∧ x R y ∧ ¬ Σ z • z ≠ x R z R y ≠ z. ?? Is this true, or do I just think it to be true…
In particular, taking R = ℙₙ, which is a hasse relation, yields the free preorder on R which is essentially the free category on the poset ≤[ R ].
Now R can be thought of as a directed graph. If we take R = { (i, i+1) ∣ i ∈ 0..n-1} then ≤R is the free graph on ℙₙ, right??
moreover it is a total order: we can show
total : ∀ {x y} → x ≤R y ⊎ y ≤R x
antisym : ∀ {x y} → x ≤R y → y ≤R x → x ≡ yAlso such categories of paths are known as simplicies??