Definition cartesian_cube_category_binproducts : BinProducts cartesian_cube_category. Proof. intros m n. use make_BinProduct. - exact (m + n). - exact (λ i : ⟦m⟧, inl (stn_left _ _ i)). - exact (λ i : ⟦n⟧, inl (stn_right _ _ i)). - use make_isBinProduct. + intros l f g. use unique_exists. * intro i. induction (weqfromcoprodofstn_invmap _ _ i) as [x1 | x2]; [exact (f x1) | exact (g x2)]. * cbn. split; apply funextfun; intro i. -- assert (H : weqfromcoprodofstn_invmap _ _ (stn_left m n i) = inl i). { now rewrite <- weqfromcoprodofstn_eq1. } now rewrite H. -- assert (H : weqfromcoprodofstn_invmap _ _ (stn_right m n i) = inr i). { now rewrite <- weqfromcoprodofstn_eq1. } now rewrite H. * intro h. now apply isapropdirprod; apply homset_property. * intros h [H1 H2]. apply funextfun; intros i. rewrite <- (maponpaths h (weqfromcoprodofstn_eq2 _ _ i)). induction (weqfromcoprodofstn_invmap _ _ i) as [x1 | x2]; [now rewrite <- H1 | now rewrite <- H2]. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Presheaf. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.ExponentiationLeftAdjoint. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.Categories.HSET.Structures.