### 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 (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 (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)))

```