A.2.6 Coproduct types


{mathparpagebreakable}\inferrule

*[right=+-form] Γ âŠĒA : 𝒰 _i
Γ âŠĒB : 𝒰 _i Γ âŠĒA+B : 𝒰 _i
\inferrule*[right=+-intro1] Γ âŠĒA : 𝒰 _i
Γ âŠĒB : 𝒰 _i

Γ âŠĒa : A Γ âŠĒ𝗂𝗇𝗅 (a) : A+B \inferrule*[right=+-intro2] Γ âŠĒA : 𝒰 _i
Γ âŠĒB : 𝒰 _i

Γ âŠĒb : B Γ âŠĒ𝗂𝗇𝗋 (b) : A+B
\inferrule*[right=+-elim] Γ,z : (A+B) âŠĒC : 𝒰 _i

Γ,x : A âŠĒc : C[𝗂𝗇𝗅 (x)/z]
Γ,y : B âŠĒd : C[𝗂𝗇𝗋 (y)/z]

Γ âŠĒe : A+B Γ âŠĒind_A+B(z.C,x.c,y.d,e) : C[e/z] \inferrule*[right=+-comp1] Γ,z : (A+B) âŠĒC : 𝒰 _i
Γ,x : A âŠĒc : C[𝗂𝗇𝗅 (x)/z]
Γ,y : B âŠĒd : C[𝗂𝗇𝗋 (y)/z]

Γ âŠĒa : A Γ âŠĒind_A+B(z.C,x.c,y.d,𝗂𝗇𝗅 (a)) ≡c[a/x] : C[𝗂𝗇𝗅 (a)/z] \inferrule*[right=+-comp2] Γ,z : (A+B) âŠĒC : 𝒰 _i
Γ,x : A âŠĒc : C[𝗂𝗇𝗅 (x)/z]
Γ,y : B âŠĒd : C[𝗂𝗇𝗋 (y)/z]

Γ âŠĒb : B Γ âŠĒind_A+B(z.C,x.c,y.d,𝗂𝗇𝗋 (b)) ≡d[b/y] : C[𝗂𝗇𝗋 (b)/z] In ð—‚ð—‡ð–―A+B, z is bound in C, x is bound in c, and y is bound in d.

Title A.2.6 CoproductMathworldPlanetmath types
\metatable