module Cat.Instances.Free where

# Graphs and free categoriesπ

A **graph** (really, an
$(o, \ell)$-graph^{1}) is given by a set
$V : \mathbf{Sets}_o$
of **vertices** and, for each pair of elements
$x, y : V$,
a set of **edges**
$E(x, y) : \mathbf{Sets}_\ell$
from
$x$
to
$y$.
Thatβs it: a set
$V$
and a family of sets over
$V \times V$.
Really, for our purposes, graphs by themselves are not very interesting:
their utility comes in constructing new *categories*.

record Graph o β : Type (lsuc o β lsuc β) where field vert : Set o edge : β£ vert β£ β β£ vert β£ β Set β

Given a graph $G$, we construct a strict category $\mathrm{Path}(G)$ in the following manner:

- The objects of $\mathrm{Path}(G)$ are the vertices of $G$
- The morphisms in
$\mathrm{Path}(G)$
are given by
*finite paths*in $G$. Finite paths are defined by the following indexed-inductive type

data Path-in : β£ G.vert β£ β β£ G.vert β£ β Type (o β β) where nil : β {a} β Path-in a a cons : β {a b c} β β£ G.edge a b β£ β Path-in b c β Path-in a c

That is: a path is either empty, in which case it starts and ends at itself (these are the identity morphisms), or we can form a path from $a \to c$ by starting with a path $b \to c$ and precomposing with an edge $(a \to b) : G$. Much of the code below is dedicated to characterising the identity types between paths. Indeed, to construct a category $\mathrm{Path}(G)$, we must show that paths in $G$ form a set.

We have a couple of options here:

We can

*construct*paths*by recursion*, on their length: Defining a βpath from $x$ to $y$ of length $n$β by recursion on $n$, and then defining a path from $x$ to $y$ as being a pair $(n, xs)$ where $n : \N$$ and $xs$ is a path of length $n$;We can

*define*paths*by induction*, as is done above.

The former approach makes it easy to show that paths form a set: we
can directly construct the *set* of paths, by recursion, then
project the underlying type if necessary. But working with these paths
is very inconvenient, since we have to deal with explicit identities
between the endpoints. The latter approach makes defining functions on
paths easy, but showing that they are a set is fairly involved. Letβs
see how to do it.

The first thing weβll need is a predicate expressing that a path $xs : x \to y$ really encodes the empty path, and we have an identity of vertices $x \equiv y$. We can do this by recursion: If $xs$ is nil, then we can take this to be the unit type, otherwise itβs the bottom type.

is-nil : β {a b} β Path-in a b β Type (o β β) is-nil nil = Lift _ β€ is-nil (cons _ _) = Lift _ β₯

Weβd like to define a relation $\mathrm{Code}(xs, ys)$, standing for an identification of paths $xs \equiv ys$. But observe what happens in the case where weβve built up a path $a \to c$ by adding an edge: We know that the edges start at $a$, and the inner paths end at $c$, but the inner vertex may vary!

Weβll need to package an identification
$p : b \equiv b'$
in the relation for
$\mathrm{cons}$,
and so, weβll have to encode for a path
$xs \equiv ys$
*over* some identification of their start points. Thatβs why we
have path-codep and not βpath-codeβ. A value in
$\mathrm{Codep}_b(xs, ys)$
codes for a path
$xs \equiv ys$
over
$b$.

path-codep : β (a : I β β£ G.vert β£) {c} β Path-in (a i0) c β Path-in (a i1) c β Type (o β β)

Note that in the case where $xs = \mathrm{nil}$, Agda refines $b$ to be definitionally $a$, and we can no longer match on the right-hand-side path $ys$. Thatβs where the is-nil predicate comes in: We say that $ys$ is equal to $\mathrm{nil}$ if is-nil $ys$ holds. Of course, a cons and a nil can never be equal.

path-codep a nil ys = is-nil ys path-codep a (cons x xs) nil = Lift _ β₯

The recursive case constructs an identification of cons cells as a triple consisting of an identification between their intermediate vertices, and over that data, an identification between the added edges, and a code for an identification between the tails.

path-codep a {c} (cons {b = b} x xs) (cons {b = bβ²} y ys) = Ξ£[ bs β (b β‘ bβ²) ] (PathP (Ξ» i β β£ G.edge (a i) (bs i) β£) x y Γ path-codep (Ξ» i β bs i) xs ys)

By recursion on the paths and the code for an equality, we can show
that if we have a code for an identification, we can indeed compute an
identification. The most involved case is actually when the lists are
empty, in which case we must show that is-nil(xs)^{2}
implies that
$xs \equiv \mathrm{nil}$,
but it must be over an arbitrary identification
$p$^{3}. Fortunately, vertices in a graph
$G$
live in a set, so
$p$
is reflexivity.

path-encode : β (a : I β β£ G.vert β£) {c} xs ys β path-codep a xs ys β PathP (Ξ» i β Path-in (a i) c) xs ys path-encode a (cons x xs) (cons y ys) (p , q , r) i = cons {a = a i} {b = p i} (q i) $ path-encode (Ξ» i β p i) xs ys r i path-encode a nil ys p = lemma (Ξ» i β a (~ i)) ys p where lemma : β {a b} (p : a β‘ b) (q : Path-in a b) β is-nil q β PathP (Ξ» i β Path-in (p (~ i)) b) nil q lemma {a = a} p nil (lift lower) = to-pathp $ subst (Ξ» e β Path-in e a) (sym p) nil β‘β¨ (Ξ» i β subst (Ξ» e β Path-in e a) (G.vert .is-tr a a (sym p) refl i) nil) β©β‘ subst (Ξ» e β Path-in e a) refl nil β‘β¨ transport-refl _ β©β‘ nil β lemma _ (cons x p) ()

The next step is to show that codes for identifications between paths live in a proposition; But this is immediate by their construction: in every case, we can show that they are either literally a proposition (the base case) or built out of propositions: this last case is inductive.

path-codep-is-prop : β (a : I β β£ G.vert β£) {b} β (p : Path-in (a i0) b) (q : Path-in (a i1) b) β is-prop (path-codep a p q) path-codep-is-prop a nil xs x y = is-nil-is-prop xs x y where is-nil-is-prop : β {a b} (xs : Path-in a b) β is-prop (is-nil xs) is-nil-is-prop nil x y = refl path-codep-is-prop a (cons h t) (cons hβ² tβ²) (p , q , r) (pβ² , qβ² , rβ²) = Ξ£-pathp (G.vert .is-tr _ _ _ _) $ Ξ£-pathp-dep (is-propβpathp (Ξ» i β PathP-is-hlevel' 1 (G.edge _ _ .is-tr) _ _) q qβ²) (is-propβpathp (Ξ» i β path-codep-is-prop (Ξ» j β G.vert .is-tr _ _ p pβ² i j) t tβ²) r rβ²)

And finally, by proving that there is a code for the reflexivity path, we can show that we have an identity system in the type of paths from $a$ to $b$ given by their codes. Since these codes are propositions, and identity systems give a characterisation of a typeβs identity types, we conclude that paths between a pair of vertices live in a set!

path-codep-refl : β {a b} (p : Path-in a b) β path-codep (Ξ» i β a) p p path-codep-refl nil = lift tt path-codep-refl (cons x p) = refl , refl , path-codep-refl p path-identity-system : β {a b} β is-identity-system {A = Path-in a b} (path-codep (Ξ» i β a)) path-codep-refl path-identity-system = set-identity-system (path-codep-is-prop Ξ» i β _) (path-encode _ _ _) path-is-set : β {a b} β is-set (Path-in a b) path-is-set {a = a} = identity-systemβhlevel 1 path-identity-system $ path-codep-is-prop Ξ» i β a

path-decode : β {a b} {xs ys : Path-in a b} β xs β‘ ys β path-codep (Ξ» _ β a) xs ys path-decode = Equiv.from (identity-system-gives-path path-identity-system)

## The path categoryπ

By comparison, constructing the actual precategory of paths is almost trivial. The composition operation, concatenation, is defined by recursion over the left-hand-side path. This is definitionally unital on the left.

_++_ : β {a b c} β Path-in a b β Path-in b c β Path-in a c nil ++ ys = ys cons x xs ++ ys = cons x (xs ++ ys)

Right unit and associativity are proven by induction.

++-idr : β {a b} (xs : Path-in a b) β xs ++ nil β‘ xs ++-idr nil = refl ++-idr (cons x xs) = ap (cons x) (++-idr xs) ++-assoc : β {a b c d} (p : Path-in a b) (q : Path-in b c) (r : Path-in c d) β (p ++ q) ++ r β‘ p ++ (q ++ r) ++-assoc nil q r = refl ++-assoc (cons x p) q r = ap (cons x) (++-assoc p q r)

And thatβs it! Note that we must compose paths backwards, since the type of the concatenation operation and the type of morphism composition are mismatched (theyβre reversed).

open Precategory Path-category : Precategory o (o β β) Path-category .Ob = β£ G.vert β£ Path-category .Hom = Path-in Path-category .Hom-set _ _ = path-is-set Path-category .id = nil Path-category ._β_ xs ys = ys ++ xs Path-category .idr f = refl Path-category .idl f = ++-idr f Path-category .assoc f g h = ++-assoc h g f

Moreover, free categories are always *gaunt*: they are automatically strict and,
as can be seen with a bit of work, univalent. Univalence follows because
any non-trivial isomorphism would have to arise as a cons, but cons can never be nil β which would be required
for a composition to equal the identity.

While types prevent us from directly stating βif a map is invertible, it is nilβ, we can nevertheless pass around some equalities to make this induction acceptable.

Path-category-is-category : is-category Path-category Path-category-is-category = r where module Pc = Cat.Reasoning Path-category remβ : β {x y} (j : Pc.Isomorphism x y) β Ξ£ (x β‘ y) Ξ» p β PathP (Ξ» i β Pc.Isomorphism x (p i)) Pc.id-iso j remβ {x = x} im = go im (im .Pc.to) refl (path-decode (im .Pc.invr)) where go : β {y} (im : Pc.Isomorphism x y) (jβ² : Path-in x y) β jβ² β‘ im .Pc.to β path-codep (Ξ» _ β x) (jβ² ++ im .Pc.from) nil β Ξ£ (x β‘ y) Ξ» p β PathP (Ξ» i β Pc.Isomorphism x (p i)) Pc.id-iso im go im nil p q = refl , Pc.β -pathp refl refl p r : is-category Path-category r .to-path i = remβ i .fst r .to-path-over i = remβ i .snd Path-category-is-gaunt : is-gaunt Path-category Path-category-is-gaunt = record { has-category = Path-category-is-category ; has-strict = hlevel! }