proposition: Lemma shSet_iso_fiber {A B : shSet_category} (i : z_iso A B): ∏ s, @z_iso HSET (A s) (B s).
proof: Proof. intro s. induction i as [i [i' [p q]]]. simpl in *. use make_z_iso. - exact (i s). - exact (i' s). - split. + exact (eqtohomot p s). + exact (eqtohomot q s). 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