{-# 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 →