# In Homotopy Type Theory, where does the lambda expression reside?

## Background

I am trying to develop a visual language for doing higher level mathematics. The language is essentially the language of categories with some allowances since this thing runs on a computer.

However, doing things naively, you run into the issue of having to hand / hard code every feature. What is needed is the ability to specify the app framework using the app itself. I've decided on HoTT because it's an active area of research and different from what Coq / Isabelle use out-of-the box.

However, I don't want to re-invent the wheel and have the users enter in proofs in a Coq/Isabelle-like textual language. I'd like them to make use of a visual editor wherever this works out nicely, and go to the text editor whereever else.

So the visual editor diagrams will get converted into the same internal data structure that the textual samples get converted to. Ideally the data structure, the textual spec and the visual spec are all synced. This will mean that a lot of visual elements will become locked, as coding change propagation in the network of the data structure can get really difficult, and at times not really make sense. Therefore you lock certain items from editing.

## Question

Anyway, where would the lambda expression reside in the above diagram? In HoTT in particular everything lies in a space (a type).

I would like a node with the expression shown and arrow to a tree definition of the expression (yes, a visual tree). Since that is how I will operate on the expressions (as trees).

If we name the two boxes up there 'type $A$' and 'type $B$', so that $f:A\to B$, then the third box, where the corresponding lambda expression lives, is $\hom(A, B)$ (meaning internal hom), which in type theory is simply denoted by $A\to B$.
Note that $f$ is of type $A\to B$(rejustifying the notation $f{\bf:}A\to B$) and that it can be rewritten as $\lambda a.f(a)$.
The yellow arrow, marked '=', from $B$ to $A\to B$ should rather (be of other color and) go from the arrow $f$.
• Thank you for the detailed analysis and involving the gui. What's wrong with $A$ instead of type A? – I Said Roll Up n Smoke Adjoint Jul 18 '18 at 22:38
• Is internal hom different from $\text{Hom}(A,B)$ in the category of small types? – I Said Roll Up n Smoke Adjoint Jul 18 '18 at 22:40