Lemma fam_z_iso (F : fam X) : z_iso ((functor_identity (fam X)) F) ((functor_composite fam_to_slice slice_to_fam) F). Proof. apply (z_iso_from_nat_z_iso has_homsets_HSET). exists ((pr1 fam_unit) F). intro x. exact (hset_equiv_is_z_iso ((pr1 F) x) (make_hSet (hfiber pr1 x) (isaset_hfiber pr1 x (isaset_total2_hSet X (λ x, (pr1 F) x)) (pr2 X))) (ezweqpr1 (funcomp (pr1 (pr1 F)) pr1) x)). Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.MonoEpiIso. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.CategoryTheory.Categories.HSET.Slice. Require Import UniMath.CategoryTheory.slicecat. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.CategoryTheory.Categories.StandardCategories.