Lemma disp_prebicat_of_univ_disp_cats_laws : disp_prebicat_laws disp_prebicat_of_univ_disp_cats_data. Proof. repeat split ; red ; intros; intros ; apply (@disp_nat_trans_eq) ; intros ; apply pathsinv0 ; unfold transportb ; (etrans ; [ apply disp_nat_trans_transportf | ]). - apply pathsinv0. etrans. { apply id_left_disp. } apply pathsinv0; unfold transportb. apply maponpaths_2. apply homset_property. - apply pathsinv0. etrans. { apply id_right_disp. } apply pathsinv0; unfold transportb. apply maponpaths_2. apply homset_property. - apply pathsinv0. etrans. { apply assoc_disp. } apply pathsinv0; unfold transportb. apply maponpaths_2. apply homset_property. - apply transportf_set. apply homset_property. - apply pathsinv0. etrans. { cbn. apply disp_functor_id. } unfold transportb. apply maponpaths_2. apply homset_property. - apply transportf_set. apply homset_property. - cbn. etrans. { apply maponpaths. apply disp_functor_comp. } etrans. { apply transport_f_f. } apply transportf_set. apply homset_property. - cbn. etrans. { apply maponpaths. apply id_left_disp. } etrans. { apply transport_f_f. } apply pathsinv0. etrans. { apply id_right_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. etrans. { apply maponpaths. apply id_left_disp. } etrans. { apply transport_f_f. } apply pathsinv0. etrans. { apply id_right_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. etrans. { apply maponpaths. apply id_left_disp. } etrans. { apply transport_f_f. } apply pathsinv0. etrans. { apply id_right_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. etrans. { apply maponpaths. apply id_left_disp. } etrans. { apply transport_f_f. } apply pathsinv0. etrans. { apply id_right_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. etrans. { apply maponpaths. apply id_right_disp. } etrans. { apply transport_f_f. } apply pathsinv0. etrans. { apply id_left_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. set (RR := @disp_nat_trans_ax_var _ _ _ _ _ _ _ _ _ φφ). etrans. { apply maponpaths. apply RR. } etrans. { apply transport_f_f. } apply transportf_set. apply homset_property. - cbn. apply pathsinv0. etrans. { apply id_right_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. apply pathsinv0. etrans. { apply id_right_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. apply pathsinv0. etrans. { apply id_right_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. apply pathsinv0. etrans. { apply id_right_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. apply pathsinv0. etrans. { apply id_right_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. apply pathsinv0. etrans. { apply id_right_disp. } unfold transportb. apply maponpaths_2. apply homset_property. - cbn. apply pathsinv0. etrans. { apply id_left_disp. } etrans. { apply maponpaths. apply disp_functor_id. } etrans. { apply transport_f_f. } apply maponpaths_2. apply homset_property. - cbn. apply pathsinv0. etrans. { apply assoc_disp_var. } etrans. { apply maponpaths. apply id_left_disp. } etrans. { apply transport_f_f. } etrans. { apply maponpaths. apply id_left_disp. } etrans. { apply transport_f_f. } etrans. { apply maponpaths. apply disp_functor_id. } etrans. { apply transport_f_f. } apply pathsinv0. etrans. { apply maponpaths. apply id_left_disp. } etrans. { apply transport_f_f. } apply maponpaths_2. apply homset_property. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Adjunctions. Require Import UniMath.CategoryTheory.DisplayedCats.Equivalences. Require Import UniMath.CategoryTheory.DisplayedCats.DisplayedFunctorEq. Require Import UniMath.CategoryTheory.DisplayedCats.EquivalenceOverId. Require Import UniMath.CategoryTheory.DisplayedCats.DisplayedCatEq. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DisplayedBicats.Examples.FullSub. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sigma. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayedCatToBicat.