\begin{code}

{-# OPTIONS --without-K #-}

module AlternativeCoproduct where

open import SetsAndFunctions
open import Two

_+'_ : Set  Set  Set
X₀ +' X₁ = Σ \(i : )  X i
 where
  X :   Set
  X  = X₀
  X  = X₁

\end{code}