Lemma disp_prod_functor_over_fixed_base_is_functor : disp_functor_axioms disp_prod_functor_over_fixed_base_data. Proof. split. - intros x xx. use total2_paths_f. + refine (pr12 FF x (pr1 xx) @ _). apply pathsinv0, pr1_transportf. + rewrite transportf_const. refine (pr12 FF' x (pr2 xx) @ _). apply pathsinv0, pr2_transportf. - intros x y z xx yy zz f g ff gg. use total2_paths_f. + refine (pr22 FF x y z (pr1 xx) (pr1 yy) (pr1 zz) f g (pr1 ff) (pr1 gg) @ _). apply pathsinv0, pr1_transportf. + rewrite transportf_const. refine (pr22 FF' x y z (pr2 xx) (pr2 yy) (pr2 zz) f g (pr2 ff) (pr2 gg) @ _). apply pathsinv0, pr2_transportf. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos.