#### Basic Definitions

This is the Base.Structures.Sigma.Basic module of the Agda Universal Algebra Library.

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

module Base.Structures.Sigma.Basic where

-- Imports from the Agda Standard Library ------------------------------------------------
open import Agda.Primitive        using () renaming ( Set to Type ; lzero to ℓ₀ )
open import Data.Product          using ( _,_ ; _×_ ; Σ-syntax )
renaming ( proj₁ to fst ; proj₂ to snd )
open import Level                 using ( _⊔_ ; suc ; Level )
open import Relation.Binary.Core  using ( _⇒_ ; _=[_]⇒_ )
renaming ( REL to BinREL ; Rel to BinRel )

-- Imports from the Agda Universal Algebra Library ---------------------------------------------
open import Overture        using ( ∣_∣ ; ∥_∥ ; ℓ₁ ; Op )
open import Base.Relations  using ( _|:_ ; _preserves_ ; Rel )

-- Inhabitants of Signature type are pairs, (s , ar), where s is an operation symbol,
Signature : Type ℓ₁                         -- OR a relation symbol (new!),
Signature = Σ[ F ∈ Type ℓ₀ ] (F → Type ℓ₀)  -- and ar the arity of s.

Structure : (𝑅 F : Signature){α ρ : Level} → Type (suc (α ⊔ ρ))
Structure 𝑅 𝐹 {α}{ρ} =
Σ[ A ∈ Type α ]                        -- the domain of the structure is A
( ((r : ∣ 𝑅 ∣) → Rel A (snd 𝑅 r){ρ})   -- the interpretations of the relation symbols
× ((f : ∣ 𝐹 ∣) → Op A (snd 𝐹 f)) )     -- the interpretations of the operation symbols

RStructure : Signature → {α ρ : Level} → Type (suc (α ⊔ ρ))
RStructure 𝑅 {α} {ρ} = Σ[ A ∈ Type α ] ∀(r : ∣ 𝑅 ∣) → Rel A (snd 𝑅 r) {ρ}

AStructure : Signature → {α : Level} → Type (suc α)
AStructure 𝐹 {α} = Σ[ A ∈ Type α ] ∀ (f : ∣ 𝐹 ∣) → Op A (snd 𝐹 f)

module _ {𝑅 𝐹 : Signature} {α ρ : Level} where

-- Reducts
Structure→RStructure : Structure 𝑅 𝐹 {α}{ρ} → RStructure 𝑅 {α}{ρ}
Structure→RStructure (A , (ℛ , _)) = A , ℛ

Structure→AStructure : Structure 𝑅 𝐹 {α}{ρ} → AStructure 𝐹
Structure→AStructure (A , (_ , ℱ)) = A , ℱ

-- Syntax for interpretation of relations and operations.
_⟦_⟧ᵣ : (𝒜 : Structure 𝑅 𝐹 {α}{ρ})(𝑟 : ∣ 𝑅 ∣) → Rel ∣ 𝒜 ∣ (∥ 𝑅 ∥ 𝑟) {ρ}
𝒜 ⟦ 𝑟 ⟧ᵣ = λ a → (fst ∥ 𝒜 ∥ 𝑟) a

_⟦_⟧ₒ : (𝒜 : Structure 𝑅 𝐹 {α}{ρ})(𝑓 : ∣ 𝐹 ∣) → Op ∣ 𝒜 ∣ (∥ 𝐹 ∥ 𝑓)
𝒜 ⟦ 𝑓 ⟧ₒ = λ a → (snd ∥ 𝒜 ∥ 𝑓) a

_ʳ_ : (𝑟 : ∣ 𝑅 ∣)(𝒜 : Structure 𝑅 𝐹 {α}) → Rel ∣ 𝒜 ∣ (∥ 𝑅 ∥ 𝑟){ρ}
𝑟 ʳ 𝒜 = λ a → (𝒜 ⟦ 𝑟 ⟧ᵣ) a

_ᵒ_ : (𝑓 : ∣ 𝐹 ∣)(𝒜 : Structure 𝑅 𝐹 {α}{ρ}) → Op ∣ 𝒜 ∣(∥ 𝐹 ∥ 𝑓)
𝑓 ᵒ 𝒜 = λ a → (𝒜 ⟦ 𝑓 ⟧ₒ) a

Compatible : {ρ' : Level}(𝑨 : Structure 𝑅 𝐹{α}{ρ}) → BinRel ∣ 𝑨 ∣ ρ'  → Type (α ⊔ ρ')
Compatible 𝑨 r = ∀ 𝑓 → (𝑓 ᵒ 𝑨) |: r

Compatible' : {ρ' : Level}(𝑨 : Structure 𝑅 𝐹 {α}{ρ}) → BinRel ∣ 𝑨 ∣ ρ'  → Type (α ⊔ ρ')
Compatible' 𝑨 r = ∀ 𝑓 → (𝑓 ᵒ 𝑨) preserves r

open Level

Lift-op : {I : Type ℓ₀}{A : Type α} → Op A I → (ℓ : Level) → Op (Lift ℓ A) I
Lift-op f ℓ = λ x → lift (f (λ i → lower (x i)))

Lift-rel : {I : Type ℓ₀}{A : Type α} → Rel A I {ρ} → (ℓ : Level) → Rel (Lift ℓ A) I{ρ}
Lift-rel r ℓ x = r (λ i → lower (x i))

Lift-Strucˡ : (ℓ : Level) → Structure 𝑅 𝐹 {α}{ρ} → Structure 𝑅 𝐹 {α = (α ⊔ ℓ)}{ρ}
Lift-Strucˡ ℓ 𝑨 = Lift ℓ ∣ 𝑨 ∣ , (lrel , lop )
where
lrel : (r : ∣ 𝑅 ∣) → Rel (Lift ℓ ∣ 𝑨 ∣)(∥ 𝑅 ∥ r){ρ}
lrel r = λ x → ((r ʳ 𝑨) (λ i → lower (x i)))
lop : (f : ∣ 𝐹 ∣) → Op (Lift ℓ ∣ 𝑨 ∣) (∥ 𝐹 ∥ f)
lop f = λ x → lift ((f ᵒ 𝑨)( λ i → lower (x i)))

Lift-Strucʳ : (ℓ : Level) → Structure 𝑅 𝐹 {α}{ρ} → Structure 𝑅 𝐹 {α}{ρ = (ρ ⊔ ℓ)}
Lift-Strucʳ ℓ 𝑨 = ∣ 𝑨 ∣ , lrel , snd ∥ 𝑨 ∥
where
lrel : (r : ∣ 𝑅 ∣) → Rel (∣ 𝑨 ∣)(∥ 𝑅 ∥ r){ρ ⊔ ℓ}
lrel r = λ x → Lift ℓ ((r ʳ 𝑨) x) -- λ x → ((r ʳ 𝑨) (λ i → lower (x i)))

module _ {𝑅 𝐹 : Signature} {α ρ : Level} where

Lift-Struc : (ℓˡ ℓʳ : Level) → Structure 𝑅 𝐹 {α}{ρ} → Structure 𝑅 𝐹 {α ⊔ ℓˡ}{ρ ⊔ ℓʳ}
Lift-Struc ℓˡ ℓʳ 𝑨 = Lift-Strucʳ ℓʳ (Lift-Strucˡ ℓˡ 𝑨)

```