    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Sums (disjoint unions)
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.Sum where

    open import Data.Unit.Polymorphic.Base using (⊤; tt)
    open import Data.Maybe.Base using (Maybe; just; nothing)
    open import Level
    import Relation.Nullary.Decidable.Core as Dec

    private
      variable
        a b : Level
        A B : Set a

    ------------------------------------------------------------------------
    -- Re-export content from base module

    open import Data.Sum.Base public

    ------------------------------------------------------------------------
    -- Additional functions

    module _ {A : Set a} {B : Set b} where

      isInj₁ : A ⊎ B → Maybe A
      isInj₁ (inj₁ x) = just x
      isInj₁ (inj₂ y) = nothing

      isInj₂ : A ⊎ B → Maybe B
      isInj₂ (inj₁ x) = nothing
      isInj₂ (inj₂ y) = just y

      From-inj₁ : A ⊎ B → Set a
      From-inj₁ (inj₁ _) = A
      From-inj₁ (inj₂ _) = ⊤

      from-inj₁ : (x : A ⊎ B) → From-inj₁ x
      from-inj₁ (inj₁ x) = x
      from-inj₁ (inj₂ _) = _

      From-inj₂ : A ⊎ B → Set b
      From-inj₂ (inj₁ _) = ⊤
      From-inj₂ (inj₂ _) = B

      from-inj₂ : (x : A ⊎ B) → From-inj₂ x
      from-inj₂ (inj₁ _) = _
      from-inj₂ (inj₂ x) = x

    ------------------------------------------------------------------------
    -- DEPRECATED NAMES
    ------------------------------------------------------------------------
    -- Please use the new names as continuing support for the old names is
    -- not guaranteed.

    -- Version 2.1

    open Dec public using (fromDec; toDec)