Lemma terminal_binprod_unit_l_z_aux {C : category} (T : Terminal C) (BC : BinProducts C) (x : C) : is_inverse_in_precat (BinProductPr2 C (BC T x)) (BinProductArrow C (BC T x) (TerminalArrow T x) (identity x)). Proof. unfold is_inverse_in_precat. split; [|apply BinProductPr2Commutes]. refine (precompWithBinProductArrow _ _ _ _ _ @ _). refine (_ @ !BinProductArrowEta _ _ _ _ _ (identity _)). apply maponpaths_12. - apply TerminalArrowEq. - exact (id_right _ @ !id_left _). Qed.
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.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.Combinatorics.StandardFiniteSets. Section BinProductFromIso. End BinProductFromIso. Section BinProductsFromProducts. End BinProductsFromProducts. Section ProductsFromBinProducts. End ProductsFromBinProducts.