Proposition indexed_functor_to_disp_functor_axioms : disp_functor_axioms indexed_functor_to_disp_functor_data. 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.
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.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedCategory. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedFunctor. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedCategoryToFibration.