Definition terminal_is_product : isProduct _ _ _ terminal_product_object terminal_product_projection. Proof. use (make_isProduct _ _ (homset_property C)). intros c' cone'. use make_iscontr. - use tpair. + exact (terminal_product_arrow c'). + exact (terminal_product_arrow_commutes c' cone'). - exact (terminal_product_arrow_unique c' cone'). 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.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Monics.