Lemma BinaryProductFunctorAssoc {B C : category} (prod : BinaryProducts C) (F G : [B, C]) : z_iso (bifunctor_assoc (binaryProductFunctor F G)) (HomPair F G). Proof. unshelve refine (makeNatiso (C := [B, C]^op) _ _). { intro H. apply hset_equiv_z_iso. unshelve refine (weq_iso _ _ _ _). { intros w. unshelve refine (_,,_). { unshelve refine (makeNattrans _ _). { intro b. exact (pr1 (pr1 w b)). } { abstract (intros b b' f; exact (maponpaths dirprod_pr1 (pr2 w b b' f))) using _L_. } } { unshelve refine (makeNattrans _ _). { intro b. exact (pr2 (pr1 w b)). } { abstract (intros b b' f; exact (maponpaths dirprod_pr2 (pr2 w b b' f))) using _L_. } } } { simpl. intros pq. unshelve refine (_,,_). { intros b. exact (pr1 pq b ,, pr2 pq b). } { abstract (intros b b' f; simpl; apply dirprodeq; ( simpl; apply nattrans_naturality )) using _L_. } } { abstract (intros w; unshelve refine (total2_paths_f _ _); [ apply funextsec; intro b; apply pathsinv0; reflexivity | (apply funextsec; intro b; apply funextsec; intro b'; apply funextsec; intro f; apply isaset_dirprod; apply homset_property) ]) using _M_. } { abstract (intros pq; apply dirprodeq; ( apply nat_trans_eq; [ apply homset_property | intro b; reflexivity ] )) using _L_. } } { abstract (intros H H' p; apply funextsec; intros v; apply dirprodeq; ( simpl; apply nat_trans_eq; [ apply homset_property | intros b; unfold makeNattrans; simpl; 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.