The category of algebras of theories

Content created by Garrett Figueroa.

Created on 2025-09-05.
Last modified on 2025-09-05.

{-# OPTIONS --lossy-unification #-}

module universal-algebra.category-of-algebras-of-theories where
Imports 
open import category-theory.isomorphisms-in-large-precategories
open import category-theory.large-categories
open import category-theory.large-precategories

open import foundation.dependent-pair-types
open import foundation.sets
open import foundation.subtype-identity-principle
open import foundation.universe-levels

open import foundation-core.equality-dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.identity-types

open import universal-algebra.algebraic-theories
open import universal-algebra.algebras-of-theories
open import universal-algebra.homomorphisms-of-algebras
open import universal-algebra.isomorphisms-of-algebras
open import universal-algebra.models-of-signatures
open import universal-algebra.precategory-of-algebras-of-theories
open import universal-algebra.signatures

Idea

The precategory of algebras of a theory is a category.

Definition

module _
  {l1 l2 : Level} (σ : signature l1) (T : Theory σ l2)
  where

  is-large-category-Algebra-Large-Precategory :
    is-large-category-Large-Precategory (Algebra-Large-Precategory σ T)
  is-large-category-Algebra-Large-Precategory = is-equiv-iso-eq-Algebra σ T

  Algebra-Large-Category :
    Large-Category (λ l → l1 ⊔ l2 ⊔ lsuc l) (λ l3 → _⊔_ (l1 ⊔ l3))
  large-precategory-Large-Category Algebra-Large-Category =
    Algebra-Large-Precategory σ T
  is-large-category-Large-Category Algebra-Large-Category =
    is-large-category-Algebra-Large-Precategory

Recent changes