Lemma idtoiso_shSet_eq_from_shSet_z_iso (F G : shSet_category) (i : z_iso F G) : idtoiso (shSet_eq_from_shSet_z_iso F G i) = i. Proof. apply z_iso_eq. apply funextsec. intro s. unfold shSet_eq_from_shSet_z_iso. assert (H' := idtoiso_shSet_category_compute_pointwise (shSet_eq_from_shSet_z_iso F G i) s). simpl in *. assert (H2 := maponpaths (@pr1 _ _ ) H'). simpl in H2. etrans. { apply H2. } intermediate_path (pr1 (idtoiso (isotoid HSET is_univalent_HSET (shSet_iso_fiber i s)))). - apply maponpaths. apply maponpaths. unfold shSet_eq_from_shSet_z_iso. rewrite toforallpaths_funextsec. apply idpath. - rewrite idtoiso_isotoid. apply idpath. 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.