proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Univalence UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.SIP UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.Limits.Initial UniMath.Algebra.Universal.TermAlgebras