Lemma slicecat_functor_identity (x : C) : slicecat_functor (identity x) = functor_identity (C / x). Proof. apply (functor_eq _ _ (has_homsets_slice_precat _ _)); simpl. apply (two_arg_paths_f (slicecat_functor_identity_ob _)). apply funextsec; intros [a f]. apply funextsec; intros [b g]. apply funextsec; intros [h hh]. rewrite transport_of_functor_map_is_pointwise; simpl in *. unfold double_transport. unfold slicecat_mor, slice_precat_ob_mor, slicecat_mor. simpl. rewrite transportf_total2. apply subtypePairEquality; [intro; apply C | ]. rewrite transportf_total2; simpl. unfold slicecat_functor_identity_ob. rewrite toforallpaths_funextsec; simpl. induction (id_right f). induction (id_right g). apply idpath. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis.