↑ Top


Products for structures as records

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

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

module Structures.Products where

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

-- Imports from the Agda Universal Algebra Library -------------------------
open import Overture.Preliminaries using ( ∣_∣ ; Π-syntax )
open import 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 = lsuc (α  ρ)  

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

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

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


← Structures.Graphs0 Structures.Congruences →