Skip to content

Legacy.Base.Structures.EquationalLogic

Equational Logic for General Structures

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


{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Legacy.Base.Structures.EquationalLogic where

-- Imports from Agda and the Agda Standard Library --------------------------------------
open import Agda.Primitive  using () renaming ( Set to Type )
open import Data.Fin.Base   using ( Fin )
open import Data.Nat        using ( β„• )
open import Data.Product    using ( _Γ—_ ; _,_ ) renaming ( proj₁ to fst ; projβ‚‚ to snd )
open import Level           using ( Level )
open import Relation.Unary  using ( Pred ; _∈_ )

-- Imports from the Agda Universal Algebra Library --------------------------------------
open import Overture               using ( _β‰ˆ_ )
open import Legacy.Base.Terms             using ( Term )
open import Legacy.Base.Structures.Basic  using ( signature ; structure ; _α΅’_ )
open import Legacy.Base.Structures.Terms  using ( _⟦_⟧ )

private variable
 π“žβ‚€ π“₯β‚€ π“žβ‚ π“₯₁ Ο‡ Ξ± ρ β„“ : Level
 𝐹 : signature π“žβ‚€ π“₯β‚€
 𝑅 : signature π“žβ‚ π“₯₁
 X : Type Ο‡

-- Entailment, equational theories, and models

_⊧_β‰ˆ_ : structure 𝐹 𝑅 {Ξ±}{ρ} β†’ Term X β†’ Term X β†’ Type _
𝑨 ⊧ p β‰ˆ q = 𝑨 ⟦ p ⟧ β‰ˆ 𝑨 ⟦ q ⟧

_⊧_≋_ : Pred(structure 𝐹 𝑅 {Ξ±}{ρ}) β„“ β†’ Term X β†’ Term X β†’ Type _
𝒦 ⊧ p ≋ q = βˆ€{𝑨 : structure _ _} β†’ 𝒦 𝑨 β†’ 𝑨 ⊧ p β‰ˆ q

-- Theories
Th : Pred (structure 𝐹 𝑅{Ξ±}{ρ}) β„“ β†’ Pred(Term X Γ— Term X) _ -- (ℓ₁ βŠ” Ο‡)
Th 𝒦 = Ξ» (p , q) β†’ 𝒦 ⊧ p ≋ q

-- Models
Mod : Pred(Term X Γ— Term X) β„“  β†’ Pred(structure 𝐹 𝑅 {Ξ±} {ρ}) _  -- (Ο‡ βŠ” β„“β‚€)
Mod β„° = Ξ» 𝑨 β†’ βˆ€ p q β†’ (p , q) ∈ β„° β†’ 𝑨 ⊧ p β‰ˆ q

fMod : {n : β„•} β†’ (Fin n β†’ (Term X Γ— Term X)) β†’ Pred(structure 𝐹 𝑅 {Ξ±} {ρ}) _
fMod β„° = Ξ» 𝑨 β†’ βˆ€ i β†’ 𝑨 ⊧ fst (β„° i) β‰ˆ snd (β„° i)