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. 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.
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.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Total. Section FromDispFunctor. End FromDispFunctor.