Definition PreShv_to_slice_is_funct : is_functor PreShv_to_slice_data. Proof. split; [intros X | intros X Y Z f g]; apply eq_mor_slicecat; apply (nat_trans_eq has_homsets_HSET); unfold PreShv_to_slice_ob_nat , PreShv_to_slice_ob_funct_fun; intro c; apply funextsec; intro p; reflexivity. Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import