This relies on the new implementation of without-K currently available
in the development version of Agda only (included in Agda 24 April
2013).

\begin{code}

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

module SumDisjoint where

open import Equality
open import SetsAndFunctions

sum-disjoint : {X Y : Set} {x : X} {y : Y}  in₀ x  in₁ y  
sum-disjoint ()

\end{code}