Definition BinProduct_from_Product : BinProduct _ c d. Proof. use ((_ ,, _ ,, _) ,, (λ p' π₁ π₂, ((_ ,, _ ,, _) ,, _))). - exact (ProductObject _ _ P). - exact (ProductPr _ _ P true). - exact (ProductPr _ _ P false). - apply ProductArrow. intro i. induction i. + exact π₁. + exact π₂. - exact (ProductPrCommutes _ _ _ P _ _ true). - exact (ProductPrCommutes _ _ _ P _ _ false). - abstract ( intro t; apply subtypePath; [ intro; apply isapropdirprod; apply homset_property | ]; apply (ProductArrowUnique _ _ _ P); intro i; induction i; [ exact (pr12 t) | exact (pr22 t) ] ). Defined.
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.