### Basic Definitions

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Λ‘ βΛ‘ π¨)
```