proposition: Proposition disp_functor_over_pair_inv_laws {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_axioms (disp_functor_over_pair_inv_data F).
proof: Proof. split. - intros x xx ; cbn. refine (disp_functor_id F xx @ _). apply transportf_set. apply homset_property. - intros x y z xx yy zz f g ff gg ; cbn. refine (disp_functor_comp F ff gg @ _). apply transportf_set. apply homset_property. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors