proposition: Proposition core_indexed_cat_laws : indexed_cat_laws core_indexed_cat_data.
proof: Proof. repeat split. - intros x y f xx ; cbn in *. use subtypePath. { intro. apply isaprop_is_z_isomorphism. } cbn. refine (indexed_cat_lunitor Φ f xx @ _). apply maponpaths. refine (_ @ !(@idtoiso_core (Φ y) _ _ _)). apply idpath. - intros x y f xx ; cbn in *. use subtypePath. { intro. apply isaprop_is_z_isomorphism. } cbn. refine (indexed_cat_runitor Φ f xx @ _). apply maponpaths. refine (_ @ !(@idtoiso_core (Φ y) _ _ _)). apply idpath. - intros w x y z f g h ww ; cbn in *. use subtypePath. { intro. apply isaprop_is_z_isomorphism. } cbn. refine (_ @ indexed_cat_lassociator Φ f g h ww). apply maponpaths. refine (@idtoiso_core (Φ z) _ _ _ @ _). apply idpath. 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.Core UniMath.CategoryTheory.Groupoids UniMath.CategoryTheory.IndexedCategories.IndexedCategory