Disjoint Union of Two Types

a  A

b  B

inl(a) and inr(b) are sometimes called the left- and right-injections of a and b.

InjCase(x; u. e(u); v. f(v))

is the destructor for left- and right-injections.

InjCase(inl(a); u. e(u); v. f(v)) * e(a)
InjCase(inr(b); u. e(u); v. f(v)) * f(b)

Thm* z:A+B. z = InjCase(z; u. inl(u); v. inr(v))

Some commonly used specializations of InjCase(x; u. e(u); v. f(v)) are:

Def isl(x) == InjCase(x; y. true; z. false)
Def outl(x) == InjCase(x; y. y; z. "???")
Def outr(x) == InjCase(x; y. "???"; z. z)

Thm* A,B:Type, x:A+B. isl(x)  
Thm* A,B:Type, x:A+B. isl(x)  outl(x)  A
Thm* A,B:Type, x:A+B. isl(x)  outr(x)  B

outl(inl(a)) * a
outr(inr(b)) * b

A+A is essentially the type A with a bit added.

We treat A+B, inl(a), inr(b), and InjCase(x; u. e(u); v. f(v)) as primitives, but we could instead have defined them using the pairing operation to add a tag:

Let A+B be isleft:if isleft A else B fi.

Let inl(a) be <true,a>.

Let inr(b) be <false,b>.

Let InjCase(x; u. e(u); v. f(v)) be

x/isleft,z. if isleft e(z) else f(z) fi.

(By we mean a two-element Boolean type.)

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html