Definition algebras_disp : disp_cat shSet_category. Proof. use disp_cat_from_SIP_data. simpl. - intro A. exact (∏ nm: names σ, A⋆ (arity nm) → A (sort nm)). - simpl. intros A B asA asB f. exact (@ishom σ (make_algebra A asA) (make_algebra B asB) f). - simpl. intros A B asA asB f opA opB. apply isapropishom. intro s. apply setproperty. - cbn. intros A asA. apply ishomid. - cbn. intros A B C opA opB opC. intros f g ishomf ishomg. exact (ishomcomp (make_hom ishomf) (make_hom ishomg)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.Algebra.Universal.TermAlgebras.