↑ Top


Graph Structures

This is the Structures.Graphs module of the Agda Universal Algebra Library.

N.B. This module differs from 0Graphs.lagda in that this module is universe polymorphic; i.e., we do not restrict universe levels (to, e.g., β„“β‚€). This complicates some things; e.g., we must use lift and lower in some places (cf. 0Graphs.lagda).

Definition (Graph of a structure). Let 𝑨 be an (𝑅,𝐹)-structure (relations from 𝑅 and operations from 𝐹). The graph of 𝑨 is the structure Gr 𝑨 with the same domain as 𝑨 with relations from 𝑅 and together with a (k+1)-ary relation symbol G 𝑓 for each 𝑓 ∈ 𝐹 of arity k, which is interpreted in Gr 𝑨 as all tuples (t , y) ∈ Aᡏ⁺¹ such that 𝑓 t ≑ y. (See also Definition 2 of https://arxiv.org/pdf/2010.04958v2.pdf)

{-# OPTIONS --without-K --exact-split --safe #-}

module Structures.Graphs where

-- imports from Agda and the Agda Standard Library -------------------------------------------
open import Agda.Primitive using ( _βŠ”_ ; lsuc ) renaming ( Set to Type ; lzero  to β„“β‚€ )
open import Data.Product   using ( _,_ ; Ξ£-syntax ; _Γ—_ )
open import Data.Sum.Base  using ( _⊎_ ) renaming ( inj₁ to inl ; injβ‚‚ to inr )
open import Data.Unit.Base using ( ⊀ ; tt )
open import Level          using ( Level ; Lift ; lift ; lower )
open import Function.Base  using ( _∘_  )
open import Relation.Binary.PropositionalEquality
                           using ( _≑_ ; refl ; module ≑-Reasoning ; cong ; sym )

-- Imports from the Agda Universal Algebra Library ---------------------------------------------
open import Overture.Preliminaries   using ( ∣_∣ ; _β‰ˆ_ ; βˆ₯_βˆ₯ ; _βˆ™_ ; lower∼lift ; lift∼lower )
open import Relations.Continuous     using ( Rel )
open import Structures.Basic         using ( signature ; structure )
open import Examples.Structures.Signatures
                                     using ( Sβˆ… )
open import Structures.Homs          using ( hom ; 𝒾𝒹 ; ∘-hom ; 𝓁𝒾𝒻𝓉 ; π“β„΄π“Œβ„―π“‡ ; is-hom-rel; is-hom-op)

open signature
open structure
open _⊎_


Gr-sig : signature β„“β‚€ β„“β‚€ β†’ signature β„“β‚€ β„“β‚€ β†’ signature β„“β‚€ β„“β‚€

Gr-sig 𝐹 𝑅 = record { symbol = symbol 𝑅 ⊎ symbol 𝐹
                    ; arity  = ar }
 where
 ar : symbol 𝑅 ⊎ symbol 𝐹 β†’ Type _
 ar (inl π‘Ÿ) = (arity 𝑅) π‘Ÿ
 ar (inr 𝑓) = (arity 𝐹) 𝑓 ⊎ ⊀

private variable
 𝐹 𝑅 : signature β„“β‚€ β„“β‚€
 α ρ : Level

Gr : βˆ€{Ξ± ρ} β†’ structure 𝐹 𝑅 {Ξ±} {ρ} β†’ structure Sβˆ… (Gr-sig 𝐹 𝑅) {Ξ±} {Ξ± βŠ” ρ}
Gr {𝐹}{𝑅}{Ξ±}{ρ} 𝑨 = record { carrier = carrier 𝑨 ; op = Ξ» () ; rel = split }
  where
  split : (s : symbol 𝑅 ⊎ symbol 𝐹) β†’ Rel (carrier 𝑨) (arity (Gr-sig 𝐹 𝑅) s) {Ξ± βŠ” ρ}
  split (inl π‘Ÿ) arg = Lift Ξ± (rel 𝑨 π‘Ÿ arg)
  split (inr 𝑓) args = Lift ρ (op 𝑨 𝑓 (args ∘ inl) ≑ args (inr tt))


open ≑-Reasoning

private variable
 ρᡃ Ξ² ρᡇ : Level

module _ {𝑨 : structure 𝐹 𝑅 {Ξ±} {ρᡃ}}
         {𝑩 : structure 𝐹 𝑅 {Ξ²} {ρᡇ}} where

 homβ†’Grhom : hom 𝑨 𝑩 β†’ hom (Gr 𝑨) (Gr 𝑩)
 hom→Grhom (h , hhom) = h , (i , ii)
  where
  i : is-hom-rel (Gr 𝑨) (Gr 𝑩) h
  i (inl π‘Ÿ) a x = lift (∣ hhom ∣ π‘Ÿ a (lower x))
  i (inr 𝑓) a x = lift goal
   where
   homop : h (op 𝑨 𝑓 (a ∘ inl)) ≑ op 𝑩 𝑓 (h ∘ (a ∘ inl))
   homop = βˆ₯ hhom βˆ₯ 𝑓 (a ∘ inl)

   goal : op 𝑩 𝑓 (h ∘ (a ∘ inl)) ≑ h (a (inr tt))
   goal = op 𝑩 𝑓 (h ∘ (a ∘ inl)) β‰‘βŸ¨ sym homop ⟩
          h (op 𝑨 𝑓 (a ∘ inl))   β‰‘βŸ¨ cong h (lower x) ⟩
          h (a (inr tt))         ∎

  ii : is-hom-op (Gr 𝑨) (Gr 𝑩) h
  ii = Ξ» ()

 Grhomβ†’hom : hom (Gr 𝑨) (Gr 𝑩) β†’ hom 𝑨 𝑩
 Grhom→hom (h , hhom) = h , (i , ii)
  where
  i : is-hom-rel 𝑨 𝑩 h
  i R a x = lower (∣ hhom ∣ (inl R) a (lift x))
  ii : is-hom-op 𝑨 𝑩 h
  ii f a = goal -- goal
   where
   split : arity 𝐹 f ⊎ ⊀ β†’ carrier 𝑨
   split (inl x) = a x
   split (inr y) = op 𝑨 f a
   goal : h (op 𝑨 f a) ≑ op 𝑩 f (Ξ» x β†’ h (a x))
   goal = sym (lower (∣ hhom ∣ (inr f) split (lift refl)))


← Structures.Basic Structures.Graphs0 β†’