open import 1Lab.Path.Cartesian
open import 1Lab.Reflection

open import Cat.Instances.StrictCat
open import Cat.Functor.Properties
open import Cat.Functor.Base
open import Cat.Prelude
open import Cat.Strict

import Cat.Reasoning

module Cat.Instances.Graphs where

private variable
  o o' β„“ β„“' : Level

The category of graphsπŸ”—

A graph (really, an 1) is given by a set of vertices and, for each pair of elements a set of edges from to That’s it: a set and a family of sets over 

record Graph (o β„“ : Level) : Type (lsuc o βŠ” lsuc β„“) where
  no-eta-equality
  field
    Vertex : Type o
    Edge : Vertex β†’ Vertex β†’ Type β„“
    Vertex-is-set : is-set Vertex
    Edge-is-set : βˆ€ {x y} β†’ is-set (Edge x y)

open Graph
open hlevel-projection

instance
  Underlying-Graph : Underlying (Graph o β„“)
  Underlying-Graph = record { ⌞_⌟ = Graph.Vertex }

  hlevel-proj-vertex : hlevel-projection (quote Graph.Vertex)
  hlevel-proj-vertex .has-level = quote Graph.Vertex-is-set
  hlevel-proj-vertex .get-level _ = pure (quoteTerm (suc (suc zero)))
  hlevel-proj-vertex .get-argument (_ ∷ _ ∷ c v∷ _) = pure c
  {-# CATCHALL #-}
  hlevel-proj-vertex .get-argument _ = typeError []

  hlevel-proj-edge : hlevel-projection (quote Graph.Edge)
  hlevel-proj-edge .has-level = quote Graph.Edge-is-set
  hlevel-proj-edge .get-level _ = pure (quoteTerm (suc (suc zero)))
  hlevel-proj-edge .get-argument (_ ∷ _ ∷ c v∷ _) = pure c
  {-# CATCHALL #-}
  hlevel-proj-edge .get-argument _ = typeError []

A graph homomorphism consists of a mapping of vertices along with a mapping of edges 

record Graph-hom (G : Graph o β„“) (H : Graph o' β„“') : Type (o βŠ” o' βŠ” β„“ βŠ” β„“') where
  no-eta-equality
  field
    vertex : ⌞ G ⌟ β†’ ⌞ H ⌟
    edge : βˆ€ {x y} β†’ G .Edge x y β†’ H .Edge (vertex x) (vertex y)

private variable
  G H K : Graph o β„“

open Graph-hom

unquoteDecl H-Level-Graph-hom = declare-record-hlevel 2 H-Level-Graph-hom (quote Graph-hom)

Graph-hom-pathp
  : {G : I β†’ Graph o β„“} {H : I β†’ Graph o' β„“'}
  β†’ {f : Graph-hom (G i0) (H i0)} {g : 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 β†’ Graph-hom (G i) (H i)) f g
Graph-hom-pathp {G = G} {H = H} {f = f} {g = g} p0 p1 = pathp where
  vertex* : I β†’ Type _
  vertex* i = (G i) .Vertex

  edge* : (i : I) β†’ vertex* i β†’ vertex* i β†’ Type _
  edge* i x y = (G i) .Edge x y

  pathp : PathP (Ξ» i β†’ Graph-hom (G i) (H i)) f g
  pathp i .vertex x = p0 (Ξ» j β†’ coe vertex* i j x) i
  pathp i .edge {x} {y} e =
    p1 {x = Ξ» j β†’ coe vertex* i j x} {y = Ξ» j β†’ coe vertex* i j y}
      (Ξ» j β†’ coe (Ξ» j β†’ edge* j (coe vertex* i j x) (coe vertex* i j y)) i j (e* j)) i
    where

      x* y* : (j : I) β†’ vertex* i
      x* j = coeiβ†’i vertex* i x (~ j ∨ i)
      y* j = coeiβ†’i vertex* i y (~ j ∨ i)

      e* : (j : I) β†’ edge* i (coe vertex* i i x) (coe vertex* i i y)
      e* j =
        comp (Ξ» j β†’ edge* i (x* j) (y* j)) ((~ i ∧ ~ j) ∨ (i ∧ j)) Ξ» where
          k (k = i0) β†’ e
          k (i = i0) (j = i0) β†’ e
          k (i = i1) (j = i1) β†’ e

Graph-hom-path
  : {f g : Graph-hom G H}
  β†’ (p0 : βˆ€ x β†’ f .vertex x ≑ g .vertex x)
  β†’ (p1 : βˆ€ {x y} β†’ (e : Graph.Edge G x y) β†’ PathP (Ξ» i β†’ Graph.Edge H (p0 x i) (p0 y i)) (f .edge e) (g .edge e))
  β†’ f ≑ g
Graph-hom-path {G = G} {H = H} p0 p1 =
  Graph-hom-pathp {G = Ξ» _ β†’ G} {H = Ξ» _ β†’ H}
    (Ξ» x i β†’ p0 (x i) i)
    (Ξ» e i β†’ p1 (e i) i)

instance
  Funlike-Graph-hom : Funlike (Graph-hom G H) ⌞ G ⌟ Ξ» _ β†’ ⌞ H ⌟
  Funlike-Graph-hom .Funlike._#_ = vertex

Graphs and graph homomorphisms can be organized into a category 

Graphs : βˆ€ o β„“ β†’ Precategory (lsuc (o βŠ” β„“)) (o βŠ” β„“)
Graphs o β„“ .Precategory.Ob = Graph o β„“
Graphs o β„“ .Precategory.Hom = Graph-hom
Graphs o β„“ .Precategory.Hom-set _ _ = hlevel 2
Graphs o β„“ .Precategory.id .vertex v = v
Graphs o β„“ .Precategory.id .edge e = e
Graphs o β„“ .Precategory._∘_ f g .vertex v = f .vertex (g .vertex v)
Graphs o β„“ .Precategory._∘_ f g .edge e = f .edge (g .edge e)
Graphs o β„“ .Precategory.idr _ = Graph-hom-path (Ξ» _ β†’ refl) (Ξ» _ β†’ refl)
Graphs o β„“ .Precategory.idl _ = Graph-hom-path (Ξ» _ β†’ refl) (Ξ» _ β†’ refl)
Graphs o β„“ .Precategory.assoc _ _ _ = Graph-hom-path (Ξ» _ β†’ refl) (Ξ» _ β†’ refl)

module Graphs {o} {β„“} = Cat.Reasoning (Graphs o β„“)

open Functor

Note that every strict category has an underlying graph, where the vertices are given by objects, and edges by morphisms. Moreover, functors between strict categories give rise to graph homomorphisms between underlying graphs. This gives rise to a functor from the category of strict categories to the category of graphs.

Strict-catsβ†ͺGraphs : Functor (Strict-cats o β„“) (Graphs o β„“)
Strict-catsβ†ͺGraphs .Fβ‚€ (C , C-strict) .Vertex = Precategory.Ob C
Strict-catsβ†ͺGraphs .Fβ‚€ (C , C-strict) .Edge = Precategory.Hom C
Strict-catsβ†ͺGraphs .Fβ‚€ (C , C-strict) .Vertex-is-set = C-strict
Strict-catsβ†ͺGraphs .Fβ‚€ (C , C-strict) .Edge-is-set = Precategory.Hom-set C _ _
Strict-catsβ†ͺGraphs .F₁ F .vertex = F .Fβ‚€
Strict-catsβ†ͺGraphs .F₁ F .edge = F .F₁
Strict-catsβ†ͺGraphs .F-id = Graph-hom-path (Ξ» _ β†’ refl) (Ξ» _ β†’ refl)
Strict-catsβ†ͺGraphs .F-∘ F G = Graph-hom-path (Ξ» _ β†’ refl) (Ξ» _ β†’ refl)

The underlying graph functor is faithful, as functors are graph homomorphisms with extra properties.

Strict-catsβ†ͺGraphs-faithful : is-faithful (Strict-catsβ†ͺGraphs {o} {β„“})
Strict-catsβ†ͺGraphs-faithful p =
  Functor-path
    (Ξ» x i β†’ p i .vertex x)
    (Ξ» e i β†’ p i .edge e)

  1. and, even more pedantically, a directed multi-β†©οΈŽ