fact: Definition make_disp_binat_trans {A B C : category} {F : bifunctor A B C} {G : bifunctor A B C} {DA : disp_cat A} {DB : disp_cat B} {DC : disp_cat C} {α : binat_trans F G} {DF : disp_bifunctor_data F DA DB DC} {DG : disp_bifunctor_data G DA DB DC} (dα : disp_binat_trans_data α DF DG) (H : is_disp_binat_trans dα) : disp_binat_trans α DF DG := (dα,,H).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Core.Isos