[Agda] Yet another questions about equality

[Permjacov Evgeniy]

1) Let assume

infixr 1 _⊎_

data _⊎_ {ℓ₁ ℓ₂} (A : Set ℓ₁) (B : Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

sum : ∀ {ℓ₁ ℓ₂ ℓ₃} {A : Set ℓ₁} {B : Set ℓ₂} {R : A ⊎ B → Set ℓ₃ }
    → ( (x : A) → R (inj₁ x) )
    → ( (y : B) → R (inj₂ y) )
    → (x : A ⊎ B ) → R x
sum c₁ c₂ (inj₁ l) = c₁ l
sum c₁ c₂ (inj₂ r) = c₂ r


how to prove
  sum inj₁ inj₂  ≡ id ?

2) is it possible to prove 
  ∀ {ℓ : Level} {A B : Set ℓ} {f g : A → B} → (∀ (a : A) → f a ≡ g a) →
f ≡ g