Library UniMath.Bicategories.PseudoFunctors.Examples.Strictify

The inclusion of pseudofunctors into strict pseudofunctors for locally univalent bicategories *********************************************************************************
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.

Local Open Scope cat.

Opaque psfunctor pstrans.
Opaque strict_psfunctor.

Section Strictify.
  Variable (B₁ B₂ : bicat)
           (HB₂_2_1 : is_univalent_2_1 B₂).

  Local Arguments idtoiso_2_1 {_} {_} {_} {_} {_} _.
  Local Arguments isotoid_2_1 {_} _ {_} {_} {_} {_} _.

  Definition strictify_ob_data
    : psfunctor B₁ B₂ → strict_psfunctor_data B₁ B₂.
  Show proof.
    intros F.
    use make_strict_psfunctor_data.
    - exact (λ X, F X).
    - exact (λ _ _ f, #F f).
    - intros a b f g α ; cbn.
      exact (psfunctor_on_cells F α).
    - intro a ; cbn.
      exact (isotoid_2_1 HB₂_2_1 (psfunctor_id F a)).
    - intros a b c f g; cbn.
      exact (isotoid_2_1 HB₂_2_1 (psfunctor_comp F f g)).

  Definition strictify_ob_is_strict_psfunctor
             (F : psfunctor B₁ B₂)
    : is_strict_psfunctor (strictify_ob_data F).
  Show proof.
    repeat split ; try (apply F)
    ; intro ; intros ; cbn ;
      unfold StrictPseudoFunctorBicat.strict_psfunctor_id_cell,
      StrictPseudoFunctorBicat.strict_psfunctor_comp_cell ;
      cbn ;
      rewrite !idtoiso_2_1_isotoid_2_1 ;
      apply F.

  Definition strictify_ob
    : psfunctor B₁ B₂ → strict_psfunctor_bicat B₁ B₂.
  Show proof.
    intros F.
    use make_strict_psfunctor.
    - exact (strictify_ob_data F).
    - exact (strictify_ob_is_strict_psfunctor F).

  Definition strictify_mor_data
             (F G : psfunctor_bicat B₁ B₂)
             (η : pstrans F G)
    : strict_pstrans_data (strictify_ob F) (strictify_ob G).
  Show proof.
    use tpair ; cbn.
    - exact (λ X, η X).
    - exact (λ X Y f, psnaturality_of η f).

  Definition strictify_mor_is_strict_pstrans
             (F G : psfunctor_bicat B₁ B₂)
             (η : pstrans F G)
    : is_strict_pstrans (strictify_mor_data F G η).
  Show proof.
    repeat split.
    - intro ; intros ; cbn.
      apply (psnaturality_natural η).
    - intro ; intros ; cbn
      ; unfold strict_psfunctor_id_cell, strict_psfunctor_comp_cell ; cbn.
      rewrite !idtoiso_2_1_isotoid_2_1.
      apply (pstrans_id η).
    - intro ; intros ; cbn
      ; unfold strict_psfunctor_id_cell, strict_psfunctor_comp_cell
      ; cbn.
      rewrite !idtoiso_2_1_isotoid_2_1.
      apply (pstrans_comp η).

  Definition strictify_mor
             (F G : psfunctor_bicat B₁ B₂)
    : pstrans F G → strictify_ob F --> strictify_ob G.
  Show proof.
    intros η.
    use make_strict_pstrans.
    - exact (strictify_mor_data F G η).
    - exact (strictify_mor_is_strict_pstrans F G η).

  Definition strictify_cell
             (F G : psfunctor_bicat B₁ B₂)
             (η₁ η₂ : pstrans F G)
    : modification η₁ η₂
      →
      (strictify_mor _ _ η₁ ==> strictify_mor _ _ η₂).
  Show proof.
    intros m.
    use make_strict_modification.
    - exact (λ X, m X).
    - abstract (intros X Y f ;
                exact (modnaturality_of m _ _ f)).

  Definition strictify_identitor_help
             (F : psfunctor B₁ B₂)
    : is_strict_modification (λ X : B₁, id₂ ((pr111 (id₁ (strictify_ob F))) X)).
  Show proof.
    intros X Y f.
    rewrite lwhisker_id2.
    rewrite id2_rwhisker.
    rewrite id2_left, id2_right.
    reflexivity.

  Definition strictify_identitor
             (F : psfunctor B₁ B₂)
    : (id₁ (strictify_ob F))
      ==>
        strictify_mor F F (id₁ F).
  Show proof.
    use make_strict_modification.
    - exact (λ X, id₂ _).
    - exact (strictify_identitor_help F).

  Definition strictify_compositor_help
             (F₁ F₂ F₃ : psfunctor B₁ B₂)
             (η₁ : F₁ --> F₂)
             (η₂ : F₂ --> F₃)
    : is_strict_modification
        (λ X : B₁, id₂ ((pr111 (strictify_mor F₁ F₂ η₁ · strictify_mor F₂ F₃ η₂)) X)).
  Show proof.
    intros X Y f.
    rewrite lwhisker_id2.
    rewrite id2_rwhisker.
    rewrite id2_left, id2_right.
    reflexivity.

  Definition strictify_compositor
             (F₁ F₂ F₃ : psfunctor B₁ B₂)
             (η₁ : F₁ --> F₂)
             (η₂ : F₂ --> F₃)
    : (strictify_mor _ _ η₁)
        · strictify_mor _ _ η₂
        ==>
        strictify_mor _ _ (η₁ · η₂).
  Show proof.
    use make_strict_modification.
    - exact (λ X, id₂ _).
    - exact (strictify_compositor_help F₁ F₂ F₃ η₁ η₂).

  Definition strictify_data
    : psfunctor_data (psfunctor_bicat B₁ B₂) (strict_psfunctor_bicat B₁ B₂).
  Show proof.
    use make_psfunctor_data.
    - exact strictify_ob.
    - exact strictify_mor.
    - exact strictify_cell.
    - exact strictify_identitor.
    - exact strictify_compositor.

  Definition strictify_laws
    : psfunctor_laws strictify_data.
  Show proof.
    refine (_ ,, (_ ,, (_ ,, (_ ,, (_ ,, (_ ,, _))))))
    ; intro ; intros ; use strict_modification_eq ; intro ; cbn.
    - exact (idpath _).
    - exact (idpath _).
    - rewrite id2_rwhisker, !id2_left.
      exact (idpath _).
    - rewrite lwhisker_id2, !id2_left.
      exact (idpath _).
    - rewrite id2_rwhisker, lwhisker_id2, !id2_right, id2_left.
      exact (idpath _).
    - rewrite id2_left, id2_right.
      exact (idpath _).
    - rewrite id2_left, id2_right.
      exact (idpath _).

  Definition strictify_invertible_2cells
    : invertible_cells strictify_data.
  Show proof.
    split ; intros ; apply make_is_invertible_strict_modification
    ; intros ; cbn ; is_iso.

  Definition strictify
    : psfunctor (psfunctor_bicat B₁ B₂) (strict_psfunctor_bicat B₁ B₂).
  Show proof.
    use make_psfunctor.
    - exact strictify_data.
    - exact strictify_laws.
    - exact strictify_invertible_2cells.

  Definition strictify_counit_comp_comp
             (F : psfunctor B₁ B₂)
    : pstrans_data (strict_psfunctor_to_psfunctor_map B₁ B₂ (strictify_ob F)) F.
  Show proof.
    use make_pstrans_data.
    - exact (λ X, id₁ (F X)).
    - simple refine (λ X Y f, make_invertible_2cell _) ; cbn.
      + exact (lunitor (# F f) • rinvunitor (# F f)).
      + is_iso.

  Definition strictify_counit_comp_is_pstrans
             (F : psfunctor B₁ B₂)
    : is_pstrans (strictify_counit_comp_comp F).
  Show proof.
    repeat split.
    - intros X Y f g α ; simpl.
      etrans.
      {
        rewrite !vassocr.
        rewrite vcomp_lunitor.
        rewrite !vassocl.
        rewrite rinvunitor_natural.
        rewrite <- rwhisker_hcomp.
        apply idpath.
      }
      rewrite !vassocl.
      apply idpath.
    - intros X ; simpl.
      etrans.
      {
        rewrite !vassocr.
        rewrite vcomp_lunitor.
        rewrite !vassocl.
        rewrite rinvunitor_natural.
        rewrite <- rwhisker_hcomp.
        apply idpath.
      }
      rewrite !vassocl.
      rewrite lunitor_runitor_identity.
      rewrite lunitor_V_id_is_left_unit_V_id.
      do 2 apply maponpaths.
      unfold strict_psfunctor_id_cell, strict_psfunctor_id.
      cbn.
      rewrite idtoiso_2_1_isotoid_2_1.
      apply idpath.
    - intros X Y Z f g ; simpl.
      etrans.
      {
        rewrite !vassocr.
        rewrite vcomp_lunitor.
        rewrite !vassocl.
        rewrite rinvunitor_natural.
        rewrite <- rwhisker_hcomp.
        apply idpath.
      }
      refine (!_).
      etrans.
      {
        do 3 apply maponpaths_2.
        etrans.
        {
          apply maponpaths_2.
          rewrite <- rwhisker_vcomp.
          rewrite !vassocr.
          rewrite lunitor_triangle.
          apply idpath.
        }
        rewrite !vassocl.
        rewrite rwhisker_hcomp.
        rewrite <- triangle_r_inv.
        rewrite <- lwhisker_hcomp.
        apply idpath.
      }
      rewrite !vassocl.
      apply maponpaths.
      etrans.
      {
        rewrite !vassocr.
        do 2 apply maponpaths_2.
        rewrite lwhisker_vcomp.
        rewrite !vassocr.
        rewrite linvunitor_lunitor, id2_left.
        apply idpath.
      }
      rewrite rinvunitor_triangle.
      apply maponpaths.
      unfold strict_psfunctor_comp_cell, strict_psfunctor_comp.
      cbn.
      rewrite idtoiso_2_1_isotoid_2_1.
      apply idpath.

  Definition strictify_counit_comp
             (F : psfunctor B₁ B₂)
    : pstrans (strict_psfunctor_to_psfunctor_map B₁ B₂ (strictify_ob F)) F.
  Show proof.
    use make_pstrans.
    - exact (strictify_counit_comp_comp F).
    - exact (strictify_counit_comp_is_pstrans F).

  Definition strict_counit_data_help
             (F G : psfunctor B₁ B₂)
             (α : pstrans F G)
             (X Y : B₁)
             (f : X --> Y)
    : (rassociator (id₁ (F X)) ((pr111 α) X) (#G f))
        • (id₁ (F X) ◃ (psnaturality_of α f))
        • (lassociator (id₁ (F X)) (#F f) (α Y))
        • (((lunitor (# F f) • rinvunitor (# F f)) ▹ α Y))
        • (rassociator (# F f) (id₁ (F Y)) (α Y))
        • (# F f ◃ (lunitor (α Y) • rinvunitor (α Y)))
      =
      ((lunitor ((pr111 α) X) • rinvunitor (α X)) ▹ # G f)
        • (rassociator (α X) (id₁ (G X)) (# G f))
        • ((α X ◃ (lunitor (# G f) • rinvunitor (# G f))))
        • (lassociator (α X) (# G f) (id₁ (G Y)))
        • ((psnaturality_of α f ▹ id₁ (G Y)))
        • rassociator (# F f) (α Y) (id₁ (G Y)).
  Show proof.
    refine (!_).
    etrans.
    {
      do 4 apply maponpaths_2.
      rewrite <- rwhisker_vcomp.
      rewrite !vassocl.
      rewrite !rwhisker_hcomp.
      rewrite <- triangle_r_inv.
      rewrite <- rwhisker_hcomp, <- lwhisker_hcomp.
      apply idpath.
    }
    rewrite !vassocl.
    etrans.
    {
      apply maponpaths.
      rewrite !vassocr.
      rewrite lwhisker_vcomp.
      rewrite !vassocr.
      rewrite linvunitor_lunitor, id2_left.
      rewrite rinvunitor_triangle.
      rewrite rwhisker_hcomp.
      rewrite <- rinvunitor_natural.
      rewrite vassocl.
      rewrite <- left_unit_inv_assoc.
      apply idpath.
    }
    rewrite <- lwhisker_vcomp.
    rewrite !vassocr.
    apply maponpaths_2.
    rewrite !vassocl.
    refine (!_).
    etrans.
    {
      do 2 apply maponpaths.
      rewrite <- rwhisker_vcomp.
      rewrite !vassocr.
      rewrite lunitor_triangle.
      rewrite rwhisker_hcomp.
      etrans.
      {
        apply maponpaths_2.
        rewrite !vassocl.
        rewrite <- triangle_r_inv.
        rewrite <- lwhisker_hcomp.
        apply idpath.
      }
      rewrite !vassocl.
      rewrite lwhisker_vcomp.
      rewrite linvunitor_lunitor, lwhisker_id2, id2_right.
      apply idpath.
    }
    rewrite vcomp_lunitor.
    rewrite !vassocr.
    apply maponpaths_2.
    rewrite <- lunitor_triangle.
    rewrite !vassocr.
    rewrite rassociator_lassociator.
    apply id2_left.

  Definition strictify_counit_data
    : pstrans_data
        (comp_psfunctor (strict_psfunctor_to_psfunctor B₁ B₂) strictify)
        (id_psfunctor (psfunctor_bicat B₁ B₂)).
  Show proof.
    use make_pstrans_data.
    - exact strictify_counit_comp.
    - intros F G α.
      use make_invertible_modification.
      + intros Z ; cbn.
        use make_invertible_2cell.
        * exact (lunitor _ • rinvunitor _).
        * is_iso.
      + abstract (intros X Y f ; cbn ;
                  rewrite !vassocr ;
                  apply strict_counit_data_help).

  Definition strictify_counit_is_pstrans_help₁
             (F₁ F₂ : psfunctor B₁ B₂)
             (α β : pstrans F₁ F₂)
             (m : modification α β)
             (X : B₁)
    : (id₁ (F₁ X) ◃ (pr111 m) X) • (lunitor ((pr111 β) X) • rinvunitor ((pr111 β) X)) =
      (lunitor ((pr111 α) X) • rinvunitor ((pr111 α) X)) • (m X ▹ id₁ (F₂ X)).
  Show proof.
    rewrite !vassocr.
    rewrite vcomp_lunitor.
    rewrite !vassocl.
    rewrite rinvunitor_natural.
    rewrite rwhisker_hcomp.
    reflexivity.

  Definition strictify_counit_is_pstrans_help₂
             (F : psfunctor B₁ B₂)
             (X : B₁)
    : (id₁ (F X) ◃ id₂ (id₁ ((pr111 F) X)))
        • (lunitor (id₁ ((pr111 F) X)) • rinvunitor (id₁ ((pr111 F) X)))
      =
      (runitor (id₁ (F X)) • linvunitor (id₁ (F X)))
        • ((pr111 (pr1 (psfunctor_id
                  (comp_psfunctor (strict_psfunctor_to_psfunctor B₁ B₂) strictify) F)) X)
             ▹ id₁ (F X)).
  Show proof.
    rewrite !vassocr.
    rewrite vcomp_lunitor.
    rewrite runitor_lunitor_identity.
    rewrite !vassocl.
    apply maponpaths.
    rewrite id2_left.
    refine (!(id2_right _) @ _).
    rewrite lunitor_V_id_is_left_unit_V_id.
    apply maponpaths.
    rewrite <- id2_rwhisker.
    apply maponpaths.
    cbn.
    rewrite id2_left.
    apply idpath.

  Definition strictify_counit_is_pstrans_help₃
             (F₁ F₂ F₃ : psfunctor B₁ B₂)
             (α : pstrans F₁ F₂)
             (β : pstrans F₂ F₃)
             (X : B₁)
    : (id₁ (F₁ X) ◃ id₂ ((pr111 α) X · (pr111 β) X))
        • (lunitor ((pr111 α) X · (pr111 β) X) • rinvunitor ((pr111 α) X · (pr111 β) X))
      =
      ((((lassociator (id₁ (F₁ X)) ((pr111 α) X) ((pr111 β) X)
           • ((lunitor ((pr111 α) X) • rinvunitor ((pr111 α) X)) ▹ (pr111 β) X))
           • rassociator
               ((pr111 (# (comp_psfunctor (strict_psfunctor_to_psfunctor B₁ B₂) strictify) α)) X)
               (id₁ (F₂ X))
               ((pr111 β) X))
          • ((pr111 (# (comp_psfunctor (strict_psfunctor_to_psfunctor B₁ B₂) strictify) α)) X
            ◃ (lunitor ((pr111 β) X)
         • rinvunitor ((pr111 β) X))))
         • lassociator
             ((pr111
                 (# (comp_psfunctor (strict_psfunctor_to_psfunctor B₁ B₂) strictify) α))
                      X)
                 ((pr111 (# (comp_psfunctor (strict_psfunctor_to_psfunctor B₁ B₂) strictify) β))
                      X)
             (id₁ (F₃ X)))
        • ((pr111 ((pr222 (pr1 (comp_psfunctor (strict_psfunctor_to_psfunctor B₁ B₂) strictify)))
                     F₁ F₂ F₃ α β)) X ▹ id₁ (F₃ X)).
  Show proof.
    cbn.
    rewrite lwhisker_id2, !id2_left.
    rewrite id2_rwhisker, id2_right.
    rewrite <- !rwhisker_vcomp.
    rewrite !vassocr.
    rewrite lunitor_triangle.
    rewrite !vassocl.
    apply maponpaths.
    rewrite <- lwhisker_vcomp.
    rewrite !vassocl.
    rewrite rinvunitor_triangle.
    rewrite !vassocr.
    refine (!(id2_left _) @ _).
    apply maponpaths_2.
    rewrite !vassocl.
    rewrite lunitor_lwhisker.
    rewrite rwhisker_vcomp.
    rewrite rinvunitor_runitor, id2_rwhisker.
    apply idpath.

  Opaque comp_psfunctor.

  Definition strictify_counit_is_pstrans
    : is_pstrans strictify_counit_data.
  Show proof.
    refine (_ ,, _ ,, _).
    - intros F₁ F₂ α β m.
      rewrite (comp_psfunctor_cell (strict_psfunctor_to_psfunctor B₁ B₂) strictify m).
      assert (psfunctor_on_cells (strict_psfunctor_to_psfunctor B₁ B₂) (psfunctor_on_cells strictify m)
              =
              strict_psfunctor_cell_to_modification _ _ _ _ _ _ (strictify_cell _ _ _ _ m))
        as p.
      {
        apply idpath.
      }
      rewrite p.
      use modification_eq.
      exact (strictify_counit_is_pstrans_help₁ F₁ F₂ α β m).
    - intros F.
      use modification_eq.
      exact (strictify_counit_is_pstrans_help₂ F).
    - intros F₁ F₂ F₃ α β.
      use modification_eq.
      exact (strictify_counit_is_pstrans_help₃ F₁ F₂ F₃ α β).

  Transparent comp_psfunctor.

  Definition strictify_counit
    : pstrans
        (comp_psfunctor (strict_psfunctor_to_psfunctor B₁ B₂) strictify)
        (id_psfunctor _).
  Show proof.
    use make_pstrans.
    - exact strictify_counit_data.
    - exact strictify_counit_is_pstrans.

  Definition strictify_counit_inv_data_comp
             (F : psfunctor B₁ B₂)
    : pstrans_data F (strict_psfunctor_to_psfunctor_map B₁ B₂ (strictify_ob F)).
  Show proof.
    use make_pstrans_data.
    - exact (λ X, id₁ (F X)).
    - simple refine (λ X Y f, make_invertible_2cell _) ; cbn.
      + exact (lunitor (# F f) • rinvunitor (# F f)).
      + is_iso.

  Definition strictify_counit_inv_data_is_pstrans
             (F : psfunctor B₁ B₂)
    : is_pstrans (strictify_counit_inv_data_comp F).
  Show proof.
    repeat split.
    - intros X Y f g α ; cbn.
      etrans.
      {
        rewrite !vassocr.
        rewrite vcomp_lunitor.
        rewrite !vassocl.
        rewrite rinvunitor_natural.
        rewrite <- rwhisker_hcomp.
        apply idpath.
      }
      rewrite vassocl.
      apply idpath.
    - intros X ; cbn.
      etrans.
      {
        rewrite !vassocr.
        rewrite vcomp_lunitor.
        rewrite !vassocl.
        rewrite rinvunitor_natural.
        rewrite <- rwhisker_hcomp.
        apply idpath.
      }
      rewrite vassocl.
      rewrite lunitor_runitor_identity.
      rewrite lunitor_V_id_is_left_unit_V_id.
      do 2 apply maponpaths.
      unfold strict_psfunctor_id_cell, strict_psfunctor_id.
      cbn.
      rewrite idtoiso_2_1_isotoid_2_1.
      apply idpath.
    - intros X Y Z f g ; simpl.
      etrans.
      {
        rewrite !vassocr.
        rewrite vcomp_lunitor.
        rewrite !vassocl.
        rewrite rinvunitor_natural.
        rewrite <- rwhisker_hcomp.
        apply idpath.
      }
      refine (!_).
      etrans.
      {
        do 3 apply maponpaths_2.
        etrans.
        {
          apply maponpaths_2.
          rewrite <- rwhisker_vcomp.
          rewrite !vassocr.
          rewrite lunitor_triangle.
          apply idpath.
        }
        rewrite !vassocl.
        rewrite rwhisker_hcomp.
        rewrite <- triangle_r_inv.
        rewrite <- lwhisker_hcomp.
        apply idpath.
      }
      rewrite !vassocl.
      apply maponpaths.
      etrans.
      {
        rewrite !vassocr.
        do 2 apply maponpaths_2.
        rewrite lwhisker_vcomp.
        rewrite !vassocr.
        rewrite linvunitor_lunitor, id2_left.
        apply idpath.
      }
      rewrite rinvunitor_triangle.
      apply maponpaths.
      unfold strict_psfunctor_comp_cell, strict_psfunctor_comp.
      cbn.
      rewrite idtoiso_2_1_isotoid_2_1.
      apply idpath.

  Definition strictify_counit_inv_data
    : pstrans_data
        (id_psfunctor (psfunctor_bicat B₁ B₂))
        (comp_psfunctor (strict_psfunctor_to_psfunctor B₁ B₂) strictify).
  Show proof.
    use make_pstrans_data.
    - intro F.
      use make_pstrans.
      + exact (strictify_counit_inv_data_comp F).
      + exact (strictify_counit_inv_data_is_pstrans F).
    - intros F₁ F₂ α.
      use make_invertible_modification.
      + intros X.
        use make_invertible_2cell ; cbn.
        * exact (lunitor _ • rinvunitor _).
        * is_iso.
      + abstract (intros X Y f ; cbn ;
                  rewrite !vassocr ;
                  apply strict_counit_data_help).

  Definition strictify_counit_inv_is_pstrans
    : is_pstrans strictify_counit_inv_data.
  Show proof.
    refine (_ ,, _ ,, _).
    - intros F₁ F₂ α β m.
      use modification_eq.
      intro X ; cbn.
      rewrite !vassocr.
      rewrite vcomp_lunitor.
      rewrite !vassocl.
      rewrite rinvunitor_natural.
      rewrite rwhisker_hcomp.
      apply idpath.
    - intros F.
      use modification_eq.
      intros X ; cbn.
      rewrite id2_left, lwhisker_id2, id2_left.
      rewrite id2_rwhisker, id2_right.
      rewrite lunitor_runitor_identity.
      rewrite lunitor_V_id_is_left_unit_V_id.
      apply idpath.
    - intros F₁ F₂ F₃ α β.
      use modification_eq.
      intros X ; cbn.
      rewrite id2_left, lwhisker_id2, id2_left.
      rewrite id2_rwhisker, id2_right.
      rewrite <- rwhisker_vcomp.
      rewrite !vassocr.
      rewrite lunitor_triangle.
      rewrite !vassocl.
      apply maponpaths.
      rewrite <- lwhisker_vcomp.
      rewrite !vassocl.
      rewrite rinvunitor_triangle.
      refine (!(id2_left _) @ _).
      rewrite !vassocr.
      apply maponpaths_2.
      rewrite !vassocl.
      rewrite lunitor_lwhisker.
      rewrite rwhisker_vcomp.
      rewrite rinvunitor_runitor.
      rewrite id2_rwhisker.
      apply idpath.

  Definition strictify_counit_inv
    : pstrans
        (id_psfunctor _)
        (comp_psfunctor (strict_psfunctor_to_psfunctor B₁ B₂) strictify).
  Show proof.
    use make_pstrans.
    - exact strictify_counit_inv_data.
    - exact strictify_counit_inv_is_pstrans.

  Local Definition modifications_help
        (F : functor_data B₁ B₂)
        (X Y : B₁)
        (f : X --> Y)
    : (rassociator (id₁ (F X)) (id₁ (F X)) (#F f))
        • (id₁ (F X) ◃ (lunitor (# F f) • rinvunitor (# F f)))
        • lassociator (id₁ (F X)) (# F f) (id₁ (F Y))
        • ((lunitor (# F f) • rinvunitor (# F f)) ▹ id₁ (F Y))
        • rassociator (#F f) (id₁ (F Y)) (id₁ (F Y))
        • (# F f ◃ lunitor (id₁ (F Y)))
      =
      (lunitor (id₁ (F X)) ▹ # F f)
        • lunitor (#F f)
        • rinvunitor (#F f).
  Show proof.
    rewrite <- lwhisker_vcomp.
    rewrite !vassocr.
    rewrite lunitor_lwhisker.
    rewrite !vassocl.
    rewrite runitor_lunitor_identity.
    apply maponpaths.
    rewrite !vassocr.
    rewrite rinvunitor_triangle.
    rewrite !vassocl.
    rewrite lunitor_lwhisker.
    rewrite rwhisker_vcomp.
    rewrite !vassocl.
    rewrite rinvunitor_runitor, id2_right.
    rewrite rinvunitor_natural.
    rewrite rwhisker_hcomp.
    apply idpath.

  Definition modification_help_alt
             (F₁ F₂ : functor_data B₁ B₂)
             (α : nat_trans_data F₁ F₂)
             (X : B₁)
    : (rassociator (id₁ (F₁ X)) (id₁ (F₁ X)) (α X))
        • (id₁ (F₁ X) ◃ (lunitor (α X) • rinvunitor (α X)))
        • lassociator (id₁ (F₁ X)) (α X) (id₁ (F₂ X))
        • ((lunitor (α X) • rinvunitor (α X)) ▹ id₁ (F₂ X))
        • rassociator (α X) (id₁ (F₂ X)) (id₁ (F₂ X))
        • (α X ◃ lunitor (id₁ (F₂ X)))
      =
      (lunitor (id₁ (F₁ X)) ▹ α X)
        • lunitor (α X)
        • rinvunitor (α X).
  Show proof.
    rewrite !vassocl.
    rewrite lunitor_lwhisker.
    rewrite rwhisker_vcomp.
    rewrite !vassocl.
    rewrite rinvunitor_runitor, id2_right.
    refine (!_).
    etrans.
    {
      rewrite rinvunitor_natural, <- rwhisker_hcomp.
      apply idpath.
    }
    rewrite !vassocr.
    apply maponpaths_2.
    rewrite !vassocl.
    rewrite <- lwhisker_vcomp.
    rewrite !vassocl.
    rewrite rinvunitor_triangle.
    rewrite !vassocr.
    apply maponpaths_2.
    rewrite lunitor_lwhisker.
    rewrite runitor_lunitor_identity.
    apply idpath.

  Local Definition psfunctor_to_functor_data
        (F : psfunctor B₁ B₂)
    : functor_data B₁ B₂.
  Show proof.
    use make_functor_data.
    - exact (λ X, F X).
    - exact (λ _ _ f, #F f).

  Local Definition strict_psfunctor_to_functor_data
        (F : strict_psfunctor B₁ B₂)
    : functor_data B₁ B₂.
  Show proof.
    use make_functor_data.
    - exact (λ X, F X).
    - exact (λ _ _ f, #F f).

  Local Definition pstrans_to_nattrans_data
        {F₁ F₂ : psfunctor B₁ B₂}
        (α : pstrans F₁ F₂)
    : nat_trans_data
        (psfunctor_to_functor_data F₁)
        (psfunctor_to_functor_data F₂)
    := λ X, α X.

  Local Definition strict_pstrans_to_nattrans_data
        {F₁ F₂ : strict_psfunctor_bicat B₁ B₂}
        (α : F₁ --> F₂)
    : nat_trans_data
        (strict_psfunctor_to_functor_data F₁)
        (strict_psfunctor_to_functor_data F₂)
    := λ X, pr111 α X.

  Definition strictify_counit_inv_strictify_counit
    : invertible_modification
        (comp_pstrans
           strictify_counit_inv
           strictify_counit)
        (id_pstrans _).
  Show proof.
    use make_invertible_modification.
    - intros F.
      use make_invertible_modification.
      + intro X ; cbn.
        use make_invertible_2cell.
        * exact (lunitor (id₁ _)).
        * is_iso.
      + abstract (intros X Y f ; cbn ;
                  rewrite !vassocr ;
                  apply (modifications_help (psfunctor_to_functor_data F) X Y f)).
    - abstract (intros F₁ F₂ α ;
                apply modification_eq ;
                intros X ; cbn ;
                rewrite !vassocr ;
                apply (modification_help_alt
                         (psfunctor_to_functor_data F₁)
                         (psfunctor_to_functor_data F₂)
                         (pstrans_to_nattrans_data α))).

  Definition strictify_counit_strictify_counit_inv
    : invertible_modification
        (comp_pstrans
           strictify_counit
           strictify_counit_inv)
        (id_pstrans _).
  Show proof.
    use make_invertible_modification.
    - intros F.
      use make_invertible_modification.
      + intro X ; cbn.
        use make_invertible_2cell.
        * exact (lunitor (id₁ _)).
        * is_iso.
      + abstract (intros X Y f ; cbn ;
                  rewrite !vassocr ;
                  apply (modifications_help (psfunctor_to_functor_data F) X Y f)).
    - abstract (intros F₁ F₂ α ;
                apply modification_eq ;
                intros X ; cbn ;
                rewrite !vassocr ;
                apply (modification_help_alt
                         (psfunctor_to_functor_data F₁)
                         (psfunctor_to_functor_data F₂)
                         (pstrans_to_nattrans_data α))).

  Definition strictify_unit_data_help1
             (F : strict_psfunctor B₁ B₂)
             (X Y : B₁)
             (f g : B₁ ⟦ X, Y ⟧)
             (α : f ==> g)
    : (id₁ (F X) ◃ ## F α)
        • lunitor (# F g)
        • rinvunitor (# F g)
      =
      (lunitor (# F f) • rinvunitor (# F f))
        • (##F α ▹ id₁ ((pr111 F) Y)).
  Show proof.
    rewrite vcomp_lunitor.
    rewrite !vassocl.
    rewrite rinvunitor_natural.
    rewrite rwhisker_hcomp.
    apply idpath.

  Definition strictify_unit_data_help2
             (F : strict_psfunctor B₁ B₂)
             (X : B₁)
    : (id₁ (F X) ◃ psfunctor_id (strict_psfunctor_to_psfunctor_map B₁ B₂ F) X)
        • lunitor (# F (id₁ X))
        • rinvunitor (# F (id₁ X))
      =
      (runitor (id₁ (F X)) • linvunitor (id₁ (F X)))
        • (idtoiso_2_1 (strict_psfunctor_id F X) ▹ id₁ (F X)).
  Show proof.
    rewrite vcomp_lunitor.
    rewrite !vassocl.
    rewrite rinvunitor_natural.
    rewrite rwhisker_hcomp.
    rewrite lunitor_runitor_identity.
    rewrite lunitor_V_id_is_left_unit_V_id.
    apply idpath.

  Definition strictify_unit_data_help3
             (F : strict_psfunctor B₁ B₂)
             (X Y Z : B₁)
             (f : X --> Y)
             (g : Y --> Z)
    : ((id₁ ((pr111 F) X) ◃ psfunctor_comp (strict_psfunctor_to_psfunctor_map B₁ B₂ F) f g)
         • lunitor (# F (f · g))) • rinvunitor (# F (f · g))
      =
      (lassociator (id₁ ((pr111 F) X)) (# F f) (# F g))
        • ((lunitor (# F f) • rinvunitor (# F f)) ▹ # F g)
        • rassociator (#F f) (id₁ (F Y)) (# F g)
        • (# F f ◃ (lunitor (# F g) • rinvunitor (# F g)))
        • lassociator (#F f) (#F g) (id₁ ((pr111 F) Z))
        • (idtoiso_2_1 ((pr222 (pr1 F)) X Y Z f g) ▹ id₁ ((pr111 F) Z)).
  Show proof.
    rewrite vcomp_lunitor.
    rewrite <- !rwhisker_vcomp.
    rewrite !vassocr.
    rewrite lunitor_triangle.
    rewrite !vassocl.
    apply maponpaths.
    rewrite !vassocr.
    rewrite rwhisker_hcomp.
    rewrite <- triangle_r_inv.
    rewrite <- lwhisker_hcomp.
    rewrite lwhisker_vcomp.
    rewrite !vassocr.
    rewrite linvunitor_lunitor, id2_left.
    rewrite rinvunitor_triangle.
    rewrite rinvunitor_natural.
    rewrite rwhisker_hcomp.
    apply idpath.

  Definition strictify_unit_data_help4
             (F₁ F₂ : strict_psfunctor B₁ B₂)
             (α : strict_psfunctor_bicat B₁ B₂ ⟦ F₁ , F₂ ⟧)
             (X Y : B₁)
             (f : X --> Y)
    : (rassociator (id₁ ((pr111 F₁) X)) ((pr111 α) X) (# F₂ f))
        • (id₁ ((pr111 F₁) X) ◃ (pr211 α) X Y f)
        • lassociator (id₁ (F₁ X)) (# F₁ f) ((pr111 α) Y)
        • ((lunitor (# F₁ f) • rinvunitor (# F₁ f)) ▹ (pr111 α) Y)
        • rassociator (#F₁ f) (id₁ (F₁ Y)) ((pr111 α) Y)
        • (# F₁ f ◃ (lunitor ((pr111 α) Y) • rinvunitor ((pr111 α) Y)))
      =
      ((lunitor ((pr111 α) X) • rinvunitor ((pr111 α) X)) ▹ # F₂ f)
        • rassociator ((pr111 α) X) (id₁ (F₂ X)) (# F₂ f)
        • ((pr111 α) X ◃ (lunitor (# F₂ f) • rinvunitor (# F₂ f)))
        • lassociator ((pr111 α) X) ((pr211 F₂) X Y f) (id₁ (F₂ Y))
        • ((pr211 α) X Y f ▹ id₁ ((pr111 F₂) Y))
        • rassociator (#F₁ f) ((pr111 α) Y) (id₁ (F₂ Y)).
  Show proof.
    refine (!_).
    etrans.
    {
      apply maponpaths_2.
      etrans.
      {
        apply maponpaths_2.
        etrans.
        {
          apply maponpaths_2.
          etrans.
          {
            apply maponpaths_2.
            rewrite <- rwhisker_vcomp.
            rewrite !vassocl.
            rewrite !rwhisker_hcomp.
            rewrite <- triangle_r_inv.
            rewrite <- rwhisker_hcomp, <- lwhisker_hcomp.
            apply idpath.
          }
          rewrite !vassocl.
          rewrite lwhisker_vcomp.
          apply maponpaths.
          rewrite !vassocr.
          rewrite linvunitor_lunitor, id2_left.
          apply idpath.
        }
        rewrite !vassocl.
        rewrite rinvunitor_triangle.
        apply idpath.
      }
      rewrite !vassocl.
      rewrite !rwhisker_hcomp.
      rewrite <- rinvunitor_natural.
      rewrite <- rwhisker_hcomp.
      apply idpath.
    }
    etrans.
    {
      rewrite !vassocl.
      rewrite <- left_unit_inv_assoc.
      apply idpath.
    }
    refine (!_).
    etrans.
    {
      rewrite !vassocl.
      rewrite <- lwhisker_vcomp.
      rewrite !vassocr.
      apply idpath.
    }
    rewrite !vassocr.
    apply maponpaths_2.
    etrans.
    {
      rewrite !vassocl.
      rewrite lunitor_lwhisker.
      rewrite rwhisker_vcomp.
      rewrite !vassocl.
      rewrite rinvunitor_runitor, id2_right.
      rewrite lunitor_triangle.
      rewrite vcomp_lunitor.
      rewrite !vassocr.
      apply idpath.
    }
    apply maponpaths_2.
    use vcomp_move_R_pM.
    { is_iso. }
    rewrite lunitor_triangle.
    apply idpath.

  Definition strictify_unit_data
    : pstrans_data
        (id_psfunctor (strict_psfunctor_bicat B₁ B₂))
        (comp_psfunctor strictify (strict_psfunctor_to_psfunctor B₁ B₂)).
  Show 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.

  Definition strictify_unit_is_pstrans
    : is_pstrans strictify_unit_data.
  Show proof.
    repeat split.
    - intros F₁ F₂ α β m.
      use strict_modification_eq.
      intros X ; cbn.
      rewrite !vassocr.
      rewrite vcomp_lunitor.
      rewrite !vassocl.
      rewrite rinvunitor_natural.
      rewrite rwhisker_hcomp.
      apply idpath.
    - intros F.
      use strict_modification_eq.
      intros X ; cbn.
      rewrite id2_left, lwhisker_id2, id2_left.
      rewrite id2_rwhisker, id2_right.
      rewrite lunitor_runitor_identity.
      rewrite lunitor_V_id_is_left_unit_V_id.
      apply idpath.
    - intros F₁ F₂ F₃ α β.
      use strict_modification_eq.
      intros X ; cbn.
      rewrite id2_left, lwhisker_id2, id2_left.
      rewrite id2_rwhisker, id2_right.
      rewrite <- rwhisker_vcomp.
      rewrite !vassocr.
      rewrite lunitor_triangle.
      rewrite !vassocl.
      apply maponpaths.
      rewrite <- lwhisker_vcomp.
      rewrite !vassocl.
      rewrite rinvunitor_triangle.
      refine (!(id2_left _) @ _).
      rewrite !vassocr.
      apply maponpaths_2.
      rewrite !vassocl.
      rewrite lunitor_lwhisker.
      rewrite rwhisker_vcomp.
      rewrite rinvunitor_runitor.
      rewrite id2_rwhisker.
      apply idpath.

  Definition strictify_unit
    : pstrans
        (id_psfunctor _)
        (comp_psfunctor strictify (strict_psfunctor_to_psfunctor B₁ B₂)).
  Show proof.
    use make_pstrans.
    - exact strictify_unit_data.
    - exact strictify_unit_is_pstrans.

  Definition strictify_unit_inv_data
    : pstrans_data
        (comp_psfunctor strictify (strict_psfunctor_to_psfunctor B₁ B₂))
        (id_psfunctor _).
  Show 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.

  Definition strictify_unit_is_pstrans_help₁
             (F₁ F₂ : strict_psfunctor_bicat B₁ B₂)
             (α β : F₁ --> F₂)
             (m : α ==> β)
             (X : B₁)
    : (id₁ (pr111 F₁ X) ◃ (pr111 m) X)
        • (lunitor ((pr111 β) X) • rinvunitor ((pr111 β) X))
      =
      (lunitor ((pr111 α) X) • rinvunitor ((pr111 α) X)) • (pr111 m X ▹ id₁ (pr111 F₂ X)).
  Show proof.
    rewrite !vassocr.
    rewrite vcomp_lunitor.
    rewrite !vassocl.
    rewrite rinvunitor_natural.
    rewrite rwhisker_hcomp.
    reflexivity.

  Definition strictify_unit_is_pstrans_help₂
             (F : strict_psfunctor B₁ B₂)
             (X : B₁)
    : (id₁ ((pr111 F) X) ◃ id₂ (id₁ ((pr111 F) X)))
         • (lunitor (id₁ ((pr111 F) X)) • rinvunitor (id₁ ((pr111 F) X)))
       =
       (runitor (id₁ ((pr111 F) X)) • linvunitor (id₁ ((pr111 F) X)))
         • ((pr111 ((pr122 (pr1
                              (comp_psfunctor strictify
                                       (strict_psfunctor_to_psfunctor B₁ B₂)))) F)) X
                                                                                                ▹ id₁ ((pr111 F) X)).
  Show proof.
    rewrite !vassocr.
    rewrite vcomp_lunitor.
    rewrite runitor_lunitor_identity.
    rewrite !vassocl.
    apply maponpaths.
    rewrite id2_left.
    refine (!(id2_right _) @ _).
    rewrite lunitor_V_id_is_left_unit_V_id.
    apply maponpaths.
    rewrite <- id2_rwhisker.
    apply maponpaths.
    cbn.
    rewrite id2_left.
    apply idpath.

  Definition strictify_unit_is_pstrans_help₃
             (F₁ F₂ F₃ : strict_psfunctor_bicat B₁ B₂)
             (α : F₁ --> F₂)
             (β : F₂ --> F₃)
             (X : B₁)
    : (id₁ ((pr111 F₁) X) ◃ id₂ ((pr111 α) X · (pr111 β) X))
        • (lunitor ((pr111 α) X · (pr111 β) X) • rinvunitor ((pr111 α) X · (pr111 β) X))
      =
      ((((lassociator (id₁ ((pr111 F₁) X)) ((pr111 α) X) ((pr111 β) X)
           • ((lunitor ((pr111 α) X) • rinvunitor ((pr111 α) X)) ▹ (pr111 β) X))
           • rassociator
               ((pr111 (# (comp_psfunctor strictify (strict_psfunctor_to_psfunctor B₁ B₂)) α)) X)
               (id₁ ((pr111 F₂) X))
               ((pr111 β) X))
          • ((pr111 (# (comp_psfunctor
                          strictify
                          (strict_psfunctor_to_psfunctor B₁ B₂)) α)) X
               ◃ (lunitor ((pr111 β) X) • rinvunitor ((pr111 β) X))))
         • lassociator
             ((pr111 (# (comp_psfunctor strictify (strict_psfunctor_to_psfunctor B₁ B₂)) α)) X)
             ((pr111 (# (comp_psfunctor strictify (strict_psfunctor_to_psfunctor B₁ B₂)) β)) X)
             (id₁ ((pr111 F₃) X)))
        • ((pr111 ((pr222 (pr1 (comp_psfunctor
                                  strictify
                                  (strict_psfunctor_to_psfunctor B₁ B₂)))) F₁ F₂ F₃ α
                                  β)) X ▹ id₁ ((pr111 F₃) X)).
  Show proof.
    cbn.
    rewrite lwhisker_id2, !id2_left.
    rewrite id2_rwhisker, id2_right.
    rewrite <- !rwhisker_vcomp.
    rewrite !vassocr.
    rewrite lunitor_triangle.
    rewrite !vassocl.
    apply maponpaths.
    rewrite <- lwhisker_vcomp.
    rewrite !vassocl.
    rewrite rinvunitor_triangle.
    rewrite !vassocr.
    refine (!(id2_left _) @ _).
    apply maponpaths_2.
    rewrite !vassocl.
    rewrite lunitor_lwhisker.
    rewrite rwhisker_vcomp.
    rewrite rinvunitor_runitor, id2_rwhisker.
    apply idpath.

  Opaque comp_psfunctor.

  Definition strictify_unit_inv_is_pstrans
    : is_pstrans strictify_unit_inv_data.
  Show proof.
    refine (_ ,, _ ,, _).
    - intros F₁ F₂ α β m.
      use strict_modification_eq.
      exact (strictify_unit_is_pstrans_help₁ F₁ F₂ α β m).
    - intros F.
      use strict_modification_eq.
      exact (strictify_unit_is_pstrans_help₂ F).
    - intros F₁ F₂ F₃ α β.
      use strict_modification_eq.
      exact (strictify_unit_is_pstrans_help₃ F₁ F₂ F₃ α β).

  Transparent comp_psfunctor.

  Definition strictify_unit_inv
    : pstrans
        (comp_psfunctor strictify (strict_psfunctor_to_psfunctor B₁ B₂))
        (id_psfunctor _).
  Show proof.
    use make_pstrans.
    - exact strictify_unit_inv_data.
    - exact strictify_unit_inv_is_pstrans.

  Definition strictify_unit_strictify_unit_inv
    : invertible_modification
        (comp_pstrans
           strictify_unit
           strictify_unit_inv)
        (id_pstrans _).
  Show proof.
    use make_invertible_modification.
    - intros F.
      use make_invertible_2cell.
      + use make_strict_modification.
        * intro X ; cbn.
          exact (lunitor (id₁ _)).
        * abstract
            (intros X Y f ; cbn ;
             rewrite !vassocr ;
             apply (modifications_help (strict_psfunctor_to_functor_data F) X Y f)).
      + use make_is_invertible_strict_modification.
        intro X ; cbn.
        is_iso.
    - abstract (intros F₁ F₂ α ;
                apply strict_modification_eq ;
                intros X ; cbn ;
                rewrite !vassocr ;
                apply (modification_help_alt
                         (strict_psfunctor_to_functor_data F₁)
                         (strict_psfunctor_to_functor_data F₂)
                         (strict_pstrans_to_nattrans_data α))).

  Definition strictify_unit_inv_strictify_unit
    : invertible_modification
        (comp_pstrans
           strictify_unit_inv
           strictify_unit)
        (id_pstrans _).
  Show proof.
    use make_invertible_modification.
    - intros F.
      use make_invertible_2cell.
      + use make_strict_modification.
        * intro X ; cbn.
          exact (lunitor (id₁ _)).
        * abstract
            (intros X Y f ; cbn ;
             rewrite !vassocr ;
             apply (modifications_help (strict_psfunctor_to_functor_data F) X Y f)).
      + use make_is_invertible_strict_modification.
        intro X ; cbn.
        is_iso.
    - abstract (intros F₁ F₂ α ;
                apply strict_modification_eq ;
                intros X ; cbn ;
                rewrite !vassocr ;
                apply (modification_help_alt
                         (strict_psfunctor_to_functor_data F₁)
                         (strict_psfunctor_to_functor_data F₂)
                         (strict_pstrans_to_nattrans_data α))).
End Strictify.