Lemma slicecat_functor_comp {x y z : C} (f : C⟦x,y⟧) (g : C⟦y,z⟧) : slicecat_functor (f · g) = functor_composite (slicecat_functor f) (slicecat_functor g). Proof. apply (functor_eq _ _ (has_homsets_slice_precat _ _)); simpl. unfold slicecat_functor_data; simpl. unfold functor_composite_data; simpl. apply (two_arg_paths_f (slicecat_functor_comp_ob _ _)). apply funextsec; intros [a fax]. apply funextsec; intros [b fbx]. 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_comp_ob. rewrite toforallpaths_funextsec; simpl. assert (H1 : transportf (fun x : C / z => pr1 x --> b) (Foundations.PartA.internal_paths_rew_r _ _ _ (λ p, tpair _ a p = tpair _ a _) (idpath (tpair _ a _)) (assoc fax f g)) h = h). induction (assoc fax f g); apply idpath. assert (H2 : ∏ h', h' = h -> transportf (fun x : C / z => a --> pr1 x) (Foundations.PartA.internal_paths_rew_r _ _ _ (λ p, tpair _ b p = tpair _ b _) (idpath _) (assoc fbx f g)) h' = h). intros h' eq. induction (assoc fbx f g); rewrite eq; apply idpath. apply H2. exact H1. 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.