fact: Definition secovercoprodtoprod {X Y : UU} (P : X ⨿ Y -> UU) (a : ∏ xy : X ⨿ Y, P xy) : (∏ x, P (ii1 x)) × (∏ y : Y, P (ii2 y)) := make_dirprod (λ x, a (ii1 x)) (λ y : Y, a (ii2 y)).
imports: UniMath.Foundations.PartC