A.2.6 Coproduct types

{mathparpagebreakable}\inferrule

*[right= $+$ -form] Γ ⊢A : $\mathcal{U}$ _i
Γ ⊢B : $\mathcal{U}$ _i Γ ⊢A+B : $\mathcal{U}$ _i
\inferrule*[right= $+$ -intro ${}_{1}$ ] Γ ⊢A : $\mathcal{U}$ _i
Γ ⊢B : $\mathcal{U}$ _i

Γ ⊢a : A Γ ⊢ ${\mathsf{inl}}$ (a) : A+B \inferrule*[right= $+$ -intro ${}_{2}$ ] Γ ⊢A : $\mathcal{U}$ _i
Γ ⊢B : $\mathcal{U}$ _i

Γ ⊢b : B Γ ⊢ ${\mathsf{inr}}$ (b) : A+B
\inferrule*[right= $+$ -elim] Γ,z : (A+B) ⊢C : $\mathcal{U}$ _i

Γ,x : A ⊢c : C[ ${\mathsf{inl}}$ (x)/z]
Γ,y : B ⊢d : C[ ${\mathsf{inr}}$ (y)/z]

Γ ⊢e : A+B Γ ⊢ind_A+B(z.C,x.c,y.d,e) : C[e/z] \inferrule*[right= $+$ -comp ${}_{1}$ ] Γ,z : (A+B) ⊢C : $\mathcal{U}$ _i
Γ,x : A ⊢c : C[ ${\mathsf{inl}}$ (x)/z]
Γ,y : B ⊢d : C[ ${\mathsf{inr}}$ (y)/z]

Γ ⊢a : A Γ ⊢ind_A+B(z.C,x.c,y.d, ${\mathsf{inl}}$ (a)) ≡c[a/x] : C[ ${\mathsf{inl}}$ (a)/z] \inferrule*[right= $+$ -comp ${}_{2}$ ] Γ,z : (A+B) ⊢C : $\mathcal{U}$ _i
Γ,x : A ⊢c : C[ ${\mathsf{inl}}$ (x)/z]
Γ,y : B ⊢d : C[ ${\mathsf{inr}}$ (y)/z]

Γ ⊢b : B Γ ⊢ind_A+B(z.C,x.c,y.d, ${\mathsf{inr}}$ (b)) ≡d[b/y] : C[ ${\mathsf{inr}}$ (b)/z] In $\mathsf{ind}_{A+B}$ , $z$ is bound in $C$ , $x$ is bound in $c$ , and $y$ is bound in $d$ .

Title	A.2.6 Coproduct types
\metatable