↑ Top


Products for structures as records

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

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

module Base.Structures.Products where

-- Imports from the Agda Standard Library ----------------------------------
open import Agda.Primitive  using () renaming ( Set to Type )
open import Data.Product    using ( _,_ ; Σ-syntax )
open import Level           using ( Level ; suc ; _⊔_ )
open import Relation.Unary  using ( _∈_ ; Pred )

-- Imports from the Agda Universal Algebra Library -------------------------
open import Overture               using ( ∣_∣ ; Π-syntax )
open import Base.Structures.Basic  using ( signature ; structure )


private variable
 𝓞₀ 𝓥₀ 𝓞₁ 𝓥₁ : Level
 𝐹 : signature 𝓞₀ 𝓥₀
 𝑅 : signature 𝓞₁ 𝓥₁
 α ρ  : Level

open structure

 : { : Type }(𝒜 :   structure 𝐹 𝑅 {α}{ρ} )  structure 𝐹 𝑅
 { = } 𝒜 =
 record  { carrier = Π[ i   ] carrier (𝒜 i)             -- domain of the product structure
         ; op = λ 𝑓 a i  (op (𝒜 i) 𝑓) λ x  a x i        -- interpretation of  operations
         ; rel = λ r a   i  (rel (𝒜 i) r) λ x  a x i  -- interpretation of relations
         }


module _ {𝒦 : Pred (structure 𝐹 𝑅 {α}{ρ}) } where
  ℓp : Level
  ℓp = suc (α  ρ)  

   : Type _
   = Σ[ 𝑨  structure 𝐹 𝑅  {α}{ρ}] 𝑨  𝒦

  𝔄 :   structure 𝐹 𝑅 {α}{ρ}
  𝔄 𝔦 =  𝔦 

  class-product : structure 𝐹 𝑅
  class-product =  𝔄

← Base.Structures.Graphs0 Base.Structures.Congruences →