    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- An either-or-both data type, basic type and operations
    ------------------------------------------------------------------------

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

    module Data.These.Base where

    open import Level using (Level; _⊔_)
    open import Data.Sum.Base using (_⊎_; [_,_]′)
    open import Function.Base using (id; flip)

    private
      variable
        a b c d e f : Level
        A : Set a
        B : Set b
        C : Set c
        D : Set d
        E : Set e
        F : Set f

    data These {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
      this  : A     → These A B
      that  :     B → These A B
      these : A → B → These A B

    ------------------------------------------------------------------------
    -- Operations

    -- injection

    fromSum : A ⊎ B → These A B
    fromSum = [ this , that ]′

    -- map

    map : (f : A → B) (g : C → D) → These A C → These B D
    map f g (this a)    = this (f a)
    map f g (that b)    = that (g b)
    map f g (these a b) = these (f a) (g b)

    map₁ : (f : A → B) → These A C → These B C
    map₁ f = map f id

    map₂ : (g : B → C) → These A B → These A C
    map₂ = map id

    -- fold

    fold : (A → C) → (B → C) → (A → B → C) → These A B → C
    fold l r lr (this a)    = l a
    fold l r lr (that b)    = r b
    fold l r lr (these a b) = lr a b

    foldWithDefaults : A → B → (A → B → C) → These A B → C
    foldWithDefaults a b lr = fold (flip lr b) (lr a) lr

    -- swap

    swap : These A B → These B A
    swap = fold that this (flip these)

    -- align

    alignWith : (These A C → E) → (These B D → F) → These A B → These C D → These E F
    alignWith f g (this a)    (this c)    = this (f (these a c))
    alignWith f g (this a)    (that d)    = these (f (this a)) (g (that d))
    alignWith f g (this a)    (these c d) = these (f (these a c)) (g (that d))
    alignWith f g (that b)    (this c)    = these (f (that c)) (g (this b))
    alignWith f g (that b)    (that d)    = that (g (these b d))
    alignWith f g (that b)    (these c d) = these (f (that c)) (g (these b d))
    alignWith f g (these a b) (this c)    = these (f (these a c)) (g (this b))
    alignWith f g (these a b) (that d)    = these (f (this a)) (g (these b d))
    alignWith f g (these a b) (these c d) = these (f (these a c)) (g (these b d))

    align : These A B → These C D → These (These A C) (These B D)
    align = alignWith id id