↑ Top


Basic Definitions

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

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

module Base.Structures.Sigma.Basic where

-- Imports from the Agda Standard Library ------------------------------------------------
open import Agda.Primitive        using () renaming ( Set to Type ; lzero to ℓ₀ )
open import Data.Product          using ( _,_ ; _×_ ; Σ-syntax )
                                  renaming ( proj₁ to fst ; proj₂ to snd )
open import Level                 using ( _⊔_ ; suc ; Level )
open import Relation.Binary.Core  using ( _⇒_ ; _=[_]⇒_ )
                                  renaming ( REL to BinREL ; Rel to BinRel )

-- Imports from the Agda Universal Algebra Library ---------------------------------------------
open import Overture        using ( ∣_∣ ; ∥_∥ ; ℓ₁ ; Op )
open import Base.Relations  using ( _|:_ ; _preserves_ ; Rel )

-- Inhabitants of Signature type are pairs, (s , ar), where s is an operation symbol,
Signature : Type ℓ₁                         -- OR a relation symbol (new!),
Signature = Σ[ F  Type ℓ₀ ] (F  Type ℓ₀)  -- and ar the arity of s.

Structure : (𝑅 F : Signature){α ρ : Level}  Type (suc (α  ρ))
Structure 𝑅 𝐹 {α}{ρ} =
  Σ[ A  Type α ]                        -- the domain of the structure is A
  ( ((r :  𝑅 )  Rel A (snd 𝑅 r){ρ})   -- the interpretations of the relation symbols
  × ((f :  𝐹 )  Op A (snd 𝐹 f)) )     -- the interpretations of the operation symbols

RStructure : Signature  {α ρ : Level}  Type (suc (α  ρ))
RStructure 𝑅 {α} {ρ} = Σ[ A  Type α ] ∀(r :  𝑅 )  Rel A (snd 𝑅 r) {ρ}

AStructure : Signature  {α : Level}  Type (suc α)
AStructure 𝐹 {α} = Σ[ A  Type α ]  (f :  𝐹 )  Op A (snd 𝐹 f)

module _ {𝑅 𝐹 : Signature} {α ρ : Level} where

-- Reducts
 Structure→RStructure : Structure 𝑅 𝐹 {α}{ρ}  RStructure 𝑅 {α}{ρ}
 Structure→RStructure (A , ( , _)) = A , 

 Structure→AStructure : Structure 𝑅 𝐹 {α}{ρ}  AStructure 𝐹
 Structure→AStructure (A , (_ , )) = A , 

  -- Syntax for interpretation of relations and operations.
 _⟦_⟧ᵣ : (𝒜 : Structure 𝑅 𝐹 {α}{ρ})(𝑟 :  𝑅 )  Rel  𝒜  ( 𝑅  𝑟) {ρ}
 𝒜  𝑟 ⟧ᵣ = λ a  (fst  𝒜  𝑟) a

 _⟦_⟧ₒ : (𝒜 : Structure 𝑅 𝐹 {α}{ρ})(𝑓 :  𝐹 )  Op  𝒜  ( 𝐹  𝑓)
 𝒜  𝑓 ⟧ₒ = λ a  (snd  𝒜  𝑓) a

 _ʳ_ : (𝑟 :  𝑅 )(𝒜 : Structure 𝑅 𝐹 {α})  Rel  𝒜  ( 𝑅  𝑟){ρ}
 𝑟 ʳ 𝒜 = λ a  (𝒜  𝑟 ⟧ᵣ) a

 _ᵒ_ : (𝑓 :  𝐹 )(𝒜 : Structure 𝑅 𝐹 {α}{ρ})  Op  𝒜 ( 𝐹  𝑓)
 𝑓  𝒜 = λ a  (𝒜  𝑓 ⟧ₒ) a

 Compatible : {ρ' : Level}(𝑨 : Structure 𝑅 𝐹{α}{ρ})  BinRel  𝑨  ρ'   Type (α  ρ')
 Compatible 𝑨 r =  𝑓  (𝑓  𝑨) |: r

 Compatible' : {ρ' : Level}(𝑨 : Structure 𝑅 𝐹 {α}{ρ})  BinRel  𝑨  ρ'   Type (α  ρ')
 Compatible' 𝑨 r =  𝑓  (𝑓  𝑨) preserves r

 open 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-rel : {I : Type ℓ₀}{A : Type α}  Rel A I {ρ}  ( : Level)  Rel (Lift  A) I{ρ}
 Lift-rel r  x = r  i  lower (x i))

 Lift-Strucˡ : ( : Level)  Structure 𝑅 𝐹 {α}{ρ}  Structure 𝑅 𝐹 {α = (α  )}{ρ}
 Lift-Strucˡ  𝑨 = Lift   𝑨  , (lrel , lop )
  where
  lrel : (r :  𝑅 )  Rel (Lift   𝑨 )( 𝑅  r){ρ}
  lrel r = λ x  ((r ʳ 𝑨)  i  lower (x i)))
  lop : (f :  𝐹 )  Op (Lift   𝑨 ) ( 𝐹  f)
  lop f = λ x  lift ((f  𝑨)( λ i  lower (x i)))

 Lift-Strucʳ : ( : Level)  Structure 𝑅 𝐹 {α}{ρ}  Structure 𝑅 𝐹 {α}{ρ = (ρ  )}
 Lift-Strucʳ  𝑨 =  𝑨  , lrel , snd  𝑨 
  where
  lrel : (r :  𝑅 )  Rel ( 𝑨 )( 𝑅  r){ρ  }
  lrel r = λ x  Lift  ((r ʳ 𝑨) x) -- λ x → ((r ʳ 𝑨) (λ i → lower (x i)))

module _ {𝑅 𝐹 : Signature} {α ρ : Level} where

 Lift-Struc : (ℓˡ ℓʳ : Level)  Structure 𝑅 𝐹 {α}{ρ}  Structure 𝑅 𝐹 {α  ℓˡ}{ρ  ℓʳ}
 Lift-Struc ℓˡ ℓʳ 𝑨 = Lift-Strucʳ ℓʳ (Lift-Strucˡ ℓˡ 𝑨)


← Base.Structures.Sigma Base.Structures.Sigma.Products →