proposition: Proposition disp_functor_to_two_sided_disp_functor_axioms : twosided_disp_functor_laws F G D₁ D₂ disp_functor_to_two_sided_disp_functor_data.
proof: Proof. split. - intros x y xy ; cbn. etrans. { exact (@disp_functor_id _ _ _ _ _ FG (x ,, y) xy). } unfold transportb_disp_mor2, transportf_disp_mor2. rewrite twosided_prod_transport. unfold transportb. apply maponpaths_2. apply isasetdirprod ; apply homset_property. - intros x₁ x₂ x₃ y₁ y₂ y₃ xy₁ xy₂ xy₃ f₁ g₁ fg₁ f₂ g₂ fg₂ ; cbn. etrans. { exact (@disp_functor_comp _ _ _ _ _ FG (x₁ ,, y₁) (x₂ ,, y₂) (x₃ ,, y₃) xy₁ xy₂ xy₃ (f₁ ,, g₁) (f₂ ,, g₂) fg₁ fg₂). } unfold transportb_disp_mor2, transportf_disp_mor2. rewrite twosided_prod_transport. unfold transportb. apply maponpaths_2. apply isasetdirprod ; apply homset_property. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete UniMath.CategoryTheory.TwoSidedDisplayedCats.Total