Definition pair_equivalence_of_cats : equivalence_of_cats (category_binproduct C₁ C₂) (category_binproduct C₁' C₂'). Proof. use make_equivalence_of_cats. - use make_adjunction_data. + exact L. + exact R. + exact pair_equivalence_of_cats_unit. + exact pair_equivalence_of_cats_counit. - split. + intro x. use is_z_iso_binprod_z_iso. * exact (z_iso_is_z_isomorphism (nat_z_iso_pointwise_z_iso (unit_nat_z_iso_from_adj_equivalence_of_cats HF) (pr1 x))). * exact (z_iso_is_z_isomorphism (nat_z_iso_pointwise_z_iso (unit_nat_z_iso_from_adj_equivalence_of_cats HG) (pr2 x))). + intro x. use is_z_iso_binprod_z_iso. * exact (z_iso_is_z_isomorphism (nat_z_iso_pointwise_z_iso (counit_nat_z_iso_from_adj_equivalence_of_cats HF) (pr1 x))). * exact (z_iso_is_z_isomorphism (nat_z_iso_pointwise_z_iso (counit_nat_z_iso_from_adj_equivalence_of_cats HG) (pr2 x))). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.PrecategoryBinProduct.