Definition eqalg_disp : disp_cat (shSet_category σ). Proof. use disp_cat_from_SIP_data. - cbn; intro A. exact (∑ ops: (∏ nm: names σ, A⋆ (arity nm) → A (sort nm)), (∏ e : equations σ, holds (make_algebra A ops) (geteq e))). - cbn. intros a b [opa iseqa] [opb iseqb] f. exact (@ishom σ (make_algebra a opa) (make_algebra b opb) f). - intros. apply isapropishom. - cbn. intros. apply ishomid. - cbn. intros A B C prpA prpB prpC. intros f g ishomf ishomg. exact (ishomcomp (make_hom ishomf) (make_hom ishomg)). Defined.
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.