Proposition disp_functor_over_pair_laws {C : category} {D₁ D₂ : disp_cat (category_binproduct C C)} (F : disp_functor (functor_identity (category_binproduct C C)) D₁ D₂) : disp_functor_axioms (disp_functor_over_pair_data F). Proof. split. - intros x xx ; cbn. refine (disp_functor_id F xx @ _). apply maponpaths_2. apply homset_property. - intros x y z xx yy zz f g ff gg ; cbn. refine (disp_functor_comp F ff gg @ _). apply maponpaths_2. apply homset_property. Qed.
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.