Proposition indexed_nat_trans_to_disp_nat_trans_axioms : disp_nat_trans_axioms indexed_nat_trans_to_disp_nat_trans_data. 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.
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.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedCategory. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedFunctor. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedTransformation. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedCategoryToFibration. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedFunctorToCartesian.