Definition modification_to_indexed_nat_trans {C : category} {F G : psfunctor (cat_to_bicat C) bicat_of_univ_cats} {τ θ : pstrans F G} (m : modification τ θ) : indexed_nat_trans (pstrans_to_indexed_functor τ) (pstrans_to_indexed_functor θ). Proof. use make_indexed_nat_trans. - exact (λ x, m x). - abstract (intros x y f xx ; exact (nat_trans_eq_pointwise (modnaturality_of m x y f) xx)). Defined.
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.OppositeCategory.Core. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedCategory. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedFunctor. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedTransformation. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Discreteness. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Examples.DiscreteBicat. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Examples.PseudoFunctorsIntoCat. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.Transformations.Examples.PseudoTransformationIntoCat. Require Import UniMath.Bicategories.Modifications.Modification.