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. unfold transportf_fst_arg_type. induction e. cbn. apply idpath. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.