module Cat.Instances.Graphs.Limits where
Limits of graphs🔗
We can compute limits in the category of graphs pointwise, i.e. by letting both the nodes and edges be the limit of same shape in the category This follows from being a category of presheaves, but constructing these directly gives us a nicer description of the resulting adjacency.
The categorical product of graphs should not be confused with the box product of graphs, even though the box product may occasionally (e.g. on Wikipedia) be called the “Cartesian product” of graphs!
_×ᴳ_ : Graph o ℓ → Graph o' ℓ' → Graph _ _ (G ×ᴳ H) .Node = ⌞ G ⌟ × ⌞ H ⌟ (G ×ᴳ H) .Edge (a , x) (b , y) = G .Edge a b × H .Edge x y (G ×ᴳ H) .Node-set = hlevel 2 (G ×ᴳ H) .Edge-set = hlevel 2
The terminal graph has a point and a loop on that point.
⊤ᴳ : Graph o ℓ ⊤ᴳ .Node = Lift _ ⊤ ⊤ᴳ .Edge _ _ = Lift _ ⊤ ⊤ᴳ .Node-set = hlevel 2 ⊤ᴳ .Edge-set = hlevel 2
We note that dependent types introduce a slight complication in defining pullbacks of graphs: if one has an edge and their images under graph homomorphisms and live in different types, namely and However, since we are defining adjacency in the pullback of and we have, by assumption, identities and We can thus compare and over these.
_⊓ᴳ_ : Graph-hom X Z → Graph-hom Y Z → Graph _ _ _⊓ᴳ_ {X = X} {Z = Z} {Y = Y} f g .Node = Σ[ x ∈ X ] Σ[ y ∈ Y ] f · x ≡ g · y _⊓ᴳ_ {X = X} {Z = Z} {Y = Y} f g .Edge (a , x , p) (b , y , q) = Σ[ α ∈ X .Edge a b ] Σ[ ξ ∈ Y .Edge x y ] PathP (λ i → Z .Edge (p i) (q i)) (f .edge α) (g .edge ξ) _⊓ᴳ_ {X = X} {Z = Z} {Y = Y} f g .Node-set = hlevel 2 _⊓ᴳ_ {X = X} {Z = Z} {Y = Y} f g .Edge-set = hlevel 2
Showing that these constructions satisfy the appropriate universal property is simply an exercise in record construction, since, as mentioned, they are pointwise inherited from where the relevant equations mostly hold definitionally.
fstᴳ : Graph-hom (X ×ᴳ Y) X fstᴳ .node = fst fstᴳ .edge = fst sndᴳ : Graph-hom (X ×ᴳ Y) Y sndᴳ .node = snd sndᴳ .edge = snd Graphs-products : ∀ {o ℓ} → has-products (Graphs o ℓ) Graphs-products a b .apex = a ×ᴳ b Graphs-products a b .π₁ = fstᴳ Graphs-products a b .π₂ = sndᴳ Graphs-products a b .has-is-product .⟨_,_⟩ f g = record where node z = f .node z , g .node z edge z = f .edge z , g .edge z Graphs-products a b .has-is-product .π₁∘⟨⟩ = trivialᴳ! Graphs-products a b .has-is-product .π₂∘⟨⟩ = trivialᴳ! Graphs-products a b .has-is-product .unique p q = ext record where node x i = p i .node x , q i .node x edge e i = p i .edge e , q i .edge e Graphs-terminal : ∀ {o ℓ} → Terminal (Graphs o ℓ) Graphs-terminal .Terminal.top = ⊤ᴳ Graphs-terminal .Terminal.has⊤ x .centre .node = _ Graphs-terminal .Terminal.has⊤ x .centre .edge = _ Graphs-terminal .Terminal.has⊤ x .paths h = trivialᴳ! Graphs-pullbacks : ∀ {o ℓ} → has-pullbacks (Graphs o ℓ) Graphs-pullbacks f g .apex = f ⊓ᴳ g Graphs-pullbacks f g .p₁ .node (x , _ , _) = x Graphs-pullbacks f g .p₁ .edge (x , _ , _) = x Graphs-pullbacks f g .p₂ .node (_ , y , _) = y Graphs-pullbacks f g .p₂ .edge (_ , y , _) = y Graphs-pullbacks f g .has-is-pb .square = ext record where node _ _ p = p edge (_ , _ , p) = p Graphs-pullbacks f g .has-is-pb .universal {p₁' = p₁'} {p₂'} α = record where node x = p₁' .node x , p₂' .node x , λ i → α i .node x edge x = p₁' .edge x , p₂' .edge x , λ i → α i .edge x Graphs-pullbacks f g .has-is-pb .p₁∘universal = trivialᴳ! Graphs-pullbacks f g .has-is-pb .p₂∘universal = trivialᴳ! Graphs-pullbacks f g .has-is-pb .unique α β = ext record where node x = (λ i → α i .node x) ,ₚ (λ i → β i .node x) ,ₚ prop! edge x = (λ i → α i .edge x) ,ₚ (λ i → β i .edge x) ,ₚ prop! Graphs-finitely-complete : Finitely-complete (Graphs o ℓ) Graphs-finitely-complete = record { Finitely-complete (with-pullbacks (Graphs _ _) Graphs-terminal Graphs-pullbacks) hiding (products) ; products = Graphs-products } Graphs-cartesian : Cartesian-category (Graphs o ℓ) Graphs-cartesian = record { Finitely-complete Graphs-finitely-complete }