Lemma is_functor_slice_to_fam : is_functor slice_to_fam_data. Proof. split; [ intro a | intros a b c f g]; apply (nat_trans_eq has_homsets_HSET); intro x; apply funextsec; intro p; apply (invmaponpathsincl pr1); simpl; try (apply isofhlevelfpr1; intro; apply setproperty); repeat (unfold hfiber; rewrite transportf_total2; simpl); repeat (rewrite transportf_const); reflexivity. Qed.
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.