------------------------------------------------------------------------
-- 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."
#-}