proposition: Proposition indexed_nat_trans_to_disp_nat_trans_axioms : disp_nat_trans_axioms indexed_nat_trans_to_disp_nat_trans_data.
proof: Proof. intros x y f xx yy ff ; cbn in *. unfold transportb, indexed_nat_trans_to_disp_nat_trans_data. rewrite !functor_comp. refine (_ @ !(transportf_indexed_cat_to_disp_cat _ _ _)). rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. do 2 apply maponpaths_2. exact (!(indexed_nat_trans_natural_inv m f yy)). } rewrite !assoc. etrans. { do 3 apply maponpaths_2. apply (nat_trans_ax (m x)). } rewrite !assoc'. apply maponpaths. refine (!_). etrans. { rewrite !assoc. do 2 apply maponpaths_2. etrans. { apply maponpaths_2. refine (!_). apply (nat_trans_ax (indexed_cat_id Ψ x)). } cbn. rewrite !assoc'. apply maponpaths. refine (!_). apply (nat_trans_ax (indexed_cat_id Ψ x)). } cbn. rewrite !assoc'. do 2 apply maponpaths. refine (_ @ !(indexed_cat_lunitor_alt Ψ _ _)). rewrite !assoc. etrans. { apply maponpaths_2. apply (indexed_cat_runitor_alt Ψ). } refine (!(pr1_idtoiso_concat _ _) @ _). do 2 apply maponpaths. refine (!(maponpathscomp0 (λ g, (Ψ $ g) (θ y yy)) _ _) @ _). apply maponpaths. apply homset_property. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.OppositeCategory.Core UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.IndexedCategories.IndexedCategory UniMath.CategoryTheory.IndexedCategories.IndexedFunctor UniMath.CategoryTheory.IndexedCategories.IndexedTransformation UniMath.CategoryTheory.IndexedCategories.IndexedCategoryToFibration UniMath.CategoryTheory.IndexedCategories.IndexedFunctorToCartesian