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).
Best Answer
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$.