Definition slice_counit_fun (X : PreShv C / P) : (slice_to_PreShv ∙ PreShv_to_slice) X --> (functor_identity _) X. Proof. destruct X as [[[X Xmor] Xisfunct] [Xnat Xisnat]]. simpl in *. repeat (use tpair; simpl). + intros x [p q]. exact (pr1 q). + intros A B f. apply funextsec; intros [p peq]. reflexivity. + apply (nat_trans_eq has_homsets_HSET). intros A. apply funextsec; intros [p [q e]]. exact (!e). 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