proposition: 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: 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.
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