module Cat.Instances.Free where

Graphs and free categoriesπŸ”—

A graph (really, an (o,β„“)(o, \ell)-graph1) is given by a set V:SetsoV : \mathbf{Sets}_o of vertices and, for each pair of elements x,y:Vx, y : V, a set of edges E(x,y):Setsβ„“E(x, y) : \mathbf{Sets}_\ell from xx to yy. That’s it: a set VV and a family of sets over VΓ—VV \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
    vert : Set o
    edge : ∣ vert ∣ β†’ ∣ vert ∣ β†’ Set β„“

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

  • The objects of Path(G)\mathrm{Path}(G) are the vertices of GG
  • The morphisms in Path(G)\mathrm{Path}(G) are given by finite paths in GG. 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→ca \to c by starting with a path b→cb \to c and precomposing with an edge (a→b):G(a \to b) : G. Much of the code below is dedicated to characterising the identity types between paths. Indeed, to construct a category Path(G)\mathrm{Path}(G), we must show that paths in GG form a set.

We have a couple of options here:

  • We can construct paths by recursion, on their length: Defining a β€œpath from xx to yy of length nn” by recursion on nn, and then defining a path from xx to yy as being a pair (n,xs)(n, xs) where n:Nn : \N$ and xsxs is a path of length nn;

  • 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β†’yxs : x \to y really encodes the empty path, and we have an identity of vertices x≑yx \equiv y. We can do this by recursion: If xsxs 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 Code(xs,ys)\mathrm{Code}(xs, ys), standing for an identification of paths xs≑ysxs \equiv ys. But observe what happens in the case where we’ve built up a path aβ†’ca \to c by adding an edge: We know that the edges start at aa, and the inner paths end at cc, but the inner vertex may vary!

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

    : βˆ€ (a : I β†’ ∣ G.vert ∣) {c}
    β†’ Path-in (a i0) c
    β†’ Path-in (a i1) c
    β†’ Type (o βŠ” β„“)

Note that in the case where xs=nilxs = \mathrm{nil}, Agda refines bb to be definitionally aa, and we can no longer match on the right-hand-side path ysys. That’s where the is-nil predicate comes in: We say that ysys is equal to nil\mathrm{nil} if is-nil ysys 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≑nilxs \equiv \mathrm{nil}, but it must be over an arbitrary identification pp3. Fortunately, vertices in a graph GG live in a set, so pp is reflexivity.

    : βˆ€ (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.

    : βˆ€ (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 _ _ _ _) $
      (is-prop→pathp (λ i → PathP-is-hlevel' 1 (G.edge _ _ .is-tr) _ _) q q′)
        (Ξ» 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 aa to bb 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

    : βˆ€ {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

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)

    : βˆ€ {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)) j
    rem₁ {x = x} im = go im (im refl (path-decode (im .Pc.invr)) where
      go : βˆ€ {y} (im : Pc.Isomorphism x y) (jβ€² : Path-in x y) β†’ jβ€² ≑ im
         β†’ path-codep (Ξ» _ β†’ x) (jβ€² ++ im .Pc.from) nil
         β†’ Ξ£ (x ≑ y) Ξ» p β†’ PathP (Ξ» i β†’ Pc.Isomorphism x (p i)) 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!

  1. and, even more pedantically, a directed multi-(o,β„“)(o, β„“)-graphβ†©οΈŽ

  2. for xs:aβ†’bxs : a \to b an arbitrary pathβ†©οΈŽ

  3. which we know is a loop a=aa = aβ†©οΈŽ