↑ Top


Product structures

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

module Base.Structures.Sigma.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 ; Lift )
open import Relation.Unary  using ( _∈_ ; Pred )

-- Imports from the Agda Universal Algebra Library ---------------------------
open import Overture                     using ( ∣_∣ ; ∥_∥ ; Π ; Π-syntax )
open import Base.Structures.Sigma.Basic  using ( Signature ; Structure ; _ʳ_ ; _ᵒ_ )

private variable
 𝑅 𝐹 : Signature
 α ρ ι : Level

 : { : Type ι}(𝒜 :   Structure  𝑅 𝐹{α}{ρ})  Structure 𝑅 𝐹 {α  ι} {ρ  ι}
 { = } 𝒜 =  Π[ 𝔦   ]  𝒜 𝔦                          -- domain of the product structure
               , ( λ r a   𝔦  (r ʳ 𝒜 𝔦) λ x  a x 𝔦 )  -- interpretations of relations
               , ( λ 𝑓 a 𝔦  (𝑓  𝒜 𝔦) λ x  a x 𝔦 )      -- interpretations of  operations

module _ {α ρ τ : Level}{𝒦 : Pred (Structure 𝑅 𝐹 {α}{ρ}) τ} where

 ℓp : Level
 ℓp = lsuc (α  ρ)  τ

  : Type ℓp
  = Σ[ 𝑨  Structure 𝑅 𝐹 ] (𝑨  𝒦)

 𝔖 :   Structure 𝑅 𝐹        -- (type \MfS to get 𝔖)
 𝔖 𝔦 =  𝔦 

 class-prod : Structure 𝑅 𝐹
 class-prod =  𝔖

If p : 𝑨 ∈ 𝒦, we view the pair (𝑨 , p) ∈ ℑ as an index over the class, so we can think of 𝔄 (𝑨 , p) (which is simply 𝑨) as the projection of the product ⨅ 𝔄 onto the (𝑨 , p)-th component.


← Base.Structures.Sigma.Basic Base.Structures.Sigma.Congruences →