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. induction p. assert (XR : nat_trans_eq_pointwise (idpath a') c' = idpath _ ). { apply homset_property. } rewrite XR. apply idpath. Qed.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Isos.