Definition strictify_unit_inv_data : pstrans_data (comp_psfunctor strictify (strict_psfunctor_to_psfunctor B₁ B₂)) (id_psfunctor _). Proof. use make_pstrans_data. - intros F. simple refine (((_ ,, _) ,, (_ ,, _ ,, _)) ,, tt). + exact (λ X, id₁ (pr111 F X)). + intros X Y f ; cbn. use make_invertible_2cell. * exact (lunitor _ • rinvunitor _). * is_iso. + abstract (intros X Y f g α ; cbn ; rewrite !vassocr ; apply strictify_unit_data_help1). + abstract (intros X ; cbn ; rewrite idtoiso_2_1_isotoid_2_1 ; rewrite !vassocr ; apply strictify_unit_data_help2). + abstract (intros X Y Z f g ; cbn ; rewrite idtoiso_2_1_isotoid_2_1 ; rewrite !vassocr ; apply strictify_unit_data_help3). - intros F₁ F₂ α. use make_invertible_2cell. + use make_strict_modification. * intros Z ; cbn. exact (lunitor _ • rinvunitor _). * abstract (intros X Y f ; cbn ; rewrite !vassocr ; apply strictify_unit_data_help4). + use make_is_invertible_strict_modification. intros X ; 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.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.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.PseudoFunctors.Display.StrictPseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.Display.Base. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map1Cells. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map2Cells. Require Import UniMath.Bicategories.PseudoFunctors.Display.StrictIdentitor. Require Import UniMath.Bicategories.PseudoFunctors.Display.StrictCompositor. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.StrictPseudoFunctor. Import PseudoFunctor.Notations. Import StrictPseudoFunctor.Notations. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.Modifications.Modification. Require Import UniMath.Bicategories.PseudoFunctors.Examples.StrictToPseudo. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition.