Definition op_indexed_cat_data : indexed_cat_data C. Proof. use make_indexed_cat_data. - exact (λ x, op_unicat (Φ x)). - exact (λ x y f, functor_opp (Φ $ f)). - exact (λ x, nat_trans_comp _ _ _ (functor_identity_op _) (op_nt (nat_z_iso_inv (indexed_cat_id_nat_z_iso Φ x)))). - exact (λ x y z f g, nat_trans_comp _ _ _ (functor_comp_op_nat_z_iso _ _) (op_nt (nat_z_iso_inv (indexed_cat_comp_nat_z_iso Φ f g)))). 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.