Lemma HomPairOp {B C : category} (F G : [B, C]) : z_iso (HomPair (functorOp F) (functorOp G) □ functorOp') (HomPair (opp_ob F) (opp_ob G)). Proof. unshelve refine (makeNatiso _ _). { intros H. apply hset_equiv_z_iso. apply weqdirprodf; exact (invweq (isomorphismOnMor functorOpIso H _)). } { abstract (intros H J p; apply funextsec; intro w; apply dirprodeq; ( apply nat_trans_eq; [ apply homset_property | reflexivity ] )). } Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import Require Import Require Import UniMath.MoreFoundations.Tactics.