Definition disp_functor_over_pair_weq {C : category} (D₁ D₂ : disp_cat (category_binproduct C C)) : disp_functor (functor_identity (category_binproduct C C)) D₁ D₂ ≃ disp_functor (pair_functor (functor_identity C) (functor_identity C)) D₁ D₂. Proof. use weq_iso. - exact disp_functor_over_pair. - exact disp_functor_over_pair_inv. - abstract (intro F ; use subtypePath ; [ intro ; apply isaprop_disp_functor_axioms | ] ; apply idpath). - abstract (intro F ; use subtypePath ; [ intro ; apply isaprop_disp_functor_axioms | ] ; apply idpath). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors.