Definition total_category_isProduct : isProduct _ _ _ total_category_Product total_category_ProductPr. Proof. intros w f. use iscontraprop1. - apply total_category_ProductUnique. - simple refine (_ ,, _). + exact (total_category_ProductArrow (pr2 w) (λ i, pr2 (f i))). + exact (total_category_ProductPrCommutes (pr2 w) (λ i, pr2 (f i))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total.