Definition toDirectSum {C:category} (h:ZeroMaps C) {I} (dec : isdeceq I) (d:I -> ob C) (B:Sum d) (D:Product d) (is: is_iso (identity_map h dec B D)) : DirectSum h I dec d. Proof. intros. set (id := identity_map h dec B D). refine (make_DirectSum h I dec d (universalObject D) (λ i, pr_ D i) (λ i, id ∘ in_ B i) _ _ _). { intros. exact (RawMatrix.from_matrix_entry_assoc D B (identity_matrix h d dec) i j). } { intros. exact (pr2 (universalProperty D c)). } { intros. assert (b : (λ (f : Hom C (universalObject D) c) (i : I), (f ∘ id) ∘ in_ B i) = (λ (f : Hom C (universalObject D) c) (i : I), f ∘ (id ∘ in_ B i))). { apply funextsec; intros f. apply funextsec; intros i. apply assoc. } destruct b. exact (twooutof3c (λ f, f ∘ id) (λ g i, g ∘ in_ B i) (iso_comp_right_isweq (id,,is) c) (pr2 (universalProperty B c))). } 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