---
layout: default
title : "Legacy.Base.Structures.Basic module (Agda Universal Algebra Library)"
date : "2021-05-20"
author: "agda-algebras development team"
---

### <a id="basic-definitions">Basic Definitions</a>

This is the [Legacy.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.


```agda


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

module Legacy.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 Legacy.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 (arity 𝐹 f) carrier      -- 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 ((arity 𝐹) f) (carrier π’œ)
 _α΅’_ = 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 I A β†’ {β„“ : Level} β†’ Op I (Lift β„“ A)

 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Λ‘ β„“Λ‘ 𝑨)
```