Definition to_fiber_disp_map_counit_inv_data : pstrans_data (id_psfunctor _) (comp_psfunctor to_fiber_disp_map from_fiber_disp_map). Proof. use make_pstrans_data. - refine (λ x, id₁ _ ,, id_pred_mor D _ ,, _). exact (comp_of_invertible_2cell (runitor_invertible_2cell _) (linvunitor_invertible_2cell _)). - intros x y f. use make_invertible_2cell. + simple refine (_ ,, _). * cbn. exact (lunitor _ • rinvunitor _). * abstract (cbn ; rewrite lwhisker_id2, id2_left ; rewrite <- !rwhisker_vcomp ; rewrite !vassocl ; do 2 apply maponpaths ; rewrite !vassocr ; rewrite runitor_rinvunitor ; rewrite id2_left ; use vcomp_move_R_Mp ; [ is_iso | ] ; cbn ; rewrite !vassocl ; rewrite runitor_rwhisker ; rewrite lwhisker_vcomp ; rewrite !vassocl ; rewrite linvunitor_lunitor ; rewrite id2_right ; rewrite runitor_triangle ; rewrite lunitor_triangle ; rewrite vcomp_lunitor ; rewrite vcomp_runitor ; rewrite !vassocr ; apply maponpaths_2 ; rewrite !vassocl ; rewrite <- lunitor_triangle ; rewrite (maponpaths (λ z, _ • (_ • z)) (vassocr _ _ _)) ; rewrite rassociator_lassociator ; rewrite id2_left ; rewrite rwhisker_vcomp ; rewrite linvunitor_lunitor ; rewrite id2_rwhisker ; rewrite id2_right ; rewrite <- runitor_triangle ; rewrite runitor_lunitor_identity ; rewrite lunitor_lwhisker ; apply idpath). + apply strict_fiber_bicat_invertible_2cell. use is_invertible_to_is_disp_invertible. cbn. is_iso. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Logic.DisplayMapBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayMapBicatToDispBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayMapBicatSlice. Require Import UniMath.Bicategories.DisplayedBicats.FiberBicategory. Require Import UniMath.Bicategories.DisplayedBicats.CleavingOfBicat. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.Modifications.Modification. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition. Require Import UniMath.Bicategories.PseudoFunctors.Biequivalence. Require Import UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.DisplayMapBicatCleaving.