# Algebras

Content created by Fernando Chu and Fredrik Bakke.

Created on 2023-03-20.

module universal-algebra.algebras-of-theories where

Imports
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import universal-algebra.abstract-equations-over-signatures
open import universal-algebra.algebraic-theories
open import universal-algebra.models-of-signatures
open import universal-algebra.signatures
open import universal-algebra.terms-over-signatures


## Idea

Given a theory, an algebra is a model on a set such that it satisfies all equations in the theory.

## Definitions

### Algebra

module _
{ l1 : Level} ( Sg : signature l1)
{ l2 : Level} ( Th : Theory Sg l2)
where

is-algebra :
{ l3 : Level} →
( X : Model-Signature Sg l3) → UU (l2 ⊔ l3)
is-algebra M =
( e : index-Theory Sg Th) →
( assign : assignment Sg (type-Model-Signature Sg M)) →
eval-term Sg (is-model-set-Model-Signature Sg M) assign
( lhs-Abstract-Equation Sg (index-Abstract-Equation-Theory Sg Th e)) ＝
eval-term Sg (is-model-set-Model-Signature Sg M) assign
( rhs-Abstract-Equation Sg (index-Abstract-Equation-Theory Sg Th e))

Algebra :
( l3 : Level) →
UU (l1 ⊔ l2 ⊔ lsuc l3)
Algebra l3 =
Σ ( Model-Signature Sg l3) (is-algebra)

model-Algebra :
{ l3 : Level} →
Algebra l3 → Model-Signature Sg l3
model-Algebra Alg = pr1 Alg

set-Algebra :
{ l3 : Level} →
Algebra l3 → Set l3
set-Algebra Alg = pr1 (pr1 Alg)

is-model-set-Algebra :
{ l3 : Level} →
( Alg : Algebra l3) →
is-model-signature Sg (set-Algebra Alg)
is-model-set-Algebra Alg = pr2 (pr1 Alg)

type-Algebra :
{ l3 : Level} →
Algebra l3 → UU l3
type-Algebra Alg =
pr1 (pr1 (pr1 Alg))

is-set-Algebra :
{ l3 : Level} →
(Alg : Algebra l3) → is-set (type-Algebra Alg)
is-set-Algebra Alg = pr2 (pr1 (pr1 Alg))

is-algebra-Algebra :
{ l3 : Level} →
( Alg : Algebra l3) →
is-algebra (model-Algebra Alg)
is-algebra-Algebra Alg = pr2 Alg


## Properties

### Being an algebra is a proposition

  is-prop-is-algebra :
{ l3 : Level} →
( X : Model-Signature Sg l3) →
is-prop (is-algebra X)
is-prop-is-algebra M =
is-prop-Π
( λ e →
( is-prop-Π
( λ assign → is-set-type-Model-Signature Sg M _ _)))