Lemma is_univalent_algebras_disp : is_univalent_disp algebras_disp. Proof. use is_univalent_disp_from_SIP_data. - intro A. cbn. use impred_isaset. intro nm. cbn. use isaset_set_fun_space. - cbn. intros A op1 op2 ishomid1 _. use funextsec. intro nm. use funextfun. intro vec. unfold ishom in *. cbn in *. set (H1:= ishomid1 nm vec). rewrite staridfun in H1. apply H1. Qed.
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.