proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis