Lemma shSet_eq_from_shSet_z_iso_idtoiso (F G : shSet_category) (p : F = G) : shSet_eq_from_shSet_z_iso F G (idtoiso p) = p. Proof. unfold shSet_eq_from_shSet_z_iso. apply (invmaponpathsweq (weqtoforallpaths _ _ _ )). simpl (pr1weq (weqtoforallpaths (λ _ : sorts σ, hSet) F G)). rewrite (toforallpaths_funextsec). apply funextsec. intro a. rewrite idtoiso_shSet_category_compute_pointwise. rewrite isotoid_idtoiso. apply idpath. 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.