Lemma sn_power_arrow_unique (t : ∑ (f: C ⟦c', sn_power_object⟧), ∏ i, f · sn_power_projection i = cone' i) : t = (sn_power_arrow ,, sn_power_arrow_commutes). Proof. apply subtypePairEquality. { intro. apply impred_isaprop. intro. apply homset_property. } apply BinProductArrowUnique. - apply ProductArrowUnique. intro i. refine (_ @ pr2 t _). refine (assoc' _ _ _ @ _). refine (maponpaths _ (!_)). exact (maponpaths _ (homotinvweqweq _ _)). - refine (!_ @ pr2 t _). apply maponpaths. exact (maponpaths _ (homotinvweqweq _ _)). 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.