------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of sums (disjoint unions) ------------------------------------------------------------------------ module Data.Sum.Properties where open import Data.Sum open import Function open import Relation.Binary.PropositionalEquality module _ {a b} {A : Set a} {B : Set b} where 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 swap-involutive : swap {A = A} {B} ∘ swap ≗ id swap-involutive = [ (λ _ → refl) , (λ _ → refl) ]