Proposition indexed_cat_to_disp_cat_axioms : disp_cat_axioms C indexed_cat_to_disp_cat_data. Proof. repeat split. - intros x y f xx yy ff ; cbn in *. etrans. { apply maponpaths_2. exact (!(nat_trans_ax (indexed_cat_id Φ x) _ _ ff)). } cbn. rewrite !assoc'. etrans. { apply maponpaths. apply (indexed_cat_runitor_alt Φ). } unfold transportb. rewrite transportf_indexed_cat_to_disp_cat. apply idpath. - intros x y f xx yy ff ; cbn in *. rewrite !assoc'. etrans. { apply maponpaths. apply (indexed_cat_lunitor_alt Φ). } unfold transportb. rewrite transportf_indexed_cat_to_disp_cat. apply idpath. - intros w x y z f g h ww xx yy zz ff gg hh ; cbn in *. rewrite !functor_comp. rewrite !assoc'. etrans. { do 3 apply maponpaths. refine (!_). apply (indexed_cat_lassociator Φ h g f zz). } unfold transportb. rewrite transportf_indexed_cat_to_disp_cat. rewrite !assoc'. cbn. do 2 apply maponpaths. etrans. { do 2 refine (assoc _ _ _ @ _). etrans. { do 2 apply maponpaths_2. apply (nat_trans_ax (indexed_cat_comp Φ g f)). } do 2 refine (assoc' _ _ _ @ _). apply idpath. } do 6 apply maponpaths. apply homset_property. - intros x y f xx yy ; cbn in *. 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.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedCategory.