Definition binaryProductFunctor {B C:category} (F G:[B,C]) : [B,[C^op,SET]]. Proof. unshelve refine (makeFunctor _ _ _ _). - intro b. exact (HomPair (F ◾ b) (G ◾ b)). - intros b b' f. unshelve refine (makeNattrans_op _ _). + intros c w. exact (F ▭ f ∘ pr1 w ,, G ▭ f ∘ pr2 w). + abstract (intros c c' g; simpl; apply funextsec; intro v; apply dirprodeq; ( simpl; apply pathsinv0, assoc )) using _L_. - abstract (intro b; apply nat_trans_eq; [ apply homset_property | intro c; simpl; apply funextsec; intro v; apply dirprodeq; ( simpl; rewrite functor_on_id; rewrite id_right; reflexivity )]) using _L_. - abstract (intros b b' b'' f g; apply nat_trans_eq; [ apply homset_property | intro c; apply funextsec; intro w; apply dirprodeq ; ( simpl; rewrite functor_on_comp; rewrite assoc; reflexivity) ]) using _L_. 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.