↑ Top


Equational Logic for General Structures

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


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

module 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 Base.Terms             using ( Term )
open import Base.Structures.Basic  using ( signature ; structure ; _ᵒ_ )
open import 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)


← Base.Structures.Substructures Base.Structures.Sigma →