↑ Top


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Λ‘ β„“Λ‘ 𝑨)


↑ Structures Structures.Graphs β†’