    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties of sums (disjoint unions)
    ------------------------------------------------------------------------

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

    module Data.Sum.Properties where

    open import Level using (Level)
    open import Data.Sum.Base using (_⊎_; inj₁; inj₂; swap; [_,_]; map;
      map₁; map₂; assocˡ; assocʳ)
    open import Function.Base using (_∋_; _∘_; id)
    open import Function.Bundles using (mk↔ₛ′; _↔_)
    open import Relation.Binary.Definitions using (DecidableEquality)
    open import Relation.Binary.PropositionalEquality.Core
      using (_≡_; _≗_; refl; cong)
    open import Relation.Nullary.Decidable.Core using (yes; no; map′)

    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

    inj₁-injective : ∀ {x y} → (A ⊎ B ∋ inj₁ x) ≡ inj₁ y → x ≡ y
    inj₁-injective refl = refl

    inj₂-injective : ∀ {x y} → (A ⊎ B ∋ inj₂ x) ≡ inj₂ y → x ≡ y
    inj₂-injective refl = refl

    module _ (dec₁ : DecidableEquality A)
             (dec₂ : DecidableEquality B) where

      ≡-dec : DecidableEquality (A ⊎ B)
      ≡-dec (inj₁ x) (inj₁ y) = map′ (cong inj₁) inj₁-injective (dec₁ x y)
      ≡-dec (inj₁ x) (inj₂ y) = no λ()
      ≡-dec (inj₂ x) (inj₁ y) = no λ()
      ≡-dec (inj₂ x) (inj₂ y) = map′ (cong inj₂) inj₂-injective (dec₂ x y)

    swap-involutive : swap {A = A} {B = B} ∘ swap ≗ id
    swap-involutive = [ (λ _ → refl) , (λ _ → refl) ]

    swap-↔ : (A ⊎ B) ↔ (B ⊎ A)
    swap-↔ = mk↔ₛ′ swap swap swap-involutive swap-involutive

    map-id : map {A = A} {B = B} id id ≗ id
    map-id (inj₁ _) = refl
    map-id (inj₂ _) = refl

    [,]-∘ : (f : A → B)
                  {g : C → A} {h : D → A} →
                  f ∘ [ g , h ] ≗ [ f ∘ g , f ∘ h ]
    [,]-∘ _ (inj₁ _) = refl
    [,]-∘ _ (inj₂ _) = refl

    [,]-map : {f : A → B}  {g : C → D}
              {f′ : B → E} {g′ : D → E} →
              [ f′ , g′ ] ∘ map f g ≗ [ f′ ∘ f , g′ ∘ g ]
    [,]-map (inj₁ _) = refl
    [,]-map (inj₂ _) = refl

    map-map : {f : A → B}  {g : C → D}
                  {f′ : B → E} {g′ : D → F} →
                  map f′ g′ ∘ map f g ≗ map (f′ ∘ f) (g′ ∘ g)
    map-map (inj₁ _) = refl
    map-map (inj₂ _) = refl

    map₁₂-map₂₁ : {f : A → B} {g : C → D} →
                    map₁ f ∘ map₂ g ≗ map₂ g ∘ map₁ f
    map₁₂-map₂₁ (inj₁ _) = refl
    map₁₂-map₂₁ (inj₂ _) = refl

    map-assocˡ : (f : A → C) (g : B → D) (h : C → F) →
      map (map f g) h ∘ assocˡ ≗ assocˡ ∘ map f (map g h)
    map-assocˡ _ _ _ (inj₁       x ) = refl
    map-assocˡ _ _ _ (inj₂ (inj₁ y)) = refl
    map-assocˡ _ _ _ (inj₂ (inj₂ z)) = refl

    map-assocʳ : (f : A → C) (g : B → D) (h : C → F) →
      map f (map g h) ∘ assocʳ ≗ assocʳ ∘ map (map f g) h
    map-assocʳ _ _ _ (inj₁ (inj₁ x)) = refl
    map-assocʳ _ _ _ (inj₁ (inj₂ y)) = refl
    map-assocʳ _ _ _ (inj₂       z ) = refl

    [,]-cong : {f f′ : A → B} {g g′ : C → B} →
               f ≗ f′ → g ≗ g′ →
               [ f , g ] ≗ [ f′ , g′ ]
    [,]-cong = [_,_]

    [-,]-cong : {f f′ : A → B} {g : C → B} →
                f ≗ f′ →
                [ f , g ] ≗ [ f′ , g ]
    [-,]-cong = [_, (λ _ → refl) ]

    [,-]-cong : {f : A → B} {g g′ : C → B} →
                g ≗ g′ →
                [ f , g ] ≗ [ f , g′ ]
    [,-]-cong = [ (λ _ → refl) ,_]

    map-cong : {f f′ : A → B} {g g′ : C → D} →
               f ≗ f′ → g ≗ g′ →
               map f g ≗ map f′ g′
    map-cong f≗f′ g≗g′ (inj₁ x) = cong inj₁ (f≗f′ x)
    map-cong f≗f′ g≗g′ (inj₂ x) = cong inj₂ (g≗g′ x)

    map₁-cong : {f f′ : A → B} →
                f ≗ f′ →
                map₁ {B = C} f ≗ map₁ f′
    map₁-cong f≗f′ = [-,]-cong ((cong inj₁) ∘ f≗f′)

    map₂-cong : {g g′ : C → D} →
                g ≗ g′ →
                map₂ {A = A} g ≗ map₂ g′
    map₂-cong g≗g′ = [,-]-cong ((cong inj₂) ∘ g≗g′)

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

    -- Version 2.0

    [,]-∘-distr = [,]-∘
    {-# WARNING_ON_USAGE [,]-∘-distr
    "Warning: [,]-∘-distr was deprecated in v2.0.
    Please use [,]-∘ instead."
    #-}

    [,]-map-commute = [,]-map
    {-# WARNING_ON_USAGE [,]-map-commute
    "Warning: [,]-map-commute was deprecated in v2.0.
    Please use [,]-map instead."
    #-}

    map-commute = map-map
    {-# WARNING_ON_USAGE map-commute
    "Warning: map-commute was deprecated in v2.0.
    Please use map-map instead."
    #-}

    map₁₂-commute = map₁₂-map₂₁
    {-# WARNING_ON_USAGE map₁₂-commute
    "Warning: map₁₂-commute was deprecated in v2.0.
    Please use map₁₂-map₂₁ instead."
    #-}