Lemma BinProducts_from_Lims : Lims_of_shape two_graph C -> BinProducts C. Proof. intros H a b. set (LC := H (binproduct_diagram a b)). use make_BinProduct. + apply (lim LC). + apply (limOut LC true). + apply (limOut LC false). + apply (make_isBinProduct C); intros c f g. use unique_exists. - apply limArrow, (Binproduct f g). - abstract (split; [ apply (limArrowCommutes LC c (Binproduct f g) true) | apply (limArrowCommutes LC c (Binproduct f g) false) ]). - abstract (intros h; apply isapropdirprod; apply C). - abstract (now intros h [H1 H2]; apply limArrowUnique; intro x; induction x). 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.