Definition slice_to_PreShv_ob_nat {X Y : PreShv C / P} (F : X --> Y) (e : ∫P^op) : (slice_to_PreShv_ob_ob X) e --> (slice_to_PreShv_ob_ob Y) e. Proof. induction e as [e Pe]. exact (λ p, hfibersgftog ((pr1 (pr1 F)) e) ((pr1 (pr2 Y)) e) Pe (transportf (λ x, hfiber (x e) Pe) (base_paths _ _ (pr2 F)) p)). 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