Lemma disp_pair_functor_axioms : @disp_functor_axioms (A ⊠ A') (C ⊠ C') (pair_functor F F') _ _ disp_pair_functor_data. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.