{-# OPTIONS --cubical-compatible --safe #-}
open import Equality
module Sum {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where
open Derived-definitions-and-properties eq
open import Prelude
private
variable
a : Level
A B C D : Type a
x y : A
f f₁ f₂ g g₁ g₂ : A → B
⊎-map-id : ⊎-map id id x ≡ x
⊎-map-id {x = inj₁ _} = refl _
⊎-map-id {x = inj₂ _} = refl _
⊎-map-∘ :
∀ x → ⊎-map (f₁ ∘ g₁) (f₂ ∘ g₂) x ≡ ⊎-map f₁ f₂ (⊎-map g₁ g₂ x)
⊎-map-∘ = [ (λ _ → refl _) , (λ _ → refl _) ]
dec-¬ : Dec A → Dec (¬ A)
dec-¬ (yes p) = no (_$ p)
dec-¬ (no p) = yes p
if-⊎-map-then-else :
∀ b →
if ⊎-map f g b then x else y ≡ if b then x else y
if-⊎-map-then-else (yes _) = refl _
if-⊎-map-then-else (no _) = refl _
if-then-else-commutes :
(f : C → D) (b : A ⊎ B) →
f (if b then x else y) ≡ if b then f x else f y
if-then-else-commutes _ (yes _) = refl _
if-then-else-commutes _ (no _) = refl _