Lemma shSet_iso_fiber {A B : shSet_category} (i : z_iso A B): ∏ s, @z_iso HSET (A s) (B s). 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.
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.