proposition: Lemma disp_nat_trans_transportf {C' C : category} {D' : disp_cat C'} {D : disp_cat C} (F' F : functor C' C) (a' a : nat_trans F' F) (p : a' = a ) (FF' : disp_functor F' D' D) (FF : disp_functor F D' D) (b : disp_nat_trans a' FF' FF) (c' : C') (xx' : D' c') : pr1 (transportf (λ x, disp_nat_trans x FF' FF) p b) c' xx' = transportf (mor_disp (FF' c' xx') (FF c' xx')) (nat_trans_eq_pointwise p _ ) (b c' xx').
proof: Proof. induction p. assert (XR : nat_trans_eq_pointwise (idpath a') c' = idpath _ ). { apply homset_property. } rewrite XR. apply idpath. Qed.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Isos