Lemma TerminalToProduct (T : Terminal C): ∏ (a : stn 0 -> C), Product (stn 0) C a. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal.