Definition slice_to_fam_mor_fun {a b : slice X} (f : a --> b) (x : X) : (s_to_f a : functor (discrete X) HSET) x --> (s_to_f b : functor (discrete X) HSET) x := λ p, hfibersgftog (pr1 f) (pr2 b) _ (transportf (λ p, hfiber p x) (pr2 f) p).
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.