proposition: Lemma disp_pair_functor_axioms : @disp_functor_axioms (A ⊠ A') (C ⊠ C') (pair_functor F F') _ _ disp_pair_functor_data.
proof: Proof. split. - intros [a a'] [d d']. apply pathsinv0. etrans. { apply disp_binprod_transportf. } cbn. apply dirprodeq; cbn. + apply pathsinv0. etrans. apply disp_functor_id. apply transportf_paths. apply C. + apply pathsinv0. etrans. apply disp_functor_id. apply transportf_paths. apply C'. - intros [a a'] [b b'] [c c'] [w w'] [x x'] [y y'] [f f'] [g g'] [ff ff'] [gg gg']. cbn in *. apply pathsinv0. etrans. { apply disp_binprod_transportf. } apply pathsinv0. apply dirprodeq; cbn. + etrans. apply disp_functor_comp. apply transportf_paths. apply C. + etrans. apply disp_functor_comp. apply transportf_paths. apply C'. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.catiso UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions