    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- An either-or-both data type
    ------------------------------------------------------------------------

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

    module Data.These where

    open import Level
    open import Data.Maybe.Base using (Maybe; just; nothing; maybe′)
    open import Data.Sum.Base using (_⊎_; [_,_]′)
    open import Function.Base using (const; _∘′_; id; constᵣ)

    ------------------------------------------------------------------------
    -- Re-exporting the datatype and its operations

    open import Data.These.Base public

    private
      variable
        a b : Level
        A : Set a
        B : Set b

    ------------------------------------------------------------------------
    -- Additional operations

    -- projections

    fromThis : These A B → Maybe A
    fromThis = fold just (const nothing) (const ∘′ just)

    fromThat : These A B → Maybe B
    fromThat = fold (const nothing) just (const just)

    leftMost : These A A → A
    leftMost = fold id id const

    rightMost : These A A → A
    rightMost = fold id id constᵣ

    mergeThese : (A → A → A) → These A A → A
    mergeThese = fold id id

    -- deletions

    deleteThis : These A B → Maybe (These A B)
    deleteThis = fold (const nothing) (just ∘′ that) (const (just ∘′ that))

    deleteThat : These A B → Maybe (These A B)
    deleteThat = fold (just ∘′ this) (const nothing) (const ∘′ just ∘′ this)