Lemma hinhcoprod (X Y : UU) : ∥ (∥ X ∥ ⨿ ∥ Y ∥) ∥ -> ∥ X ⨿ Y ∥. Proof. intros is. unfold ishinh. intro P. intro CP. set (CPX := λ x : X, CP (ii1 x)). set (CPY := λ y : Y, CP (ii2 y)). set (is1P := is P). assert (f : (ishinh X) ⨿ (ishinh Y) -> P). apply (sumofmaps (hinhuniv CPX) (hinhuniv CPY)). apply (is1P f). Defined.