Definition op_indexed_cat_isos : indexed_cat_isos op_indexed_cat_data. Proof. split. - intros x xx. use opp_is_z_isomorphism. use is_z_isomorphism_comp. + apply (is_z_iso_inv_from_z_iso (indexed_cat_id_z_iso Φ xx)). + cbn. apply is_z_isomorphism_identity. - intros x y z f g xx. use opp_is_z_isomorphism. use is_z_isomorphism_comp. + apply (is_z_iso_inv_from_z_iso (indexed_cat_comp_z_iso Φ f g xx)). + cbn. apply is_z_isomorphism_identity. Defined.
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.opp_precat. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedCategory.