proposition: Lemma functorOpIso {B C:category} : categoryIsomorphism [B, C]^op [B^op, C^op].
proof: Proof. unshelve refine (_,,_). { unshelve refine (_,,_). { exact functorOp. } { intros H H'. unshelve refine (isweq_iso _ _ _ _). { simpl. intros p. unshelve refine (makeNattrans _ _). { intros b. exact (pr1 p b). } { abstract (intros b b' f; simpl; exact (!nat_trans_ax p _ _ f)) using _L_. } } { abstract (intro p; apply nat_trans_eq; [ apply homset_property | intro b; reflexivity ]) using _L_. } { abstract (intro p; apply nat_trans_eq; [ apply homset_property | intro b; reflexivity ]) using _L_. } } } { simpl. unshelve refine (isweq_iso _ _ _ _). { exact (functor_opp : B^op ⟶ C^op -> B ⟶ C). } { abstract (intros H; simpl; apply (functor_eq _ _ (homset_property C)); unshelve refine (total2_paths_f _ _); reflexivity) using _L_. } { abstract (intros H; simpl; apply functor_eq; [ exact (homset_property C^op) | unshelve refine (total2_paths_f _ _); reflexivity]). } } Defined.
imports: UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.yoneda UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.MonoEpiIso UniMath.Foundations.Preamble UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics