Definition DirectSum : Type := ∑ (ds : C) (ds_pr : ∏ i, Hom C ds (c i)) (ds_in : ∏ i, Hom C (c i) ds) (ds_id : ∏ i j, ds_pr i ∘ ds_in j = identity_matrix h c dec i j) (ds_isprod : ∏ c, isweq (λ f : Hom C c ds, λ i, ds_pr i ∘ f)), ∏ c, isweq (λ f : Hom C ds c, λ i, f ∘ ds_in i).
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