Definition identity_map {C:category} (h:ZeroMaps C) {I} {d:I -> ob C} (dec : isdeceq I) (B:Sum d) (D:Product d) : Hom C (universalObject B) (universalObject D). Proof. intros. apply RawMatrix.from_matrix. apply identity_matrix. - assumption. - assumption. 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.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import