Legacy.Base.Structures.Sigma.Products

Product structures

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Legacy.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 Legacy.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.