Definition from_fiber_cod_data : psfunctor_data (strict_fiber_bicat (cod_disp_bicat B) (cod_local_iso_cleaving B) b) (slice_bicat b). Proof. use make_psfunctor_data. - exact (λ f, f). - exact (λ a₁ a₂ g, pr1 g ,, comp_of_invertible_2cell (rinvunitor_invertible_2cell _) (pr2 g)). - cbn. refine (λ a₁ a₂ g₁ g₂ β, pr1 β ,, _). abstract (cbn ; rewrite !vassocl ; refine (maponpaths (λ z, _ • z) (pr2 β) @ _) ; rewrite lwhisker_id2 ; rewrite id2_left ; apply idpath). - cbn. refine (λ a, id2 _ ,, _). abstract (cbn ; rewrite id2_rwhisker ; rewrite id2_right ; rewrite !vassocr ; rewrite rinvunitor_runitor ; rewrite id2_left ; apply idpath). - cbn. refine (λ a₁ a₂ a₃ g₁ g₂, id2 _ ,, _). abstract (cbn ; rewrite id2_rwhisker ; rewrite id2_right ; rewrite !vassocl ; apply maponpaths ; rewrite <- lwhisker_vcomp ; rewrite !vassocr ; do 2 apply maponpaths_2 ; rewrite !lwhisker_hcomp ; rewrite triangle_r_inv ; rewrite <- rwhisker_hcomp, <- lwhisker_hcomp ; rewrite !vassocl ; rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite rassociator_lassociator ; rewrite id2_left ; rewrite left_unit_inv_assoc ; rewrite !vassocr ; apply maponpaths_2 ; rewrite rinvunitor_natural ; rewrite <- rwhisker_hcomp ; apply maponpaths_2 ; refine (_ @ id2_right _) ; use vcomp_move_L_pM ; [ is_iso | ] ; cbn ; use vcomp_move_R_Mp ; [ is_iso | ] ; cbn ; rewrite id2_left ; rewrite <- runitor_triangle ; rewrite runitor_lunitor_identity ; rewrite lunitor_lwhisker ; apply idpath). 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.