HoTT Without Vars

There are a few notational conveniences of the lambda calculus that seem to be missing in the HoTT calculus. Here are some ideas about how to add them.  First, a kind of "reverse lambda" operator that allows us to refer to arbitrary elements of a type without using a name, just like lambda does with functions.  Second, an explicit type former for enumerated types, that allows us to express such types without using a name.  Lastly, a pipeline application operator that allows us to string expressions together.

A PDF version of this article is at HoTT Without Vars.  This is revision 2.

Type Specialization

The type formers of HoTT (×, →, Π, Σ and the rest) are very similar to the lambda operator λ. Just as λ turns an open formula into the name of the associated function (λx.x + 1 names the function associated with x + 1), the type formers turn expressions into the names of types. For example, × turns A, B into the type name A × B; → turns A, B into the type name A → B, and so forth.

Lambda expressions like λx.x + 1 are called lambda abstractions; by extension, we can call type formation expressions type abstractions. To “undo” a lambda abstraction, we use application: λx.x + 1(2) = 3. Since the opposite of abstraction is specialization, it is tempting to think of application as specialization; but application involves more than mere specialization. If we think of a function (that is, a lambda abstraction) as a set of ordered pairs, then its specialization should be a particular ordered pair; but application does not deliver a pair, it projects the second element of a pair. So application can be thought of as a combination of specialization and projection.

Lambda abstractions are treated not only as the names of functions, but as function definitions. That’s what allows us to write, e.g. f = λx.x + 1.

There is no application operator for type abstractions. We cannot undo A → B by writing (A → B)(x), for example. But we can specialize type abstractions; that is just what expressions like a : A do. One (classical) way to interpret such an expression is to say that a denotes an “element” of A. Such an interpretation presupposes a denotational semantics and thus implicates a notion of choice; a more detailed gloss might say that “:” chooses an element of A and assigns it to a. Under a pragmatic interpretation that eschews denotational semantics, we might simply stipulate that a : A means that a is a token of type A and leave it at that. Either way, we have introduced a variable, a, in the service of specializing a type abstraction.

Now one of the great advantages of the lambda notation is that it allows us to dispense with function names. In fact this notational convenience was Church’s original motivation in introducing λ; he did not realize until later that it formed the basis of a powerful computation/logical calculus. Without the lambda operator we would have to define and name every function we need to use, so that we can later refer to it by name. With the lambda calculus we can just write out the function definition wherever we need it.

In principle we should be able to do the same thing – that is, dispense with intermediate names – for type abstractions and specializations. But the HoTT notation does not currently support this; if you want to work with an arbitrary element of a type, you must name it using the “:” operator.  And enumerated types (e.g. the boolean type) cannot be specified without naming.

To address this notational deficiency we propose a specialization operator for type abstractions, ƛ (this is U+019B, lambda with stroke; in latex, I use reversed lambda). Its meaning is exactly analogous to the lambda operator, but instead of abstracting it specializes.  λ turns a particular formula into an abstraction; ƛ turns a type abstraction into a particular. Under a classical interpretation, the operator “selects” an element of the type to which it is applied; under a pragmatic interpretation, the combination of the operator symbol and a type symbol is a symbol of that type.

1)	f :A→B	f names an arbitrary function of type A→B
2)	ƛA → B	ƛA→B : A→B
3)	ƛN	an arbitrary natural number

The usefulness of this becomes more evident with Π and Σ types. From the definition of path induction, p. 49:

4)	\(C:Π_{(x,y:A)}(x=_Ay)→U\)	same as: \(C :\equiv ƛ \bigg(Π_{(x,y:A)} ƛ\big( (x=_Ay)\to\mathcal{U}\big)\bigg)\)
5)	\(c:Π_{(x:A)}C(x,x,refl_x)\)	same as: \(c :\equiv ƛ \bigg(Π_{(x:A)} ƛ\ C(x,x,refl_x)\bigg)\)

These may be rewritten as follows using the pipeline application operator “|” described below; briefly, x|f = f (x) :

6)	\(c:≡ƛ\Pi_{(x:A)}\bigg(\ x\to\Sigma_{(x,x:A)}(x=_Ax)\ \bigg\rvert\ ƛ\Pi_{(x,y:A)}(x= y)→U\bigg)\)	incorrect
6a)	\(c:≡ƛ\Pi_{(x:A)}\ x\toƛ\bigg(ƛ\Sigma_{(x,x:A)}(x=_Ax)\ \bigg\rvert\ ƛ\Pi_{(x,y:A)}(x= y)→U\bigg)\)	correct?
7)	\(c:≡ƛ\Pi_{(x:A)}\bigg(\ x\to\Sigma_{(x:A)}\Big(\Sigma_{(x:A)}(x=_Ax)\Big)\ \bigg\rvert\ ƛ\Pi_{(x,y:A)}(x= y)→U\bigg)\)	incorrect
7a)	\(c:≡ƛ\Pi_{(x:A)}\ x\to\ ƛ\bigg(ƛ\Sigma_{(x:A)}\Big(\Sigma_{(x:A)}(x=_Ax)\Big)\ \bigg\rvert\ ƛ\Pi_{(x,y:A)}(x= y)→U\bigg)\)	correct?

These are equivalent (I think); (7) is just more explicit than (6). They are slightly different than (4) and (5) in that they do not use \(refl_x\). In both cases, the entire meaning can be read off the one expression, just as in the case of a lambda definition; it can be glossed in order: c is an element of a function type that takes any x : A, produces a dependent triple of the form (x, x, p), where p is any proof that x = x, and feeds that into a function that maps such triples to a new type.

This notation seems to make it possible to render structure more explicitly; whether or not this is a better way to write this is beside the point; the λ operator at least makes it possible.

(Of course, the symbol is arbitrary but motivated - it’s a reverse lambda. We may find a better symbol than this; e.g. upside down lambda: or the like).

Caveat: You cannot just replace named elements with λ expressions willy-nilly, since the latter pick out arbitrary elements. Where a name occurs multiple times in a context it must mean the same thing each time; e.g. in the formula for \(ind=_A\) on p. 49. (reproduced below).

Definitions:  Implicit v. Explicit 

A specialization like a : A says that a is an arbitrary token of type A. But arbitrary does not mean indefinite; if we adopt the classical perspective and treat a : A as meaning that a denotes an arbitrary element of A we have not said that a is undefined. On the contrary, if it is to denote at all, it must denote something definite. So we might say that a denotes a definite but unknown element of A. Since it is defi- nite, we can say that a is implicitly defined. If we then offer a “defining equation” for a, it becomes explicitly defined.

In other words, typing judgments of the form a : A implicitly define their token component.

The difference is clear in the case of function types:

8)	f:N→N
9)	f :≡λx:N.x+1

Expression (8) implicitly defines f by giving its type explicitly and “judging” that f has that type; that is, by assigning f to a specialization of its type. Expression (9) then makes that definition explicit.

Since the term “definition” thus has two meanings, we will generally use the term “specification” and leave it to the reader to determine from context which kind of definition is involved. For example, we might say “Given the specification a : A”, meaning that a : A specifies that a names an implicitly defined element of A.

An Explicit Operator for Enumerated Types

Enumerated types like 2 do not have an explicit abstraction operator. We propose Λ. This allows us to specify “anonymous” enumerated types, e.g.

Λ{Mon, Tues, Wed, Thu, Fri, Sat, Sun}

names a “Day” type without naming it. To name it we can write:

Day :≡ Λ{Mon, Tues, Wed, Thu, Fri, Sat, Sun}

Pipeline Application

10)	\(ƛ\Sigma_{(x,y:A)}(x=_A y)\ \Big\rvert\ ƛ\Pi_{(x,y:A)}(x=_Ay)→U\)

meaning, apply an element of the Π type to an element of the Σ type, or feed the latter into the former. In this case we can safely omit the specialization operators since they can be inferred from the context:

11)	\(\Sigma_{(x,y:A)}(x=_Ay)\ \Big\rvert\ \Pi_{(x,y:A)}(x=_Ay)→U\)

Using names, these two expressions are equivalent to the pair of expressions:

12)	\(C:\Pi_{(x,y:A)}(x=_Ay)→U\)
13)	\(C(a,b,p)\)	where \(a,b:A\) and \(p:(a=_Ab)\)

Universe Operator

For lack of a better term.  The standard way to express a family is B : A → U. This is fine if B and A are relatively simple; B(a) is a type. But if B and/or A are complex this can be awkward. Sometimes we may want a name to refer to members of a type family, if only for expository purposes; e.g. B(a) :≡ P. The prosposal here is that we introduce a new operator that allows us to name an element of U: PU. Read this as “P is an element drawn from U”.

This allows us to say e.g.  B : A → PU

This is to be interpreted as “B takes each element of A to an element of U, which we name P”; it does not mean “B takes each element of A to an element of P”.