Definition category_op_binproduct {C D:category}: ((C^op) × (D^op)) ⟶ (C × D)^op. Proof. use make_functor. + use make_functor_data. - use idfun. - intros (c,d) (c',d'). use idfun. + split. - intro. apply idpath. - repeat intro. apply idpath. Defined.
Require Import UniMath.Foundations.All. 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.FunctorCategory. Require Import UniMath.CategoryTheory.opp_precat.