Definition cod_counit_inv_left_data : invertible_modification_data (comp_pstrans to_fiber_cod_counit_inv to_fiber_cod_counit) (id_pstrans _). Proof. intros x. use make_invertible_2cell. - simple refine (_ ,, _). + exact (lunitor _). + abstract (cbn ; rewrite lwhisker_id2, id2_left ; rewrite !vassocl ; rewrite lunitor_runitor_identity ; rewrite runitor_rwhisker ; rewrite lwhisker_vcomp ; rewrite !vassocl ; rewrite linvunitor_lunitor ; rewrite id2_right ; rewrite <- rwhisker_vcomp ; rewrite !vassocl ; rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite <- lunitor_lwhisker ; rewrite !vassocl ; rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite lassociator_rassociator ; rewrite id2_left ; rewrite !vassocr ; rewrite lwhisker_vcomp ; rewrite linvunitor_lunitor ; rewrite lwhisker_id2 ; rewrite id2_left ; rewrite !vassocl ; rewrite runitor_triangle ; rewrite vcomp_runitor ; apply idpath). - use strict_fiber_bicat_invertible_2cell. use is_disp_invertible_2cell_cod. 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.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.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Slice. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Codomain. 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.CodomainCleaving.