proposition: Lemma is_z_iso_constprod_functor1 a : @is_z_isomorphism [C,C] _ _ (nat_trans_constprod_functor1 a).
proof: Proof. exists (nat_trans_constprod_functor2 a). split. + abstract ( apply (nat_trans_eq C); intro x; simpl; unfold BinProduct_of_functors_ob; simpl; eapply pathscomp0; [apply precompWithBinProductArrow|]; now rewrite BinProductPr1Commutes, BinProductPr2Commutes, BinProductArrowEta, !id_left). + abstract ( apply (nat_trans_eq C); intro x; simpl; unfold BinProduct_of_functors_ob; simpl; eapply pathscomp0; [apply precompWithBinProductArrow|]; now rewrite BinProductPr1Commutes, BinProductPr2Commutes, BinProductArrowEta, !id_left). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.catiso UniMath.CategoryTheory.CategoryEquality UniMath.CategoryTheory.Core.Univalence