module Cat.Instances.MarkedGraphs where

# Marked graphsπ

Recall that every graph
$G$
gives rise to a free
category
$Path(G).$
Though useful, this construction is rather limiting; if we want to
construct (strict)
categories via combinatorial methods, then we really do need a way to
add non-trivial equalities. In other words, we need to be able to
construct categories freely from a set of generators *and*
relations! This leads us to the following series of definitions:

A **marked graph** consists of a graph
$G$
along with a set of pairs of distinguished paths in
$G,$
which we will call **marked pairs**.

record Marked-graph (o β : Level) : Type (lsuc o β lsuc β) where no-eta-equality field graph : Graph o β open Graph graph public field Marked : β {x y} β Path-in graph x y β Path-in graph x y β Ξ©

private variable o β o' β' : Level G H K : Marked-graph o β open Marked-graph open hlevel-projection instance Underlying-Marked-graph : Underlying (Marked-graph o β) Underlying-Marked-graph = record { β_β = Vertex }

A **marked graph homomorphism**
$f:GβH$
is a graph
homomorphism that takes a marked pair
$p,q:G_{β}$
in
$G$
to a marked pair
$f(p),g(p):H_{β}$
in
$H.$

record Marked-graph-hom (G : Marked-graph o β) (H : Marked-graph o' β') : Type (o β β β o' β β') where no-eta-equality field hom : Graph-hom (G .graph) (H .graph) pres-marked : β {x y} {p q : Path-in (G .graph) x y} β β£ G .Marked p q β£ β β£ H .Marked (path-map hom p) (path-map hom q) β£ open Graph-hom hom public

open Marked-graph-hom unquoteDecl H-Level-Marked-graph-hom = declare-record-hlevel 2 H-Level-Marked-graph-hom (quote Marked-graph-hom) instance Funlike-Marked-graph-hom : Funlike (Marked-graph-hom G H) β G β Ξ» _ β β H β Funlike-Marked-graph-hom .Funlike._#_ = vertex Marked-graph-hom-pathp : {G : I β Marked-graph o β} {H : I β Marked-graph o' β'} β {f : Marked-graph-hom (G i0) (H i0)} {g : Marked-graph-hom (G i1) (H i1)} β (p0 : β (x : β i β G i .Vertex) β PathP (Ξ» i β H i .Vertex) (f .vertex (x i0)) (g .vertex (x i1))) β (p1 : β {x y : β i β G i .Vertex} β (e : β i β G i .Edge (x i) (y i)) β PathP (Ξ» i β H i .Edge (p0 x i) (p0 y i)) (f .edge (e i0)) (g .edge (e i1))) β PathP (Ξ» i β Marked-graph-hom (G i) (H i)) f g Marked-graph-hom-pathp {G = G} {H = H} {f = f} {g = g} p0 p1 = comm-path where hom-path : PathP (Ξ» i β Graph-hom (G i .graph) (H i .graph)) (f .hom) (g .hom) hom-path = Graph-hom-pathp {G = Ξ» i β G i .graph} {H = Ξ» i β H i .graph} {f = f .hom} {g .hom} p0 p1 comm-path : PathP (Ξ» i β Marked-graph-hom (G i) (H i)) f g comm-path i .hom = hom-path i comm-path i .pres-marked {x} {y} {p} {q} = is-propβpathp (Ξ» i β Ξ -is-hlevel {A = G i .Vertex} 1 Ξ» x β Ξ -is-hlevel {A = G i .Vertex} 1 Ξ» y β Ξ -is-hlevel {A = Path-in (G i .graph) x y} 1 Ξ» p β Ξ -is-hlevel {A = Path-in (G i .graph) x y} 1 Ξ» q β Ξ -is-hlevel {A = β£ G i .Marked p q β£} 1 Ξ» _ β H i .Marked (path-map (hom-path i) p) (path-map (hom-path i) q) .is-tr) (Ξ» _ _ _ _ β f .pres-marked) (Ξ» _ _ _ _ β g .pres-marked) i x y p q Marked-graph-hom-path : {f g : Marked-graph-hom G H} β (p0 : β x β f .vertex x β‘ g .vertex x) β (p1 : β {x y} β (e : G .Edge x y) β PathP (Ξ» i β H .Edge (p0 x i) (p0 y i)) (f .edge e) (g .edge e)) β f β‘ g Marked-graph-hom-path {G = G} {H = H} p0 p1 = Marked-graph-hom-pathp {G = Ξ» _ β G} {H = Ξ» _ β H} (Ξ» x i β p0 (x i) i) (Ξ» e i β p1 (e i) i)

We can organize marked graphs and their homomorphisms into a category $MarkedGraphs.$

Marked-graphs : β o β β Precategory (lsuc o β lsuc β) (o β β) Marked-graphs o β .Precategory.Ob = Marked-graph o β Marked-graphs o β .Precategory.Hom = Marked-graph-hom

## Composition, identities, and their corresponding equations are a bit tedious, so we omit the details.

Marked-graphs o β .Precategory.Hom-set _ _ = hlevel 2 Marked-graphs o β .Precategory.id {G} .hom = Graphs.id Marked-graphs o β .Precategory.id {G} .pres-marked p~q = substβ (Ξ» p q β β£ G .Marked p q β£) (sym (path-map-id _)) (sym (path-map-id _)) p~q Marked-graphs o β .Precategory._β_ f g .hom = (f .hom) Graphs.β (g .hom) Marked-graphs o β .Precategory._β_ {G} {H} {K} f g .pres-marked p~q = substβ (Ξ» p q β β£ K .Marked p q β£) (sym (path-map-β _)) (sym (path-map-β _)) (f .pres-marked (g .pres-marked p~q)) Marked-graphs o β .Precategory.idr _ = Marked-graph-hom-path (Ξ» _ β refl) (Ξ» _ β refl) Marked-graphs o β .Precategory.idl _ = Marked-graph-hom-path (Ξ» _ β refl) (Ξ» _ β refl) Marked-graphs o β .Precategory.assoc _ _ _ = Marked-graph-hom-path (Ξ» _ β refl) (Ξ» _ β refl)

Moreover, there is a faithful functor from the category of strict categories to the category of marked graphs.

Strict-catsβͺMarked-graphs : Functor (Strict-cats o β) (Marked-graphs o β)

The action on objects takes a strict category $C$ to its underlying graph, and adds a marked pair between $p,q:C_{β}$ whenever $p$ and $q$ are equal as morphisms in $C.$

Strict-catsβͺMarked-graphs .Fβ C .graph = Strict-catsβͺGraphs .Fβ C Strict-catsβͺMarked-graphs .Fβ C .Marked p q = elΞ© (path-reduce C p β‘ path-reduce C q)

Functoriality follows from the fact that functors take equal paths in $C$ to equal paths in $D.$

Strict-catsβͺMarked-graphs .Fβ F .hom = Strict-catsβͺGraphs .Fβ F Strict-catsβͺMarked-graphs .Fβ F .pres-marked {p = p} {q = q} = β‘-map Ξ» p~q β path-reduce-natural F p β ap (F .Fβ) p~q β sym (path-reduce-natural F q) Strict-catsβͺMarked-graphs .F-id = Marked-graph-hom-path (Ξ» _ β refl) (Ξ» _ β refl) Strict-catsβͺMarked-graphs .F-β F G = Marked-graph-hom-path (Ξ» _ β refl) (Ξ» _ β refl)

This functor is clearly faithful; the proof is essentially just relabeling data.

Strict-catsβͺMarked-graphs-faithful : is-faithful (Strict-catsβͺMarked-graphs {o} {β}) Strict-catsβͺMarked-graphs-faithful p = Functor-path (Ξ» x i β p i .vertex x) (Ξ» f i β p i .edge f)

More surprisingly this functor is also full!

Strict-catsβͺMarked-graphs-full : is-full (Strict-catsβͺMarked-graphs {o} {β})

To see why, suppose that $f:CβD$ is a marked graph homomorphism between strict categories. By definition, $f$ already contains the data of a functor; the tricky part is showing that this data is functorial.

Strict-catsβͺMarked-graphs-full {x = C} {y = D} f = pure (functor , Marked-graph-hom-path (Ξ» _ β refl) (Ξ» _ β refl)) where module C = Precategory (C .fst) module D = Precategory (D .fst) functor : Functor (C .fst) (D .fst) functor .Fβ = f .vertex functor .Fβ = f .edge

The trick is that marked graph homomorphisms between categories cannot observe the intensional structure of paths, as they must preserve all marked pairs. In particular, $f$ will preserve the makred pair consisting of $[id]$ and the empty path; so $f(id)=id$

functor .F-id = f .edge C.id β‘Λβ¨ D.idl _ β©β‘Λ D.id D.β f .edge C.id β‘β¨ β‘-out! (f .pres-marked {p = cons C.id nil} {q = nil} (inc (C.idl _))) β©β‘ D.id β

Additionally, $f$ will preserve the marked pair consisting of the singleton path $[gβh]$ and the path $[h,g],$ so $f(gβh)=fgβfh.$

functor .F-β g h = f .edge (g C.β h) β‘Λβ¨ D.idl _ β©β‘Λ D.id D.β f .edge (g C.β h) β‘Λβ¨ β‘-out! (f .pres-marked {p = cons h (cons g nil)} {q = cons (g C.β h) nil} (pure (sym (C.assoc _ _ _)))) β©β‘Λ (D.id D.β f .edge g) D.β f .edge h β‘β¨ apβ D._β_ (D.idl _) refl β©β‘ f .edge g D.β f .edge h β

## Categories from generators and relationsπ

In this section, we will detail how to freely construct a category from a marked graph $G.$ Intuitvely, this works by freely generating a category from $G,$ and then identifying all marked pairs. However, there is a slight subtlety here: the marked pairs of $G$ may not respect path concatenation, and may not even form an equivalence relation!

Luckily, there is an easy (though tedious) solution to this problem: we can instead quotient by the reflexive-transitive-congruent closure instead, which we encode in Agda via the following higher-inductive type.

data Marking : β {x y} β Path-in G.graph x y β Path-in G.graph x y β Type (o β β) where marked : β {x y} {p q : Path-in G.graph x y} β β£ G.Marked p q β£ β Marking p q reflexive : β {x y} {p : Path-in G.graph x y} β Marking p p symmetric : β {x y} {p q : Path-in G.graph x y} β Marking q p β Marking p q transitive : β {x y} {p q r : Path-in G.graph x y} β Marking p q β Marking q r β Marking p r congruent : β {x y z} {p q : Path-in G.graph x y} {r s : Path-in G.graph y z} β Marking p q β Marking r s β Marking (p ++ r) (q ++ s) trunc : β {x y} {p q : Path-in G.graph x y} β is-prop (Marking p q)

The resulting category is not too difficult to construct: the objects are the vertices of $G,$ and the morphisms are paths in $G$ quotiented by the aforementioned closure.

Marked-path-category : Precategory o (o β β) Marked-path-category .Precategory.Ob = G.Vertex Marked-path-category .Precategory.Hom x y = Path-in G.graph x y / Marking Marked-path-category .Precategory.Hom-set _ _ = hlevel 2 Marked-path-category .Precategory.id = inc nil Marked-path-category .Precategory._β_ = Quot-opβ (Ξ» _ β reflexive) (Ξ» _ β reflexive) (flip _++_) (Ξ» p q r s p~q r~s β congruent r~s p~q) Marked-path-category .Precategory.idr = elim! Ξ» p β refl Marked-path-category .Precategory.idl = elim! Ξ» p β ap inc (++-idr p) Marked-path-category .Precategory.assoc = elim! Ξ» p q r β ap inc (++-assoc r q p)

Proving that this construction is free involves a bit more work.

We start with a useful lemma. Let $C$ be an arbitrary strict category, $G$ a marked graph, and $f:GβC$ a marked graph homomorphism. If $p,q$ are related by the marked closure of $G,$ then folding $f$ over $p$ and $q$ results in the same morphism.

module _ (C : Ξ£ (Precategory o β) is-strict) where private module C = Cat.Reasoning (C .fst) β£Cβ£ : Marked-graph o β β£Cβ£ = Strict-catsβͺMarked-graphs .Fβ C path-fold-marking : (f : Marked-graph-hom G β£Cβ£) β β {x y} (p q : Path-in (G .graph) x y) β Marking G p q β path-fold C (f .hom) p β‘ path-fold C (f .hom) q

The proof is an easy but tedious application of the elimination
principle of `Marking`

.

path-fold-marking {G = G} f p q = Marking-elim-prop G {P = Ξ» {x} {y} {p} {q} _ β path-fold C (f .hom) p β‘ path-fold C (f .hom) q} (Ξ» _ β hlevel 1) (Ξ» {_} {_} {p} {q} p~q β sym (path-reduce-map p) β β‘-out! (f .pres-marked p~q) β path-reduce-map q) refl (Ξ» _ β sym) (Ξ» _ p=q _ q=r β p=q β q=r) (Ξ» {_} {_} {_} {p} {q} {r} {s} _ p=q _ r=s β path-fold-++ C p r β apβ C._β_ r=s p=q β sym (path-fold-++ C q s))

This lemma lets us extend folds over paths to folds over quotiented paths.

comm-path-fold : (f : Marked-graph-hom G β£Cβ£) β β {x y} β Path-in (G .graph) x y / Marking G β C.Hom (f .vertex x) (f .vertex y) comm-path-fold f = Quot-elim (Ξ» _ β hlevel 2) (path-fold C (f .hom)) (path-fold-marking f)

Moreover, this extends to a functor from the free category over $G$ to $C.$

MarkedF : Marked-graph-hom G β£Cβ£ β Functor (Marked-path-category G) (C .fst) MarkedF f .Fβ = f .vertex MarkedF f .Fβ = comm-path-fold f MarkedF f .F-id = refl MarkedF f .F-β = elim! Ξ» p q β path-fold-++ C q p

Like path categories, functors out of marked path categories are purely characterized by their behaviour on edges.

Marked-path-category-functor-path : {F F' : Functor (Marked-path-category G) C} β (p0 : β x β F .Fβ x β‘ F' .Fβ x) β (p1 : β {x y} (e : G .Edge x y) β PathP (Ξ» i β C.Hom (p0 x i) (p0 y i)) (F .Fβ (inc (cons e nil))) (F' .Fβ (inc (cons e nil)))) β F β‘ F'

## Like the analogous result for path categories, this proof involves some cubical yoga which we will hide from the innocent reader.

Marked-path-category-functor-path {G = G} {F = F} {F' = F'} p0 p1 = Functor-path p0 (elim! p1-paths) where p1-paths : β {x y} β (p : Path-in (G .graph) x y) β PathP (Ξ» i β C.Hom (p0 x i) (p0 y i)) (F .Fβ (inc p)) (F' .Fβ (inc p)) p1-paths {x = x} nil i = hcomp (β i) Ξ» where j (i = i0) β F .F-id (~ j) j (i = i1) β F' .F-id (~ j) j (j = i0) β C.id p1-paths (cons e p) i = hcomp (β i) Ξ» where j (i = i0) β F .F-β (inc p) (inc (cons e nil)) (~ j) j (i = i1) β F' .F-β (inc p) (inc (cons e nil)) (~ j) j (j = i0) β p1-paths p i C.β p1 e i

With these results in hand, we can return to our original goal of showing that the marked path category on $G$ is a free object relative to the underlying marked graph functor.

Marked-free-category : β (G : Marked-graph β β) β Free-object Strict-catsβͺMarked-graphs G Marked-free-category G .Free-object.free = Marked-path-category G , hlevel 2

The unit of the free object takes vertices to themselves, and edges to singleton paths. We need to do a bit of work to show that this construction preserves markings but itβs not too difficult.

Marked-free-category G .Free-object.unit = unit-comm where G* : Ξ£ (Precategory _ _) is-strict G* = Marked-path-category G , hlevel 2 β£G*β£ : Graph _ _ β£G*β£ = Strict-catsβͺGraphs .Fβ G* unit : Graph-hom (G .graph) β£G*β£ unit .Graph-hom.vertex x = x unit .Graph-hom.edge e = inc (cons e nil) unit-comm : Marked-graph-hom G (Strict-catsβͺMarked-graphs .Fβ G*) unit-comm .hom = unit unit-comm .pres-marked {p = p} {q = q} p~q = pure $ path-reduce G* (path-map unit p) β‘β¨ path-reduce-map p β©β‘ path-fold G* unit p β‘Λβ¨ path-fold-unique G* inc refl (Ξ» _ _ β refl) p β©β‘Λ inc p β‘β¨ quot (marked p~q) β©β‘ inc q β‘β¨ path-fold-unique G* inc refl (Ξ» _ _ β refl) q β©β‘ path-fold G* unit q β‘Λβ¨ path-reduce-map q β©β‘Λ path-reduce G* (path-map unit q) β

Weβve already put in the work for the universal property: all that we need to do is assemble previous results!

Marked-free-category G .Free-object.fold {Y = C} f = MarkedF C f Marked-free-category G .Free-object.commute {Y = C} = Marked-graph-hom-path (Ξ» _ β refl) (Ξ» _ β idl _) where open Precategory (C .fst) Marked-free-category G .Free-object.unique {Y = C} F p = Marked-path-category-functor-path (Ξ» x i β p i .vertex x) (Ξ» e β to-pathp (from-pathp (Ξ» i β p i .edge e) β sym (idl _))) where open Precategory (C .fst)

Marked-free-categories : Functor (Marked-graphs β β) (Strict-cats β β) Marked-free-categories = free-objectsβfunctor Marked-free-category Marked-free-categoriesβ£Underlying-marked-graph : Marked-free-categories {β} β£ Strict-catsβͺMarked-graphs Marked-free-categoriesβ£Underlying-marked-graph = free-objectsβleft-adjoint Marked-free-category

This means that the category of strict categories is a reflective subcategory of the category of marked graphs. In more intuitive terms, that we can think about strict categories as algebraic structure placed atop a marked graph, as inclusions from reflective subcategories are monadic!

Marked-free-categoriesβ£Underlying-marked-graph-reflective : is-reflective (Marked-free-categoriesβ£Underlying-marked-graph {β}) Marked-free-categoriesβ£Underlying-marked-graph-reflective = full+faithfulβff Strict-catsβͺMarked-graphs Strict-catsβͺMarked-graphs-full Strict-catsβͺMarked-graphs-faithful