A.1.4 Coproduct types

We introduce primitive constants c+, c𝗂𝗇𝗅, and c𝗂𝗇𝗋. We write A+B instead of c+(A,B), 𝗂𝗇𝗅(a) instead of c𝗂𝗇𝗅(a), and 𝗂𝗇𝗋(a) instead of c𝗂𝗇𝗋(a):

  • if A,B:𝒰n then A+B:𝒰n

  • moreover, 𝗂𝗇𝗅:AA+B and 𝗂𝗇𝗋:BA+B

If we have A and B as above, C:A+B𝒰m, d:(x:A)C(𝗂𝗇𝗅(x)), and e:(y:B)C(𝗂𝗇𝗋(y)), then we can introduce a defined constant f:(z:A+B)C(z) with the defining equations

f(𝗂𝗇𝗅(x)):d(x)  and  f(𝗂𝗇𝗋(y)):e(y).
Title A.1.4 CoproductMathworldPlanetmath types