proposition: Lemma transportf_fst_arg {A B C : category} {DA : disp_cat A} {DB : disp_cat B} {DC : disp_cat C} {F : A ⊠ B ⟶ C} (FF : disp_functor F (DA ⊠⊠ DB) DC) {a₁ a₂ : A} {da₁ : DA a₁} {da₂ : DA a₂} {f f' : a₁ --> a₂} (e : f = f') (ff : da₁ -->[f] da₂) {b₁ b₂ : B} {db₁ : DB b₁} {db₂ : DB b₂} {g : b₁ --> b₂} (gg : db₁ -->[g] db₂) : transportf_fst_arg_type FF e ff gg.
proof: Proof. unfold transportf_fst_arg_type. induction e. cbn. apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.catiso UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions