proposition: Lemma TerminalToProduct (T : Terminal C): ∏ (a : stn 0 -> C), Product (stn 0) C a.
proof: Proof. intros a. use make_Product. - exact T. - exact(λ (x : ⟦ 0 ⟧), fromempty (weqstn0toempty x)). - intros c g. use unique_exists. + apply TerminalArrow. + exact(λ (x : ⟦ 0 ⟧), fromempty (weqstn0toempty x)). + intro; apply impred_isaprop. intro; apply homset_property. + intros; apply TerminalArrowEq. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Terminal