\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}