Lemma is_univalent_eqalg_disp : is_univalent_disp eqalg_disp. Proof. use is_univalent_disp_from_SIP_data. - cbn; intro A. apply isaset_total2. * apply impred_isaset. cbn; intro nm; use isaset_set_fun_space. * cbn; intros. apply impred_isaset. cbn; intro sys. apply impred_isaset; cbn. intro t. apply isasetaprop. apply A. - cbn; intros A [opA iseqA][op'A iseq'A]. intros i i'. use total2_paths2_f. * use funextsec. intro nm. use funextfun. intro v. unfold ishom in *. cbn in *. set (H1 := i nm v). eapply pathscomp0. exact H1. apply maponpaths. apply staridfun. * cbn. apply funextsec; cbn; intro e. apply funextsec; intro f. apply A. Qed.
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.