------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of sums (disjoint unions) ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Data.Sum.Properties where open import Level open import Data.Sum.Base open import Function open import Relation.Binary using (Decidable) open import Relation.Binary.PropositionalEquality open import Relation.Nullary using (yes; no) open import Relation.Nullary.Decidable using (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₁ : Decidable {A = A} {B = A} _≡_) (dec₂ : Decidable {A = B} {B = B} _≡_) where ≡-dec : Decidable {A = 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) ] map-id : map {A = A} {B = B} id id id map-id (inj₁ _) = refl map-id (inj₂ _) = refl [,]-∘-distr : (f : A B) {g : C A} {h : D A} f [ g , h ] [ f g , f h ] [,]-∘-distr _ (inj₁ _) = refl [,]-∘-distr _ (inj₂ _) = refl [,]-map-commute : {f : A B} {g : C D} {f′ : B E} {g′ : D E} [ f′ , g′ ] map f g [ f′ f , g′ g ] [,]-map-commute (inj₁ _) = refl [,]-map-commute (inj₂ _) = refl map-commute : {f : A B} {g : C D} {f′ : B E} {g′ : D F} map f′ g′ map f g map (f′ f) (g′ g) map-commute (inj₁ _) = refl map-commute (inj₂ _) = refl map₁₂-commute : {f : A B} {g : C D} map₁ f map₂ g map₂ g map₁ f map₁₂-commute (inj₁ _) = refl map₁₂-commute (inj₂ _) = 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′)