def0 Tag : ★₀ = {left, right};

def0 Payload : 0.(A : ★₀) → 0(B : .★₀) → 1.Tag → ★₀ =
  λ A B tag ⇒ case1 tag return ★₀ of { 'left ⇒ A; 'right ⇒ B };

def0 Either : 0.★₀ → 0.★₀ → ★₀ =
  λ A B ⇒ (tag : Tag) × Payload A B tag;

defω Left : 0.(A : ★₀) → 0.(B : ★₀) → 1.A → Either A B =
  λ A B x ⇒ ('left, x);

defω Right : 0.(A : ★₀) → 0.(B : ★₀) → 1.B → Either A B =
  λ A B x ⇒ ('right, x);

defω either-elim :
    0.(A : ★₀) → 0.(B : ★₀) →
    0.(P : 0.(Either A B) → ★₀) →
    ω.(1.(x : A) → P (Left  A B x)) →
    ω.(1.(x : B) → P (Right A B x)) →
    1.(x : Either A B) → P x =
  λ A B P f g x ⇒
    case1 x return x' ⇒ P x' of {
      (tag, value) ⇒
        (case1 tag
         return tag' ⇒
           0.(eq : (tag ≡ tag' : Tag)) →
           P (tag, coerce [i ⇒ Payload A B (eq i)] @0 @1 value)
         of {
           'left  ⇒ λ eq ⇒ f value;
           'right ⇒ λ eq ⇒ g value
         }) (δ _ ⇒ tag)
    };