Lemma functorOpIso {B C:category} : categoryIsomorphism [B, C]^op [B^op, C^op]. 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.
Require Import UniMath.MoreFoundations.Tactics.