4
$\begingroup$

So, obviously for a term $t$ of type $T$, I would represent it as:

      T
+-----------+
|           |
|     t     |
|           |
+-----------+

That is a node labeled $T$ parenting another node labeled $t$. I'm wondering though how you can represent $\Pi x:A, B(x)$ in a canonical fashion. MS paint drawings welcome! :)

My attempt and best guess is something like this:

Visualization of a Pi-Type

So that says that $x$ inhabits the Pi-type $(\Pi_{a:A} B(a))$, hopefully. So even the labels can be more complicated than a string, i.e. consist of nodes & arrows themselves. Or is there some better way of doing this? Your go.

Improve this question
$\endgroup$
15
  • 2
    $\begingroup$ You'll have to interpret the notion of contexts here $\endgroup$
    – ice1000 ♦
    Commented Nov 3, 2022 at 20:45
  • 1
    $\begingroup$ A context is the thing you wrote at the left-hand side of a judgment. For instance, in $\Gamma \vdash u : A$, the $\Gamma$ is a context. In a DTT, all terms/types are discussed under a context. $\endgroup$
    – ice1000 ♦
    Commented Nov 3, 2022 at 21:36
  • 1
    $\begingroup$ @ice1000 isn't the whole current diagram making up the context! :) I thought a context was like an ordered-AND list of propositions. In that case empty space is the AND gluing together all the visual expressions inside of it. If it needs to be ordered, but I'm not sure that it does, you could work with the natural left-to-right top-to-bottom ordering of visual elements. $\endgroup$
    – SeekingAMathGeekGirlfriend
    Commented Nov 3, 2022 at 21:46
  • 1
    $\begingroup$ Your project is an interactive, visual proof explorer? Wherever you're going, it looks fun! $\endgroup$
    – user1168
    Commented Nov 5, 2022 at 11:18
  • 1
    $\begingroup$ $n$Lab is a great resource! From your post, I would say you are taking a "bottom up" approach. I always end up "eclectic" and include top down design, which is always revealing. In this case, find an interesting and substantial proof then brainstorm out how diagramming the proof might make some aspects clearer. Try using traditional notation at the leaves, see what you can see. Just a thought. $\endgroup$
    – user1168
    Commented Nov 6, 2022 at 16:47

1 Answer 1

Reset to default
6
$\begingroup$

I addressed some of these questions in my lecture “Spartan Type Theory” (PDF slides) at the UniMath 2017 school in Birmingham. In particular, slide 18 looks like this:

A picture of dependent type

Please look at the slides for further ideas and explanations.

Improve this answer
$\endgroup$
5
  • 1
    $\begingroup$ Thanks! Your timing couldn't be better: I'm about to start my journey toward coming to grips with TT. $\endgroup$
    – user1168
    Commented Nov 4, 2022 at 18:55
  • $\begingroup$ It is an interesting slide presentation, however, this idea seems tangential to what I'm asking, so I cannot select it as the answer. How would you program a computer using these graphs? The visual language I presented is much closer to textual type theory than this and so has the potential for being an actual language one could use. These graphs might be useful in a later version as visualizations for things, but not part of the main language. For example I don't want to make string-diagram based proofs (a couple of those exist as web apps), I would like something more general than that. $\endgroup$
    – SeekingAMathGeekGirlfriend
    Commented Nov 4, 2022 at 22:34
  • 3
    $\begingroup$ There is no indication in your question that you are considering graphical programming in dependent type theory, unless you intended to do so with MS Paint. $\endgroup$
    – Andrej Bauer
    Commented Nov 4, 2022 at 22:38
  • $\begingroup$ I did say that a typed term is represented as an inhabitant of a box node. And my example preserved that requirement, so… you are clearly smarting me 😀 $\endgroup$
    – SeekingAMathGeekGirlfriend
    Commented Nov 5, 2022 at 16:57
  • $\begingroup$ AndrejBauer I'm still absorbing your presentation (a little at a time, like osmosis), but it's given me an excuse to treat myself to a copy of Taschen's (fancy-shmancy) edition of Euclid's Elements. A reprinting of an older attempt to "go graphical" with math, that edition might be (tangentially) relevant to @DanielDonnelly's Q! $\endgroup$
    – user1168
    Commented Nov 10, 2022 at 21:18

Not the answer you're looking for? Browse other questions tagged or ask your own question.