Proposition two_sided_disp_functor_to_disp_functor_axioms : disp_functor_axioms two_sided_disp_functor_to_disp_functor_data. Proof. split. - intros x xx ; cbn. rewrite twosided_disp_functor_id. unfold transportb_disp_mor2, transportf_disp_mor2. rewrite twosided_prod_transport. unfold transportb. apply maponpaths_2. apply isasetdirprod ; apply homset_property. - intros x y z xx yy zz f g ff gg ; cbn. rewrite twosided_disp_functor_comp. 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.