proposition: Proposition indexed_cat_to_disp_cat_axioms : disp_cat_axioms C indexed_cat_to_disp_cat_data.
proof: 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.
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.IndexedCategories.IndexedCategory