proposition: Lemma disp_prod_functor_over_fixed_base_is_functor : disp_functor_axioms disp_prod_functor_over_fixed_base_data.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Isos