Proposition disp_cat_axioms_of_strict_twosided_disp_cat : disp_cat_axioms cat_of_setcategory disp_cat_data_of_strict_twosided_disp_cat. Proof. repeat split. - cbn ; intros C₁ C₂ F D₁ D₂ FF. use eq_twosided_disp_functor. + intros x y xy ; cbn. exact (!(transportb_disp_cat_of_strict_twosided_disp_cat_ob _ _ _ _ _ _)). + intros x₁ x₂ f y₁ y₂ g xy₁ xy₂ fg ; cbn -[idtoiso_twosided_disp]. refine (!_). etrans. { do 2 apply maponpaths. apply transportb_disp_cat_of_strict_twosided_disp_cat_mor. } cbn -[idtoiso_twosided_disp]. rewrite (two_disp_post_whisker_f (D := D₂)). rewrite transport_f_f_disp_mor2. etrans. { apply maponpaths. apply (assoc_two_disp (D := D₂)). } unfold transportb_disp_mor2. rewrite transport_f_f_disp_mor2. etrans. { apply maponpaths. apply maponpaths_2. apply (assoc_two_disp (D := D₂)). } unfold transportb_disp_mor2. rewrite two_disp_pre_whisker_f. rewrite transport_f_f_disp_mor2. etrans. { apply maponpaths. do 2 apply maponpaths_2. apply (idtoiso_twosided_disp_concat (D := D₂)). } unfold transportb_disp_mor2. rewrite !two_disp_pre_whisker_f. rewrite transport_f_f_disp_mor2. rewrite idtoiso_twosided_disp_identity. etrans. { apply maponpaths. apply maponpaths_2. apply (id_two_disp_left (D := D₂)). } unfold transportb_disp_mor2. rewrite two_disp_pre_whisker_f. rewrite transport_f_f_disp_mor2. apply transportf_disp_mor2_idpath. - cbn ; intros C₁ C₂ F D₁ D₂ FF. use eq_twosided_disp_functor. + intros x y xy ; cbn. exact (!(transportb_disp_cat_of_strict_twosided_disp_cat_ob F _ _ (@id_right cat_of_setcategory _ _ F) FF xy)). + intros x₁ x₂ f y₁ y₂ g xy₁ xy₂ fg ; cbn -[idtoiso_twosided_disp]. refine (!_). etrans. { do 2 apply maponpaths. apply (transportb_disp_cat_of_strict_twosided_disp_cat_mor _ _ _ (id_right (C := cat_of_setcategory) F)). } cbn -[idtoiso_twosided_disp]. rewrite (two_disp_post_whisker_f (D := D₂)). rewrite transport_f_f_disp_mor2. etrans. { apply maponpaths. apply (assoc_two_disp (D := D₂)). } unfold transportb_disp_mor2. rewrite transport_f_f_disp_mor2. etrans. { apply maponpaths. apply maponpaths_2. apply (assoc_two_disp (D := D₂)). } unfold transportb_disp_mor2. rewrite two_disp_pre_whisker_f. rewrite transport_f_f_disp_mor2. etrans. { apply maponpaths. do 2 apply maponpaths_2. apply (idtoiso_twosided_disp_concat (D := D₂)). } unfold transportb_disp_mor2. rewrite !two_disp_pre_whisker_f. rewrite transport_f_f_disp_mor2. rewrite idtoiso_twosided_disp_identity. etrans. { apply maponpaths. apply maponpaths_2. apply (id_two_disp_left (D := D₂)). } unfold transportb_disp_mor2. rewrite two_disp_pre_whisker_f. rewrite transport_f_f_disp_mor2. apply transportf_disp_mor2_idpath. - cbn ; intros C₁ C₂ C₃ C₄ F G H D₁ D₂ D₃ D₄ FF GG HH. use eq_twosided_disp_functor. + intros x y xy ; cbn. exact (!(transportb_disp_cat_of_strict_twosided_disp_cat_ob _ _ _ (@assoc cat_of_setcategory _ _ _ _ F G H) (comp_twosided_disp_functor (comp_twosided_disp_functor FF GG) HH) xy)). + intros x₁ x₂ f y₁ y₂ g xy₁ xy₂ fg. refine (!_). etrans. { do 2 apply maponpaths. apply (transportb_disp_cat_of_strict_twosided_disp_cat_mor _ _ _ (assoc (C := cat_of_setcategory) F G H)). } cbn -[idtoiso_twosided_disp]. rewrite (two_disp_post_whisker_f (D := D₄)). rewrite transport_f_f_disp_mor2. etrans. { apply maponpaths. apply (assoc_two_disp (D := D₄)). } unfold transportb_disp_mor2. rewrite transport_f_f_disp_mor2. etrans. { apply maponpaths. apply maponpaths_2. apply (assoc_two_disp (D := D₄)). } unfold transportb_disp_mor2. rewrite two_disp_pre_whisker_f. rewrite transport_f_f_disp_mor2. etrans. { apply maponpaths. do 2 apply maponpaths_2. apply (idtoiso_twosided_disp_concat (D := D₄)). } unfold transportb_disp_mor2. rewrite !two_disp_pre_whisker_f. rewrite transport_f_f_disp_mor2. rewrite idtoiso_twosided_disp_identity. etrans. { apply maponpaths. apply maponpaths_2. apply (id_two_disp_left (D := D₄)). } unfold transportb_disp_mor2. rewrite two_disp_pre_whisker_f. rewrite transport_f_f_disp_mor2. apply transportf_disp_mor2_idpath. - intros. apply isaset_twosided_disp_functor. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.DisplayedCatEq. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.DispFunctorPair. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedNatTrans. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TransportLaws. Section FromIso. End FromIso.