 ### Graph Structures (again)

This is the Base.Structures.Graphs0 module of the Agda Universal Algebra Library.

N.B. This module differs from Graphs.lagda in that here we assume some universes are level zero (i.e., ℓ₀). This simplifies some things; e.g., we avoid having to use lift and lower (cf. Base/Structures/Graphs.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 Base.Structures.Graphs0 where

-- Imports from Agda and the Agda Standard Library -------------------------------------------
open import Agda.Primitive  using () 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.Fin.Base   using ( Fin )
open import Data.Nat        using ( ℕ )
open import Data.Unit.Base  using ( ⊤ ; tt )
open import Function.Base   using ( _∘_ )
open import Relation.Unary  using ( Pred ; _∈_ )
open import Relation.Binary.PropositionalEquality
using ( _≡_ ; module ≡-Reasoning ; cong ; sym ; refl )

-- Imports from the Agda Universal Algebra Library ---------------------------------------------
open import Overture                        using ( ∣_∣ ; ∥_∥ )
open import Base.Relations                  using ( Rel )
open import Base.Structures.Basic           using ( signature ; structure )
open import Base.Structures.Homs            using ( hom ; is-hom-rel ; is-hom-op )
open import Examples.Structures.Signatures  using ( S∅ )

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 ℓ₀ ℓ₀

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 = rel 𝑨 𝑟 arg
split (inr 𝑓) args = op 𝑨 𝑓 (args ∘ inl) ≡ args (inr tt)

open ≡-Reasoning

module _ {𝑨 𝑩 : 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 = ∣ hhom ∣ 𝑟 a x
i (inr 𝑓) a x = 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 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 = ∣ hhom ∣ (inl R) a x
ii : is-hom-op 𝑨 𝑩 h
ii f a = 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 (∣ hhom ∣ (inr f) split refl)

```

Lemma III.1. Let `𝑆` be a signature and `𝑨` be an `𝑆`-structure. Let `ℰ` be a finite set of identities such that `𝑨 ⊧ ℰ`. For every instance `𝑿` of CSP(`𝑨`), one can compute in polynomial time an instance `𝒀` of CSP(`𝑨`) such that `𝒀 ⊧ ℰ` and `| hom 𝑿 𝑨 | = | hom 𝒀 𝑨 |`.

Proof. `∀ s ≈ t` in `ℰ` and each tuple `b` such that `𝑩 ⟦ s ⟧ b ≢ 𝑩 ⟦ t ⟧ b`, one can compute the congruence `θ = Cg (𝑩 ⟦ s ⟧ b , 𝑩 ⟦ t ⟧ b)` generated by `𝑩 ⟦ s ⟧ b` and `𝑩 ⟦ t ⟧ b`. Let `𝑩₁ := 𝑩 / θ`, and note that `| 𝑩₁ | < | 𝑩 |`.

We show there exists a bijection from `hom 𝑩 𝑨` to `hom 𝑩₁ 𝑨`. Fix an `h : hom 𝑩 𝑨`. For all `s ≈ t` in `ℰ`, we have

`h (𝑩 ⟦ s ⟧ b) = 𝑨 ⟦ s ⟧ (h b) = 𝑨 ⟦ t ⟧ (h b) = h (𝑩 ⟦ t ⟧ b)`.

Therefore, `θ ⊆ ker h`, so `h` factors uniquely as `h = h' ∘ π : 𝑩 → (𝑩 / θ) → 𝑨`, where `π` is the canonical projection onto `𝑩 / θ`.

Thus the mapping `φ : hom 𝑩 𝑨 → hom 𝑩₁ 𝑨` that takes each `h` to `h'` such that `h = h' ∘ π` is injective. It is also surjective since each `g' : 𝑩 / θ → 𝑨` is mapped back to a `g : 𝑩 → 𝑨` such that `g = g' ∘ π`. Iterating over all identities in `ℰ`, possibly several times, at the final step we obtain a structure `𝑩ₙ` that satisfies `ℰ` and is such that `∣ hom 𝑩 𝑨 ∣ = ∣ hom 𝑩ₙ 𝑨 ∣`. Moreover, since the number of elements in the intermediate structures decreases at each step, `| 𝑩ᵢ₊₁ | < | 𝑩ᵢ |`, the process finishes in time that is bounded by a polynomial in the size of `𝑩`.

```record _⇛_⇚_ (𝑩 𝑨 𝑪 : structure 𝐹 𝑅) : Type ℓ₀ where
field
to   : hom 𝑩 𝑨 → hom 𝑪 𝑨
from : hom 𝑪 𝑨 → hom 𝑩 𝑨
to∼from : ∀ h → (to ∘ from) h ≡ h
from∼to : ∀ h → (from ∘ to) h ≡ h

-- TODO: formalize Lemma III.1
-- module _ {χ : Level}{X : Type χ}
--          {𝑨 : structure 𝐹 𝑅 {ℓ₀} {ℓ₀}} where
-- LEMMAIII1 : {n : ℕ}(ℰ : Fin n → (Term X × Term X))(𝑨 ∈ fMod ℰ)
--  →          ∀(𝑩 : structure 𝐹 𝑅) → Σ[ 𝑪 ∈ structure 𝐹 𝑅 ] (𝑪 ∈ fMod ℰ × (𝑩 ⇛ 𝑨 ⇚ 𝑪))
-- LEMMAIII1 ℰ 𝑨⊧ℰ 𝑩 = {!!} , {!!}
```