Library UniMath.CategoryTheory.categories.Universal_Algebra.EqAlgebras

The univalent category of equational algebras over an equational specification.

Gianluca Amato, Marco Maggesi, Cosimo Perini Brogi 2019-2021

Require Import UniMath.Foundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.

Require Import UniMath.Algebra.Universal.EqAlgebras.
Require Import UniMath.CategoryTheory.categories.Universal_Algebra.Algebras.

Context (σ : eqspec).

Local Open Scope sorted_scope.

Definition eqalg_disp : disp_cat (category_algebras σ).
Show proof.

use disp_full_sub.
exact (λ A , is_eqalgebra A).

Lemma is_univalent_eqalg_disp : is_univalent_disp eqalg_disp.
Show proof.

  use disp_full_sub_univalent.
  intros A isT isT'.
  use impred_isaprop.
  intro eq.
  use impred_isaprop.
  intros α p p'.
  apply (pr1 A).

Definition category_eqalgebras : category := total_category eqalg_disp.

Lemma is_univalent_category_eqalgebras : is_univalent category_eqalgebras.
Show proof.

exact (@is_univalent_total_category
(category_algebras σ) eqalg_disp (is_univalent_category_algebras σ) is_univalent_eqalg_disp).