\begin{code}

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

module MLTT.Plus-Type where

open import MLTT.Universes public

data _+_ {𝓤 𝓥} (X : 𝓤 ̇ ) (Y : 𝓥 ̇ ) : 𝓤 ⊔ 𝓥 ̇ where
 inl : X → X + Y
 inr : Y → X + Y

\end{code}