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Λ‘ βΛ‘ π¨)