This is the Base.Structures.Basic module of the Agda Universal Algebra Library. It is a submodule of the Structures module which presents general (relational-algebraic) structures as inhabitants of record types. For a similar development using Sigma types see the Base.Structures.Sigma.Basic module.
{-# OPTIONS --without-K --exact-split --safe #-} module Base.Structures.Basic where -- Imports from Agda and the Agda Standard Library ----------------------------- open import Agda.Primitive using () renaming ( Set to Type ) open import Function.Base using ( flip ; _∘_ ) open import Level using ( _⊔_ ; suc ; Level ) open import Relation.Binary.Core using () renaming ( Rel to BinRel ) -- Imports from the Agda Universal Algebra Library ----------------------------- open import Overture using ( Op ) open import Base.Relations using ( _|:_ ; _preserves_ ; Rel ) private variable 𝓞₀ 𝓥₀ 𝓞₁ 𝓥₁ : Level -- Signature as a record type record signature (𝓞 𝓥 : Level) : Type (suc (𝓞 ⊔ 𝓥)) where field symbol : Type 𝓞 arity : symbol → Type 𝓥 siglˡ : {𝓞 𝓥 : Level} → signature 𝓞 𝓥 → Level siglˡ {𝓞}{𝓥} _ = 𝓞 siglʳ : {𝓞 𝓥 : Level} → signature 𝓞 𝓥 → Level siglʳ {𝓞}{𝓥} _ = 𝓥 sigl : {𝓞 𝓥 : Level} → signature 𝓞 𝓥 → Level sigl {𝓞}{𝓥} _ = 𝓞 ⊔ 𝓥 open signature public record structure (𝐹 : signature 𝓞₀ 𝓥₀) (𝑅 : signature 𝓞₁ 𝓥₁) {α ρ : Level} : Type (𝓞₀ ⊔ 𝓥₀ ⊔ 𝓞₁ ⊔ 𝓥₁ ⊔ (suc (α ⊔ ρ))) where field carrier : Type α op : ∀(f : symbol 𝐹) → Op carrier (arity 𝐹 f) -- interpret. of operations rel : ∀(r : symbol 𝑅) → Rel carrier (arity 𝑅 r) {ρ} -- interpret. of relations -- Forgetful Functor 𝕌 : Type α 𝕌 = carrier open structure public module _ {𝐹 : signature 𝓞₀ 𝓥₀}{𝑅 : signature 𝓞₁ 𝓥₁} where -- Syntactic sugar for interpretation of operation _ʳ_ : ∀{α ρ} → (r : symbol 𝑅)(𝒜 : structure 𝐹 𝑅 {α}{ρ}) → Rel (carrier 𝒜) ((arity 𝑅) r) {ρ} _ʳ_ = flip rel _ᵒ_ : ∀{α ρ} → (f : symbol 𝐹)(𝒜 : structure 𝐹 𝑅 {α}{ρ}) → Op (carrier 𝒜)((arity 𝐹) f) _ᵒ_ = flip op compatible : ∀{α ρ ℓ} → (𝑨 : structure 𝐹 𝑅 {α}{ρ}) → BinRel (carrier 𝑨) ℓ → Type _ compatible 𝑨 r = ∀ (f : symbol 𝐹) → (f ᵒ 𝑨) |: r open Level -- lift an operation to act on type of higher universe level Lift-op : ∀{ι α} → {I : Type ι}{A : Type α} → Op A I → {ℓ : Level} → Op (Lift ℓ A) I Lift-op f = λ z → lift (f (lower ∘ z)) -- lift a relation to a predicate on type of higher universe level -- (note ρ doesn't change; see Lift-Structʳ for that) Lift-rel : ∀{ι α ρ} → {I : Type ι}{A : Type α} → Rel A I {ρ} → {ℓ : Level} → Rel (Lift ℓ A) I{ρ} Lift-rel r x = r (lower ∘ x) -- lift the domain of a structure to live in a type at a higher universe level Lift-Strucˡ : ∀{α ρ} → (ℓ : Level) → structure 𝐹 𝑅 {α}{ρ} → structure 𝐹 𝑅 {α ⊔ ℓ}{ρ} Lift-Strucˡ ℓ 𝑨 = record { carrier = Lift ℓ (carrier 𝑨) ; op = λ f → Lift-op (f ᵒ 𝑨) ; rel = λ R → Lift-rel (R ʳ 𝑨) } -- lift the relations of a structure from level ρ to level ρ ⊔ ℓ Lift-Strucʳ : ∀{α ρ} → (ℓ : Level) → structure 𝐹 𝑅 {α}{ρ} → structure 𝐹 𝑅 {α}{ρ ⊔ ℓ} Lift-Strucʳ ℓ 𝑨 = record { carrier = carrier 𝑨 ; op = op 𝑨 ; rel = lrel } where lrel : (r : symbol 𝑅) → Rel (carrier 𝑨) ((arity 𝑅) r) lrel r = Lift ℓ ∘ r ʳ 𝑨 -- lift both domain of structure and the level of its relations Lift-Struc : ∀{α ρ} → (ℓˡ ℓʳ : Level) → structure 𝐹 𝑅 {α}{ρ} → structure 𝐹 𝑅 {α ⊔ ℓˡ}{ρ ⊔ ℓʳ} Lift-Struc ℓˡ ℓʳ 𝑨 = Lift-Strucʳ ℓʳ (Lift-Strucˡ ℓˡ 𝑨)