proposition: Proposition indexed_functor_to_disp_functor_axioms : disp_functor_axioms indexed_functor_to_disp_functor_data.
proof: Proof. split. - intros x xx ; cbn in *. etrans. { apply maponpaths_2. exact (!(indexed_functor_id τ xx)). } refine (!_). use z_iso_inv_on_left. apply idpath. - intros x y z xx yy zz f g ff gg ; cbn in *. refine (!_). use z_iso_inv_on_left. rewrite !functor_comp. rewrite !assoc'. apply maponpaths. refine (!_). use z_iso_inv_on_right. etrans. { do 2 apply maponpaths. exact (indexed_functor_comp τ g f zz). } cbn. rewrite !assoc. apply maponpaths_2. refine (_ @ nat_trans_ax (indexed_functor_natural τ f) _ _ _). apply maponpaths_2. cbn. rewrite <- !functor_comp. apply maponpaths. rewrite !assoc'. rewrite z_iso_after_z_iso_inv. apply id_right. 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.Fibrations UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.IndexedCategories.IndexedCategory UniMath.CategoryTheory.IndexedCategories.IndexedFunctor UniMath.CategoryTheory.IndexedCategories.IndexedCategoryToFibration