proposition: Lemma BinaryProductFunctorAssoc {B C : category} (prod : BinaryProducts C) (F G : [B, C]) : z_iso (bifunctor_assoc (binaryProductFunctor F G)) (HomPair F G).
proof: 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.
imports: UniMath.Foundations.Preamble UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.yoneda UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.MonoEpiIso UniMath.CategoryTheory.RepresentableFunctors.Bifunctor UniMath.CategoryTheory.RepresentableFunctors.Precategories UniMath.MoreFoundations.Tactics