 Basic Definitions

This is the Structures.Basic module of the Agda Universal Algebra Library. It is a submodule of the Structures module which presents general (relational-algebraic) structures as inhabitants of record types. For a similar development using Sigma types see the Structures.Sigma.Basic module.

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

module Structures.Basic  where

-- Imports from Agda and the Agda Standard Library -----------------------------
open import Agda.Primitive       using ( _⊔_ ; lsuc ) renaming ( Set to Type )
open import Function.Base        using ( flip ; _∘_ )
open import Level                using ( Level ; Lift ; lift ; lower )
open import Relation.Binary.Core using () renaming ( Rel to BinRel )

-- Imports from the Agda Universal Algebra Library -----------------------------
open import Relations.Discrete     using ( Op ; _|:_ ; _preserves_ )
open import Relations.Continuous   using ( Rel )

private variable
𝓞₀ 𝓥₀ 𝓞₁ 𝓥₁ : Level

-- Signature as a record type
record signature (𝓞 𝓥 : Level) : Type (lsuc (𝓞  𝓥)) where
field
symbol : Type 𝓞
arity : symbol  Type 𝓥

siglˡ : {𝓞 𝓥 : Level}  signature 𝓞 𝓥  Level
siglˡ {𝓞}{𝓥} _ = 𝓞

siglʳ : {𝓞 𝓥 : Level}  signature 𝓞 𝓥  Level
siglʳ {𝓞}{𝓥} _ = 𝓥

sigl : {𝓞 𝓥 : Level}  signature 𝓞 𝓥  Level
sigl {𝓞}{𝓥} _ = 𝓞  𝓥

open signature public

record structure (𝐹 : signature 𝓞₀ 𝓥₀)(𝑅 : signature 𝓞₁ 𝓥₁)
{α : Level}{ρ : Level} : Type (𝓞₀  𝓥₀  𝓞₁  𝓥₁  (lsuc (α  ρ))) where
field
carrier : Type α
op  :  (f : symbol 𝐹)  Op  carrier (arity 𝐹 f)      -- interpret. of operations
rel :  (r : symbol 𝑅)  Rel carrier (arity 𝑅 r) {ρ}  -- interpret. of relations

-- Forgetful Functor
𝕌 : Type α
𝕌 = carrier

open structure public

module _ {𝐹 : signature 𝓞₀ 𝓥₀}{𝑅 : signature 𝓞₁ 𝓥₁} where

-- Syntactic sugar for interpretation of operation
_ʳ_ :  {α ρ}  (r : symbol 𝑅)(𝒜 : structure 𝐹 𝑅 {α}{ρ})  Rel (carrier 𝒜) ((arity 𝑅) r) {ρ}
_ʳ_ = flip rel

_ᵒ_ :  {α ρ}  (f : symbol 𝐹)(𝒜 : structure 𝐹 𝑅 {α}{ρ})  Op (carrier 𝒜)((arity 𝐹) f)
_ᵒ_ = flip op

compatible :  {α ρ }  (𝑨 : structure 𝐹 𝑅 {α}{ρ})  BinRel (carrier 𝑨)   Type _
compatible 𝑨 r =  (f : symbol 𝐹)  (f  𝑨) |: r

open Level

-- lift an operation to act on type of higher universe level
Lift-op :  {ι α}  {I : Type ι}{A : Type α}  Op A I  { : Level}  Op (Lift  A) I
--  Lift-op f = λ x → lift (f (λ i → lower (x i)))
Lift-op f = λ z  lift (f (lower  z))

-- lift a relation to a predicate on type of higher universe level
-- (note ρ doesn't change; see Lift-Structʳ for that)
Lift-rel :  {ι α ρ}  {I : Type ι}{A : Type α}  Rel A I {ρ}  { : Level}  Rel (Lift  A) I{ρ}
Lift-rel r x = r (lower  x)

-- lift the domain of a structure to live in a type at a higher universe level
Lift-Strucˡ :  {α ρ}  ( : Level)  structure 𝐹 𝑅 {α}{ρ}  structure 𝐹 𝑅  {α  }{ρ}
Lift-Strucˡ  𝑨 = record { carrier = Lift  (carrier 𝑨)
; op = λ f  Lift-op (f  𝑨)
; rel = λ R  Lift-rel (R ʳ 𝑨)
}

-- lift the relations of a structure from level ρ to level ρ ⊔ ℓ
Lift-Strucʳ :  {α ρ}  ( : Level)  structure 𝐹 𝑅 {α}{ρ}  structure 𝐹 𝑅 {α}{ρ  }
Lift-Strucʳ  𝑨 = record { carrier = carrier 𝑨 ; op = op 𝑨 ; rel = lrel }
where
lrel : (r : symbol 𝑅)  Rel (carrier 𝑨) ((arity 𝑅) r)
lrel r = Lift   r ʳ 𝑨

-- lift both domain of structure and the level of its relations
Lift-Struc :  {α ρ}  (ℓˡ ℓʳ : Level)  structure 𝐹 𝑅 {α}{ρ}  structure 𝐹 𝑅 {α  ℓˡ}{ρ  ℓʳ}
Lift-Struc ℓˡ ℓʳ 𝑨 = Lift-Strucʳ ℓʳ (Lift-Strucˡ ℓˡ 𝑨)