Definition to_fiber_cod_unit_data : pstrans_data (id_psfunctor _) (comp_psfunctor from_fiber_cod to_fiber_cod). Proof. use make_pstrans_data. - cbn. exact (λ f, id₁ _ ,, linvunitor_invertible_2cell _). - cbn. refine (λ f₁ f₂ g, _). use make_invertible_2cell. + cbn. simple refine (_ ,, _). * cbn. exact (lunitor _ • rinvunitor _). * abstract (cbn ; rewrite !vassocr ; rewrite rinvunitor_runitor ; rewrite id2_left ; rewrite lwhisker_hcomp ; rewrite <- linvunitor_natural ; rewrite !vassocl ; apply maponpaths ; rewrite linvunitor_assoc ; rewrite !vassocl ; rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite rassociator_lassociator ; rewrite id2_left ; rewrite <- rwhisker_vcomp ; rewrite !vassocr ; use vcomp_move_R_Mp ; [ is_iso | ] ; cbn ; rewrite rwhisker_vcomp ; rewrite linvunitor_lunitor ; rewrite id2_rwhisker ; rewrite !vassocl ; rewrite runitor_rwhisker ; rewrite lwhisker_vcomp ; rewrite linvunitor_lunitor ; rewrite lwhisker_id2 ; apply idpath). + apply is_invertible_2cell_in_slice_bicat ; 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.