fact: Definition disp_functor_over_pair_inv {C : category} {D₁ D₂ : disp_cat (category_binproduct C C)} (F : disp_functor (pair_functor (functor_identity C) (functor_identity C)) D₁ D₂) : disp_functor (functor_identity (category_binproduct C C)) D₁ D₂.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors