Graphs are to categories as lists are to monoids

In our exploration of what graphs could possibly be and their relationships to lists are, we shall mechanise or implement our claims since there will be many details and it is easy to make mistakes –moreover as a self-learning project, I'd feel more confident to make bold claims when I have a proof assistant checking my work ;-)

Before reading any further please ingrain into your mind that the Agda keyword Set is read “type”! This disparity is a historical accident.

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
open import Relation.Binary using (module DecTotalOrder)
open import Data.Nat.Properties using(≤-decTotalOrder ; ≤-refl)
open DecTotalOrder Data.Nat.Properties.≤-decTotalOrder

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

module _ {i} {S : Set i} where
    open import Relation.Binary.EqReasoning (≡-setoid S) public

We intend our proofs to be sequences of formulae interleaved with justifications for how the formulae are related. At times, the justifications are by definition and so may be omitted, but we may want to mention them for presentational –pedagogical?– purposes. Hence, we introduce the combinator notation lhs ≡⟨" by definition of something "⟩′ rhs.

open import Agda.Builtin.String

defn-chasing : ∀ {i} {A : Set i} (x : A) → String → A → A
defn-chasing x reason supposedly-x-again = supposedly-x-again

syntax defn-chasing x reason xish = x ≡⟨ reason ⟩′ xish

infixl 3 defn-chasing

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 eq

Example usage would be to prove mor G (mor F Id) ≡ mor G Id directly by ≡-cong (mor G) (id F) which can be written more clearly as functor F preserves-identities even-under (mor G), while longer it is also much clearer and easier to read and understand –self-documenting in some sense.

Interestingly, our first calculational proof is in section 5 when we introduced an large 𝒞𝒶𝓉egory.

However, we must admit that a slight downside of the typed approach –the two-piece definition– is now we may need to use the following ‘shifting’ combinators: They shift, or slide, the edge types.

-- casting
_⟫_ : ∀{x y y’} →  (x ⟶ y) → (y ≡ y’) → (x ⟶ y’)
e ⟫ ≡-refl = e

-- Casting leaves the edge the same, only type information changes
≅-⟫ : ∀{x y y’} {e : x ⟶ y} (y≈y’ : y ≡ y’) → e ≅ (e ⟫ y≈y’)
≅-⟫ ≡-refl = ≅-refl

Such is the cost of using a typed-approach.

Even worse, if we use homogeneous equality then we’d have the ghastly operator

≡-⟫ : ∀{x y y’} {e : x ⟶ y} (y≈y’ : y ≡ y’) → e ⟫ y≈y’ ≡ (≡-subst (λ ω → x ⟶ ω) y≈y’ e)

However, it seems that our development does not even make use of these. Lucky us! However, it is something to be aware of.

A signature consists of ‘sort symbols’ and ‘function symbols’ each of which is associated source-sorts and a target-sort –essentially it is an interface in the programming sense of the word thereby providing a lexicon for a language. A model or algebra of a language is an interpretation of the sort symbols as sets and an interpretation of the function symbols as functions between those sets; i.e., it is an implementation in programming terms. 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 function symbols 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 signature

For example, the signature of monoids consists of a single sort symbol C –which can be interpreted 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 which 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 symbols 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 logics to also be similar. Moreover we now have a few slogans, \[\color{green}{\text{Categories are precisely typed monoids!}}\] \[\color{green}{\text{Categories are precisely graphs with a monoidal structure!}}\] \[\color{green}{\text{Categories are precisely coherently constructive lattices!}}\]

( The last one is completely unmotivated from our discussion, but it's a good place for the slogan and will be touched on when we look at examples of categories. )

A signature can be visualised in the plane by associating a dot for each sort symbol and an arrow for each function symbol 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 visualised 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 being sets and edges being functions.

Notice that a Graph₀ is precisely a model of the graph • ⇉ •, which consists of two vertices and two edges from the first vertex to the second vertex. We will return to this point ;-)

Before we move on, it is important to note that a signature does not capture any constraints required on the symbols –e.g., a monoid is the monoid signature as well as the constraint that the 2-arity operation is associative and the 0-arity operation is its unit. More generally, a specification consists of a signature declaring symbols of interest, along with a set of sentences over it that denote axioms or constraints. In programming parlance, this is an interface consisting of types and functions that need to be provided and implemented, along with constraints that are usually documented in comments. Unsurprisingly, models of specifications also form 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 E-quivalence 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 structure-preserving maps must also be congruences.

For our purposes 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, without providing any real insight for our uses, 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 develop a library for category theory, which has already been done so elegantly by Kahl who calls it the RATH-Agda project.

module _ where -- An anyonomous module for categorial 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 : Obj} {f : A ⟶ B} → Id ⨾ f ≡ f
    rightId  : ∀ {A B : Obj} {f : A ⟶ B} → f ⨾ Id ≡ f

 open Category using (Obj)
 open Category ⦃...⦄ hiding (Obj)

 -- Some sugar for times when we must specify the category
 -- “colons associate to the right” ;-)

 arr = Category._⟶_
 syntax arr 𝒞 x y  =  x ⟶ y ∶ 𝒞    -- “ghost colon”

 cmp = Category._⨾_
 syntax cmp 𝒞 f g  =  f ⨾ g ∶ 𝒞    -- “ghost colon”

However, similar to nearly everything else in this document, we can leave the setoid approach as an exercise 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 her-self, 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 interested to know that Maarten Fokkinga has written a very gentle introduction to category theory using the calculational approach; I highly recommend it!

Anyhow, in place of strict equality, one uses categorical isomorphism instead.

 open Category using (Obj) public

 record Iso {i} {j} (𝒞 : Category {i} {j}) (A B : Obj 𝒞) : Set j where
   private instance 𝒞′ : Category ; 𝒞′ = 𝒞
   field
     to   : A ⟶ B
     from : B ⟶ A
     lid  : to ⨾ from ≡ Id
     rid  : from ⨾ to ≡ Id

 syntax Iso 𝒞 A B = A ≅ B within 𝒞

Interestingly, we shall later encounter a rather large category named 𝒞𝒶𝓉 possessing the special property of being a “2-Category”: It has morphisms between objects, as expected, which are now called “1-morphisms”, and it has morphisms between 1-morphisms, also called “2-morphisms”.

That is, it has morphisms between morphisms.

Above we argued that equality should be deferred in favour of isomorphism at the morphism level. Hence, in a 2-Category, it is only reasonable to defer an equation involving objects to be up to isomorphism of 2-morphisms —this is then called an “equivalence”.

ℒHS ≃ ℛHS  ⇔  Σ F ∶ ℒHS ⟶ ℛHS • Σ G ∶ ℛHS ⟶ ℒHS • F ⨾ G ≅ G ⨾ F ≅ Id

Hence when it comes to categories themselves, one usually speaks in terms of equivalences rather than isomorphisms.

For example, let 𝒫𝒶𝓇 be the supercategory of 𝒮e𝓉 with morphisms being ‘partial functions’ (A ⟶ B) = (A → B + 𝟙) where the extra element of 𝟙 = { * } represents ‘undefined’ —also known as the Partial, Option, or Maybe monads. Moreover, let 𝒫𝒮ℯ𝓉 be the category of sets with an elected point. Then, 𝒫𝒶𝓇 ≃ 𝒫𝒮e𝓉 is witnessed by (A ⟶ B) ↦ ( (A + 𝟙, *) ⟶ (B + 𝟙, *) ) and conversely ( (A , a) ⟶ (B , b) ) ↦ ( A - a ⟶ B - b) where
X - x ≡ Σ y ∶ X • ¬(x ≡ y). Exercise: Work out the remaining details for the equivalence.

Let us give some elementary examples of the notion of a category to exhibit its ubiquity.

A functor among monoids –construed as categories– is just a monoid homomorphism; i.e., an identity and multiplication preserving function of the carriers.

By induction, h preserves all finite ⊕-multiplication and, more generally, functors preserve finite compositions: \[ F (f₀ ⨾ f₁ ⨾ ⋯ ⨾ fₙ) \;\;=\;\; F\,f₀ ⨾ F\,f₁ ⨾ ⋯ ⨾ F\,fₙ \] Cool beans :-)

In the same way, sit down and check your understanding!

• A functor among discrete categories is just a function of the associated sets.
• A functor among poset categories is an order-preserving function.

Two examples of functors from a poset (category) to a monoid (category):

• monus : (ℕ, ≤) ⟶ (ℕ,+, 0) is a functor defined on morphisms by \[ i ≤ j \quad⇒\quad \mathsf{monus}(i,j) ≔ j - i\] Then the functor laws become i - i = 0 and (k - j) + (j - i) = k - i.
• div : (ℕ⁺, ≤) → (ℚ, ×, 1) is defined on morphisms by \[i ≤ j \quad⇒\quad \mathsf{div}(i,j) ≔ j / i\] 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 are categorically seen as kan extensions. Alternatively, they’re are instances of ‘(Kopka) Difference-posets’.

For more examples of categories, we will need to reason by extensionality –two things are ‘equal’ when they have equivalent properties … recall Leibniz and his law of indiscernibles ;p

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 that says how every category can be construed as a graph.

First the category of smaller categories,

𝒞𝒶𝓉 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! )

 instance
  𝒞𝒶𝓉 : ∀ {i j} → Category {ℓsuc (i ⊍ j)} {ℓsuc (i ⊍ j)}
  𝒞𝒶𝓉 {i} {j} = record {
      Obj = Category {i} {j}
    ; _⟶_ = Functor
    ; _⨾_ = λ {𝒞} {𝒟} {ℰ} F G →
        let instance
                   𝒞′ : Category ; 𝒞′ = 𝒞
                   𝒟′ : Category ; 𝒟′ = 𝒟
                   ℰ′ : Category ; ℰ′ = ℰ
        in 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)
            ≡⟨ functor F preserves-identities even-under (mor G) ⟩
              mor G Id
            ≡⟨ functor G preserves-identities ⟩
              Id
            ∎
        ; comp = λ {x y z f g} →
             begin
               (mor F ⨾ mor G) (f ⨾ g)
            ≡⟨ "definition of function composition" ⟩′
               mor G (mor F (f ⨾ g))
             ≡⟨ functor F preserves-composition even-under mor G ⟩
               mor G (mor F f ⨾ mor F g)
             ≡⟨ functor G preserves-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,

• First off: functor F preserves-composition even-under mor G is a real line of code! It consists of actual function calls and is merely an alias for ≡-cong (mor G) (mor F) but it sure is far more readable than this form!

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

In a nearly identical way, just ignoring the algebraic datum, we can show that Graph's with GraphMap's form a graph

  𝒢𝓇𝒶𝓅𝒽 : Category
  𝒢𝓇𝒶𝓅𝒽 = {! exercise !}

Let’s formalise 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 --≡-refl– 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.

Now the remainder of these notes is to build-up the material needed to realise the notion of ‘free’ which is, in some sense, the best-possible approximate inverse to ‘forgetful’ –however, forgetting is clearly not invertible since it can easily confuse two categories as the same graph!

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\); namely \((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 possible natural transformation \(F \natTo G\).

That is,

Thus, if a construction every involves having to decide between distinct routes, then chances are the result is not formally natural. Sometimes this ‘inution’ is developed from working in a field for some time; sometimes it just “feel”" natural.

Some would even say: Natural = God-given.

A natural transformation can be thought of as a polymorphic function ∀ {X} → F X ⟶ G X where we restrict ourselves to avoid inspecting any X.

• Recall that a mono-morphic operation makes no use of type variables in its signature, whereas a poly-morphic operation uses type variables in its signature.
• For example, in C# one can ask if one type is a subclass of another thereby obtaining specific information, whereas there is no such mechanism in Haskell.

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 and so such functions are natural transformations by default! Theorems for free!

For example,

-- Let 𝒦 x y ≔ Id {x} for morphisms, and 𝒦 x y ≔ x for objects.

size : ∀ {X} → List X → 𝒦 ℕ X
size [x₁, …, xₙ] = n

is a polymorphic function and so naturality follows and is easily shown –show it dear reader! So we have always have \[List\; f \;⨾\; size \quad=\quad size\] Since 𝒦 ℕ f = Id, then by extensionality: size : List ⟶̇ 𝒦.

On the other hand, the polymorphic function

whyme : ∀ {X} → List X → 𝒦 Int X
whyme {X} [x₁,…,xₙ] = If X = ℕ then 1729 else n

is 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 –do so!

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, observe that a solution in \(h\) to the absorptive-equation \(F f ⨾ h = h\) is precisely a natural transformation from \(F\) to the aforementioned ‘diagonal functor’: \[F f ⨾ h \;=\; h \qquad⇔\qquad ∃ X : Obj \;•\; h ∈ F \overset{.}{⟶} 𝒦 X ~\]

In particular, due to the constant-fusion property \(g \,⨾\, 𝒦\, e \;=\; 𝒦\, e\), we have that \[∀ \{F\} \{X\} \{e \,:\, X\} \;→\; (𝒦\, e) \,∈\, F \overset{.}{⟶} 𝒦\, X \] Is the converse also true? If \(h ∈ F ⟶̇ 𝒦 X\) then \(h \,=\, 𝒦\, 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 ★ : 𝟙

  -- Choice function: For any type X, it yields an argument of that type.
  postulate ε : (X : Set) → X

  nay : ∀ {X} → X → X
  nay {X} _ = ε X

Now naturality \(\Id \, f ⨾ nay_B \;=\; nay_A ⨾ \Id \, f\) breaks as witnessed by \(f \;=\; (λ _ → εℕ + 1) \;:\; 𝟙 → ℕ\) –and provided \(εℕ ≠ 0\), otherwise we could use an \(f\) with no fix points.

From this we may hazard the following: If we have natural transformations \(ηᵢ \,:\, ∀ {X : Objᵢ} →\, F X \overset{.}{⟶} G X\) where the \(Objᵢ\) partition the objects available — i.e., \(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 simultaneously for all x —there is no inspection of some particular x here and there, no, it is uniform! With this view, the naturality condition is thought of as a ‘simultaneity’ condition. Rephrasing GToNE.

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. For example, TODO seq-pair or pair-seq ;-)

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 compound structure can be ‘promoted’ into its components.
• Reading F f ⨾ η {B} = η {A} ⨾ G f from left to right: Mapping \(f\) over a complicated structure then handling the result is the same as handling the complex datum then mapping \(f\) over the result.
  • `Handling' can be thought of as `processing' or as `reshaping'.

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 Richard Bird and Oege de Moor –whose text can be found here, albeit the legitimacy of the link may be suspect.

For example, recall the 𝒦onstant functor now construed only as a polymorphic binary operation:

_⟪_    :  ∀{A B : Set} → A → B → A
a ⟪ b  =  a

The above is a constant time operation, whereas the next two are linear time operations; i.e., they take n steps to compute, where n is the length of the given list.

-- This' map for List's; i.e., the mor of the List functor
map    : ∀ {A B : Set} (f : A → B) → List A → List B
map f []         =  []
map f (x ∷ xs)  =  f x ∷ map f xs

-- Interpret syntax `x₀∷⋯∷xₙ₋₁` semantically as `x₀ ⊕ ⋯ ⊕ xₙ₋₁`, where ⊕ = cons.
fold  : ∀ {A B : Set} (cons : A → B → B) (nil : B) → List A → B
fold cons nil [] = nil
fold cons nil (x ∷ xs) = cons x (fold cons nil xs)

By Theorems for Free, or a simple proof, we have that fold is a natural transformation \(List \overset{.}{→} \Id\): \[ List\; f \;⨾\; fold \; cons_B \; nil_B \qquad=\qquad fold \; cons_A \; nil_A \;⨾\; f \] Note that here we are ranging over objects \(X\) equipped with \(nil_X : X, \; cons_X : X → X → X\); as such the equation is not valid when this is not the case.

Now we map compute,

postulate A B : Set
postulate nil-B : B
postulate f : A → B -- possibly expensive operation

head  :  List B → B
head  =  fold _⟪_ nil-B

compute  :  List A → B
compute  =  map f  ⨾  head

That is,

  compute [x₀, …, xₙ₋₁]
= head (map f [x₀, …, xₙ₋₁])
= head [f x₀, …, f xₙ₋₁]
= f x₀  ⟪  f x₁ ⟪ ⋯ ⟪ ⋯ f xₙ₋₁ ⟪ nil-B
= f x₀

However this approach performs the potentially expensive operation \(f\) a total of \(n = \text{“length of input”}\) times! In spite of that, it only needs the first element of the list and performs the operation only once! Indeed, by the naturality of fold we have an equivalent, and more efficient, formulation:

compute  =  head  ⨾  f

This operation only performs the potentially costly f once!

A more concrete and realistic example is to produce an efficient version of the function that produces the average xs = div (sum xs, length xs) of a list of numbers: This operation traverses the input list twice, yet we can keep track of the length as we sum-along the list to obtain an implementation that traverses the list only once!

Indeed,

div : ℕ × ℕ → ℕ
div (0, 0) = 0
div (m, n) = m ÷ n

average     :  List ℕ → ℕ
average xs  =  div (fold _⊕_ 𝟘 xs)
  where  𝟘 = (0 , 0)
         _⊕_  : ℕ → (ℕ × ℕ) → ℕ
         a ⊕ (b , n) = (a + b , n + 1)

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.

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 … –mind blown!

For example, I want to define a transformation \(\mathsf{List} ⟶̇ \mathsf{List}\).

1. So let me suppose the input is of the shape \(\List \, f\, x\), more concretely it is of the shape
   [f x₀, f x₁, …, f xₙ₋₁] –for arbitrary \(f : A → B\).
2. Then the output shape must be \(\List \, f\, (η \, x)\), more concretely it is of the shape
   [f y₀, f y₁, …, f yₘ₋₁] where \(y \,=\, η\,x\).

3. So my only choices are \(y : \List A\) and \(m : ℕ\)

   Here are some possibilities and the resulting η:

   \(y, m = x, n\)

   Identity function

   \(y, m = x, 0\)

   Constantly empty list [] function

   \(y, m = x, 1\)

   The first element, ‘head’, function

   \(y, m = x, k\)

   The first \(k < n\) elements function

   \(m = n\) with \(yᵢ = xₙ₋ᵢ\)

   List reversal function

   \(y, m = \mathsf{reverse}(x), k\)

   The last \(k < n\) elements, in reverse, function

   • Here we applied an already known natural transformation and indeed the composition of naturally transformation is itself natural.

Pointwise Monotonicity

A functor among poset categories is an order-preserving function and a natural transformation \(f \natTo g\) is a proof that \(f \overset{.}{≤} g\) pointwise: \(∀ x \,•\, f\, x \;≤\; g\, x\) —all the other pieces for a natural transformation are automatic from the definition of begin a poset category.

conjugation

A functor among monoids –construed as categories– is just a monoid homomorphism:

\begin{align*} & (M, ⊕, e) ⟶ (N, ⊗, d) {{{newline}}} ≅ \quad & Σ h ∶ M → N • ∀ \{x \, y \} •\; h(x ⊕ y) = h x ⊗ h y \lands h e = d \end{align*}

A natural transformation (f, prf) ⟶ (g, prf’) is a point \(n : N\) with \(∀ x ∶ M \;•\; f x ⊗ n \,=\, n ⊗ g x\), a so-called ‘conjugation’ by \(n\) that takes \(f\) to \(g\).

fold

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 \(𝒰 × 𝒰 \natTo 𝒰\), 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 \(ℒ \natTo 𝒰\) 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ₙ

–The reader would pause to consider implementing this formally using Agda's Data.Fin and Data.Vec ;-)–

Now for any monoid homomorphism h, applying induction, yields

    h₀(x₁ ⊕ ⋯ ⊕ xₙ)  =  h₀ x₁ ⊕ ⋯ ⊕ h₀ xₙ  where  h₀ = 𝒰 (h₀, prf) = 𝒰 h

Which is easily seen to be just naturality – if we use backwards composition \(f ⨾ g \;=\; g ∘ f\) –

    𝒰 h ∘ fold {M}  =  fold {N} ∘ ℒ h

Woah!

Every operation in any multisorted algebraic structure gives a natural transformation

This is mentioned in the Barr and Wells' Category Theory for Computing Science text, citing Linton, 1969a-b.

For example, src, tgt —from the graph signature— give natural transformations \(V \natTo E\) from the vertex functor to the edge functor … keep reading ;)

Representability

Recall that \(V(G)\) is essentially \(ℙ₀ ⟶ G\) where \(ℙₙ\) is the graph of \(n\) edges on \(n+1\) vertices named \(0..n\) with typing \(i \,:\, i-1 ⟶ i\), which I like to call the path graph of length n; and in particular \(ℙ₀\) is the graph of just one dot, called 0, and no edges. —Earlier I used the notation [n], but I’m using \(ℙ\) since I like the view point of ℙaths.

What does it mean to say that V(G) is essentially ℙ₀ ⟶ G?

It means that the vertices functor – \(𝒱 \;:\; 𝒢𝓇𝒶𝓅𝒽 ⟶ 𝒮ℯ𝓉\) that takes objects \(G ↦ V(G)\) and morphisms \(h ↦ \mathsf{ver}\, h\) – can be ‘represented’ as the Hom functor \((ℙ₀ ⟶ \_{})\), that is to say \[𝒱 \quad≅\quad (ℙ₀ ⟶ \_{}) \;\mathsf{within \; Func} \; 𝒢𝓇𝒶𝓅𝒽 \; 𝒮ℯ𝓉\] --Func-tor categories will be defined in the next section!–

Notice that we arrived at this expression by ‘eta-reducing’ the phrase V(G) is essentially ℙ₀ ⟶ G! ;)

More generally, we have the functor \(ℙₙ ⟶ \_{}\) which yields all paths of length \(n\) for a given graph.

Observe –i.e., show– that we also have an edges functor.

We give an example of a functor by building on our existing graphs setup. After showing that graphs correspond to certain functors, we then mention that the notion of graph-map is nothing more than the associated natural transformations!

 module graphs-as-functors where

Let 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 = f

Putting 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 laws

Now 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 whose vertices and edges are the sets associated with the sort-symbols V and E, respectively.

  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 𝒢₁.t

It 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. Nice!

The ‘dual’ or ‘opposite’ category 𝒞ᵒᵖ is the category constructed from 𝒞 by reversing arrows: \((A ⟶_{𝒞ᵒᵖ} B) \;≔\; (B ⟶_𝒞 A)\), then necessarily \((f ⨾_{𝒞ᵒᵖ} g) \;≔\; g ⨾_𝒞 f\). A ‘contravariant functor’, or ‘cofunctor’, is a functor F from an opposite category and so there is a reversal of compositions: \(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 naturally isomorphic to identities; C.f., ‘evil’ above.

Some interpretations:

• 𝒮e𝓉ᵒᵖ is usual sets and functions but with ‘backwards composition’:

   infix 10 _∘_
   _∘_ : ∀ {i j } ⦃ 𝒞 : Category {i} {j}⦄ {A B C : Obj 𝒞} → 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 𝓉ℯ𝒮 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.

• Stone Duality: FinBoolAlg ≃ FinSets ᵒᵖ , witnessed by considering the collection of atoms of a Boolean Algebra in one direction and the power set in the other. Finiteness can be removed at the cost of completeness and atomicitiy, CompleteAtomicBoolAlg ≃ 𝒮ℯ𝓉 ᵒᵖ.
• 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 ‘op’ium 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.

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 produces 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 • 𝒞, likewise for ‘Σ’. For the empty family, the empty sum yields the category 𝟘 with no objects and the empty product yields the category 𝟙 of one object. One can then show the usual ‘laws of arithmetic’ —i.e., ×,+ form a commutative monoid, up to isomorphism— 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 distributivity 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 distributivity 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).
• Interestingly, the sum of two monoids is not formed by their disjoint union: Instead it is the set of all alternating lists of elements from the two given monoids. Exercise: Find the associated operation ;-)

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 }

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 !}

By ‘extensionality’ 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𝓉 {j})
   -- hence contravariant in ‘first arg’ and covaraint in ‘second arg’
 Hom {𝒞 = 𝒞} =
   let
     module 𝒞 = Category 𝒞
     instance 𝒞′ : Category ; 𝒞′ = 𝒞
     ⨾-cong₂ : ∀ {A B C : Obj 𝒞} {f : A 𝒞.⟶ B} {g g’ : B 𝒞.⟶ C}
             → g ≡ g’ → f 𝒞.⨾ g ≡ f 𝒞.⨾ g’
     ⨾-cong₂  q  =  ≡-cong₂ 𝒞._⨾_ ≡-refl q
   in record {
     obj = λ{ (A , B) →  A ⟶ B }
   ; mor = λ{ (f , g) → λ h → f ⨾ h ⨾ g }
   ; id = 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’
          ∎)
     }

The naming probably comes from the algebra/monoid case where the functors are monoid hom-omorphisms. Some prefer to use the name Mor, short for mor-phisms, 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 :-)

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 F consists of two maps (F₀, F₁) ≔ (obj F, mor F) 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 is

full

If morphisms starting and ending at F are a result of applying \(F\);
i.e., F₁ is surjective on the image of F₀:
\(∀ 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:

1. Suppose 𝒞 consists of 𝒟 objects satisfying some axioms and 𝒟 maps preserving this structure.
2. That is, 𝒞 has pairs of 𝒟 objects/morphisms with a proof that it satisfies the axioms/preserves-structure.
3. Then “\(F : 𝒞 ⟶ 𝒟\) forgets only axioms” means \(F\, (f, \mathsf{proof}) \;=\; f\).

4. 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 0, the relation equidistant-from-0 is an equivalence relation –Exercise!–, 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.

( Exercise: A functor F : 𝒞 ≃ 𝒟 is (part of) an equivalence iff it is full, faithful, and ‘‘essentially surjective on objects’’: ∀ D : Obj 𝒟 • Σ C : Obj 𝒞 • F C ≅ D —note the iso. )

If you’ve ever studied abstract algebra —the math with vector spaces— then you may recall that a collection of vectors ℬ 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 ℬ 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!

Thus, 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 \(ι : ℬ ↪ 𝒱\) 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]. Reasoning similarly as above, or if you have familiarity 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: \(F ⊣ U\) is a (free-forgetful) ‘adjunction’ means for functors ‘forget’ \(U : 𝒞 ⟶ 𝒮\) and ‘free’ \(F : 𝒮 → 𝒞\), we have that for a given 𝒮imple-object \(S\) there’s 𝒮imple-map \(ι : S ⟶_𝒮 U\,(F\, S)\) —a way to realise ‘basis vectors’— such that for any 𝒞omplicated-object \(C\) and 𝒮imple-maps \(φ : S ⟶_𝒮 U\, C\), there is a unique 𝒞omplicated-map \(Φ : F\, S ⟶_𝒞 C\) that preserves the basis vectors: \(φ = ι ⨾ U Φ\).

By analogy to the previous two cases, we may consider \(U\, X\) to be a ‘basis’, and make the slogan: 𝒞omplicated-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 determined by what \(f\) does to the generators ;-) ]

An adjunction \(L ⊣ U\), where the L-ower adjoint is from 𝒮 to 𝒞 and the U-pper 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!

Formally this correspondence, saying \(F : 𝒞 ⟶ 𝒟\) is adjoint to \(G : 𝒟 ⟶ 𝒞\), written \(F ⊣ G\), holds precisely when \((F ∘ X ⟶ Y) \;≅\; (X ⟶ G ∘ Y)\) in a functor category:

 _⊣₀_ : ∀ {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 Agda's built-in rewrite mechanism to add the rule,

{𝒞 𝒟 : Category {ℓ₀} {ℓ₀}} → Functor (𝒞 ᵒᵖ) (𝒟 ᵒᵖ) ≡ Functor 𝒞 𝒟

then we might be able to get away without using opify.

Anyhow, this says for any objects \(X\) and \(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

   open Category 𝒟 renaming (_⨾_ to _⨾₂_)
   open Category 𝒞 renaming (_⨾_ to _⨾₁_)
   field
     -- ‘left-adjunct’  L ≈ ⌊  and  ‘right-adjunct’  r ≈ ⌈
     ⌊_⌋ : ∀ {X Y} →   obj F X ⟶ Y ∶ 𝒟   →   X ⟶ obj G Y ∶ 𝒞
     ⌈_⌉ : ∀ {X Y} →   X ⟶ obj G Y ∶ 𝒞   →   obj F X ⟶ Y ∶ 𝒟

     -- Adjuncts are inverse operations
     lid : ∀ {X Y} {d : obj F X ⟶ Y ∶ 𝒟} → ⌈ ⌊ d ⌋ ⌉ ≡ d
     rid : ∀ {X Y} {c : X ⟶ obj G Y ∶ 𝒞} → ⌊ ⌈ c ⌉ ⌋ ≡ c

     -- That for a fixed argument, are natural transformations between Hom functors
     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 ⨾₂ ⌈ ψ ⌉ ⨾₂ g

This is easier for verifying an adjunction, while the former is easier for remembering and understanding what an adjunction actually is.

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 lengthy. More elegantly, we can say the supremum operation is left-adjoint to the constant function: \[ \mathsf{sup} ⊣ 𝒦 \] which means \[ ∀ z •\qquad \mathsf{sup}\, f \,≤\, z \quad⇔\quad f \overset{.}{≤} 𝒦\, z\] Where \(𝒦\, x\, y \,=\, x\) and the \(\overset{.}{≤}\) on the right is the point-wise ordering on functions. 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 & Al-hassy.

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.

Another awesome thing about adjunctions L ⊣ U is that they give us ‘representable functors’, a.k.a. ‘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 𝒮ℯ𝓉 we have (A ⟶ 𝟙) ≅ 𝟙 and (𝟙 ⟶ A) ≅ A.
• Specialising 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 𝒮ℯ𝓉 by adding some structure and we are interested in 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 the one-point monoid is the terminal object: 𝟙 ≔ ({*}, ⊕, *) with x ⊕ y ≔ ⋆. Then every monoid-homomorphism from 𝟙 just picks out an element of the carrier of a monoid and so (𝟙 ⟶ M) ≅ 𝒰 M where 𝒰 is the forgetful functor for monoids mentioned in the introduction.

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 comic book library and for more on the adjective ‘forgetful’ see ncatlab or mathworld A nice list of common free objects can be found on wikipedia.

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 listening to this lovely musical 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 from 𝒞𝒶𝓉 to 𝒢𝓇𝒶𝓅𝒽.

With paths in hand, we can now consider a neat sequence of exercises :-)

1. 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 ;)

   Hint: This is lift from the next section.

2. Define

   a connected b  ≡  (a ⇝ b) ⊎ (b ⇝ a)  --  path “between” a and b; not ‘from a to b’.
   

3. This is an equivalence relation whose equivalence classes are called the connected components of G; denote them by 𝒦G.
4. For any category 𝒞, define 𝒦 𝒞 ≔ 𝒦 (𝒰₀ 𝒞) which is a subcategory of 𝒞.
5. Phrase the connected components subcategory using a universal property, thereby avoiding the need for quotient types.
6. Since graphmaps preserve paths, every graph map can be extended to connected components, 𝒦f : 𝒦G ⟶ 𝒦H : (connected component of x) ↦ (connected component of fᵥ x).
7. Hence, we have a functor 𝒦 : Graph ⟶ Set.

8. Then there is a natural transformation 𝒱 ⟶ 𝒦, where 𝒱 is the vertices functor.

   Hint: Such a transformation means we can realise vertices as connected components and this suggests taking assigning a vertex to the connected-component block that contains it.

   yeah!

Finally, if we let 𝒟 : 𝒮ℯ𝓉 → 𝒞𝒶𝓉 be the free category functor that associates each set with the discrete category over it, then we have 𝒦 is the associated forgetful functor.

Here's a handy-dandy combinator for forming certain equality proofs of paths.

  -- Preprend preserves path equality
  ⟶-≡ : ∀{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) eq

Less usefully, we leave as exercises:

  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.

Now we turn back to the problem of catenating 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-associativity

Notice that the the base case indicate that ! forms a left-unit for ++, while the inductive case says that path-formation associates with path catenation. Both observations also hold for the definition of list catenation ;-)

If we had not typed our paths, as in Path₂, we would need to carry around a proof that paths are compatible for concatenation:

  catenate : (p q : Path) (coh : end p ≡ head q) → Path
  syntax catenate p q compatibility = p ++[ compatibility ] q

Even worse, to show p ++[ coh ] q ≡ p ++[ coh’ ] q we need to invoke proof-irrelevance of identity proofs to obtain coh ≡ coh’, 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 _++_ indicates _! is a left unit,

  leftId : ∀ {x y} {p : x ⇝ y} → x ! ++ p ≡ p
  leftId = ≡-refl

Is 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) rightId

Is 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 G constitute a category! Let’s call it 𝒫 G.

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 defining it 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  = amore
    ; id   = ≡-refl
    ; comp = λ {x} {y} {z} {p} → comp {p = p}
    }
    where
      open TypedPaths ⦃...⦄ public
      instance G' : Graph ; G' = G
               H' : Graph ; H' = H

      amore : {x y : Graph.V G} →  x ⇝ y → (ver f x) ⇝ (ver f y)
      amore (x !) = ver f x !
      amore (x ⟶[ e ]⟶ p) = ver f x ⟶[ edge f e ]⟶ amore p

      comp : {x y z : Graph.V G} {p : x ⇝ y} {q : y ⇝ z}
          →  amore (p ++ q)  ≡  amore p ++ amore 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 (id ⦃ G ⦄)
            ; comp = funcext ≡-refl comp
            }
    where
      open TypedPaths ⦃...⦄
      open Category   ⦃...⦄

      module 𝒞𝒶𝓉   = Category 𝒞𝒶𝓉
      module 𝒢𝓇𝒶𝓅𝒽 = Category 𝒢𝓇𝒶𝓅𝒽

      id : ∀ ⦃ G ⦄ {x y} {p : x ⇝ y}
        →   mor (𝒞𝒶𝓉.Id {𝒫₀ G}) p  ≡  mor (𝒫₁ (𝒢𝓇𝒶𝓅𝒽.Id)) p
      id {p = x !} = ≡-refl
      id {p = x ⟶[ e ]⟶ ps} = ⟶-≡ (id {p = ps})

      comp : {G H K : Graph} {f : GraphMap G H} {g : GraphMap H K}
           → {x y : Graph.V G} {p : TypedPaths._⇝_ G x y}
           →  mor (𝒫₁ f 𝒞𝒶𝓉.⨾ 𝒫₁ g) p  ≡  mor (𝒫₁ (f 𝒢𝓇𝒶𝓅𝒽.⨾ g)) p
      comp {p = x !} = ≡-refl
      comp {p = x ⟶[ e ]⟶ ps} = ⟶-≡ (comp {p = ps})

It seemed prudent in this case to explicitly delimit where the compositions lives —this is for clarity, since Agda can quickly resolve the appropriate category instances.

Exercise: Show that we have a natural transformation Id ⟶ 𝒰 ∘ 𝒫.

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 the edges \(e₁, …, eₖ\) of a path to a morphism \(\edge\, f\, e₁ ⨾ ⋯ ⨾ \edge\, f\, eₖ\). That is, a path of the form \[x_0 \xrightarrow{e_1} x_1 \xrightarrow{e_2} x_2 \xrightarrow{e_3} ⋯ \xrightarrow{e_k} x_k \] Is lifted to the composition of morphisms \[\mathsf{ver}\, f\, x_0 \xrightarrow{\edge\, f\, e_1} \mathsf{ver}\, f\, x_1 \xrightarrow{\edge\, f\, e_2} \mathsf{ver}\, f\, x_2 \xrightarrow{\edge\, f\, e_3} ⋯ \xrightarrow{\edge\, f\, e_k} \mathsf{ver}\, f\, x_k \]

Of course, we then need to verify that this construction is indeed functorial.

  lift : G ⟶ 𝒰₀ 𝒞  →  𝒫₀ G ⟶ 𝒞
  lift f = record
     { obj  = λ v → ver f v -- Only way to obtain an object of 𝒞; hope it works!
     ; mor  = fmap
     ; id   = ≡-refl
     ; comp = λ {x y z p q} → proof {x} {y} {z} {p} {q}
     }
     where
          fmap : ∀ {x y} → x ⇝ y → ver f x 𝒞.⟶ ver f y
          fmap (y !) = 𝒞.Id
          fmap (x ⟶[ e ]⟶ p) = edge f e 𝒞.⨾ fmap p

          -- homomorphism property
          proof : ∀{x y z} {p : x ⇝ y} {q : y ⇝ z} → fmap (p ++ q) ≡ fmap p 𝒞.⨾ fmap q
          proof {p = ._ !} = ≡-sym 𝒞.leftId
          proof {p = ._ ⟶[ e ]⟶ ps} =  ≡-cong (λ m → edge f e 𝒞.⨾ m) (proof {p = ps})
                                     ⟨≡≡⟩ ≡-sym assoc
                                     -- Exercise: Rewrite this calculationally!

Now we have the embedding and the lifting, it remains to show that the aforementioned ‘preserves basis’ property holds as does uniqueness.

Let's begin with the ‘basis preservation’ property:

  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 identity "⟩′
              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 graphmapext ≡-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 that there is a unique way to preserve ‘basis’:

  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
       ≡⟨" definition of 𝒰 gives: edge (𝒰₁ F) = mor F "⟩′
         (edge ι 𝒮ℯ𝓉.⨾ mor F) e 𝒞.⨾ mor F ps
       ≡⟨" definition of functional composition 𝒮ℯ𝓉 "⟩′
          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)
       ∎

Challenge: Define graph-map equality ‘≈g’ by extensionality –two graph maps are equal iff their vertex and edge maps are extensionally equal. This is far more relaxed than using propositional equality ‘≡’. Now show the stronger uniqueness claim:

∀{f : G ⟶ 𝒰₀ 𝒞} {F : 𝒫₀ G ⟶ 𝒞}   →   f  ≈g  (ι ⨾ 𝒰₁ F)   →   lift f  ≡  F

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 exercises,

  lift˘ : Functor 𝒫G 𝒞 → GraphMap G (𝒰₀ 𝒞)
  lift˘ F = ι ⨾g 𝒰₁ F  --  i.e., record {ver = obj F , edge = 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 provide an alternative, and more succinct, proof of uniqueness for ‘basis preservation’:

  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
    ∎

The difference between this proof and the original one is akin to the difference between heaven and earth! That or it's much more elegant ;-)

Thus far, we have essentially shown \[(𝒫₀\, G \,⟶\, 𝒞) \quad≅\quad (G \,⟶\, 𝒰₀\, 𝒞)\] We did so by finding a pair of inverse maps:

lift   :  (    G ⟶ 𝒰₀ 𝒞)  →  (𝒫₀ G ⟶     𝒞)
lift˘  :  (𝒫₀ G  ⟶    𝒞)  →  (   G ⟶  𝒰₀ 𝒞)

This is nearly 𝒫 ⊣ 𝒰 which implies 𝒫 is a ‘free-functor’ since it is left-adjoint to a forgetful-functor.

‘Nearly’ since we need to exhibit naturality: For every graph map g and functors F, k we have lift˘ (𝒫 g ⨾ k ⨾ F) ≈ g ⨾ lift˘ k ⨾ 𝒰 F in the category of graphs.

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 lift-ed morphisms.

First the setup,

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 ⦃...⦄

  module 𝒞     = Category 𝒞
  module 𝒟     = Category 𝒟
  module 𝒢𝓇𝒶𝓅𝒽 = Category 𝒢𝓇𝒶𝓅𝒽
  module 𝒞𝒶𝓉   = Category (𝒞𝒶𝓉 {ℓ₀} {ℓ₀})
  module 𝒮ℯ𝓉   = Category (𝒮e𝓉 {ℓ₀})

Just as we needed to prove two inverse laws for lift and lift˘, we need two naturality proofs.

  naturality˘ : ∀ {K : Functor (𝒫₀ H) 𝒞}
              →  lift˘ (𝒫₁ g 𝒞𝒶𝓉.⨾ K 𝒞𝒶𝓉.⨾ F)  ≡  (g 𝒢𝓇𝒶𝓅𝒽.⨾ lift˘ K 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ F)
  naturality˘ = graphmapext ≡-refl ≡-refl

That was easier than assumed! Hahaha: Hard to formalise but so easy to prove lolz! It says we can ‘shunt’ lift˘ into certain compositions at the cost of replacing functor instances.

Now for the other proof:

  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 ⦃...⦄
      instance G′ : Graph ; G′ = G
               H′ : Graph ; H′ = H
      proof : ∀ {x y : Graph.V G} {p : x ⇝ y}
            →    mor (𝒫₁ g 𝒞𝒶𝓉.⨾ lift {H} {𝒞} k 𝒞𝒶𝓉.⨾ F) p
               ≡  mor (lift {G} {𝒟} (g 𝒢𝓇𝒶𝓅𝒽.⨾ k 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ F)) p
      proof {p = _ !} = functor (𝒫₁ g 𝒞𝒶𝓉.⨾ lift {H} {𝒞} k 𝒞𝒶𝓉.⨾ F) preserves-identities
      proof {p = x ⟶[ e ]⟶ ps} = begin
            mor (𝒫₁ g 𝒞𝒶𝓉.⨾ lift {H} {𝒞} k 𝒞𝒶𝓉.⨾ F) (x ⟶[ e ]⟶ ps)
         ≡⟨" By definition, “mor” distributes over composition "⟩′
            (mor (𝒫₁ g) 𝒮ℯ𝓉.⨾ mor (lift {H} {𝒞} k) 𝒮ℯ𝓉.⨾ mor F) (x ⟶[ e ]⟶ ps)
         ≡⟨" Definitions of function composition and “𝒫₁ ⨾ mor” "⟩′
            mor F (mor (lift {H} {𝒞} k) (mor (𝒫₁ g) (x ⟶[ e ]⟶ ps)))
                                                  -- This explicit path is in G
         ≡⟨" Lifting graph-map “g” onto a path "⟩′
            mor F (mor (lift {H} {𝒞} k) (ver g x ⟶[ edge g e ]⟶ mor (𝒫₁ g) ps))
                                                  -- This explicit path is in H
         ≡⟨" Definition of “lift ⨾ mor” on inductive case for paths "⟩′
            mor F (edge k (edge g e) 𝒞.⨾ mor (lift {H} {𝒞} k) (mor (𝒫₁ g) ps))
         ≡⟨ functor F preserves-composition ⟩
                mor F (edge k (edge g e))
           𝒟.⨾  mor F (mor (lift {H} {𝒞} k) (mor (𝒫₁ g) ps))
         ≡⟨" Definition of function composition, for top part "⟩′
               (edge g 𝒮ℯ𝓉.⨾ edge k 𝒮ℯ𝓉.⨾ mor F) e  -- ≈ mor F ∘ edge k ∘ edge g
           𝒟.⨾ (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)
         ∎

Formally, we now have an adjunction:

𝒫⊣𝒰 : 𝒫 ⊣ 𝒰
𝒫⊣𝒰 = 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 {𝒞} public

We called our path catenation _++_, why the same symbol as that for list catenation?

How do we interpret a list over \(A\) as a 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 we might as well 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 [x₀, …, xₖ] of A’s corresonds to a path x₀ ⇝ xₖ.
  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 in the inductive case, “list : Fin (suc (suc n)) → A”
    -- whereas “suc ⨾ list : Fin (suc n) → A”.
    --
    -- For example, if “list ≈ [x , y , z]” yields
    --          “fsuc ⨾ list ≈ [y , z ]” and
    --   “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, but it's in terms of path 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 consing its elements infront of ‘r’

  -- Exercise: Write path catenation as a path-fold.

These few adventures would suggest that much of list theory can be brought over to the world of paths. It looks promising, let me know dear reader if you make progress on related explorations!