Definition PreShv_unit_fun (F : PreShv ∫P) : (functor_identity _) F --> (PreShv_to_slice ∙ slice_to_PreShv) F. Proof. use tpair. + intros [X p] x. exact ((p ,, x) ,, idpath p). + intros [X p] [X' p'] [f feq]. simpl in *. apply funextsec; intros x. apply (invmaponpathsincl pr1). apply isofhlevelfpr1; intro; apply setproperty. induction (!feq). apply (total2_paths2_f (idpath _)). rewrite idpath_transportf. assert (set_eq : idpath _ = feq). { apply (pr2 (P X')). } now induction set_eq. 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