Four languages:

- proper cat'ish drawing

$$ \require{AMScd} \begin{CD} {\large\hbar} @>{\large{!}}>> {\large{*}} \\ @V{{\large{m}}}VV @VV{{\large\top}}V \\ {\large\heartsuit} @>>{\large{\chi}}> {\large{\Omega}} \end{CD} $$

- drawing where you see terms, circled (the type universe is circled as well)

- typey syntax

- FOL/SOL

Here some type judgements and also some drawings.

We draw graph pictures that display parts of our type system. E.g. the type of integers are part of our system and may we draw the vertex $$ {\mathbb Z} $$

i : Integer
i = 13
 
k : Integer
k = 4
 
n : Integer
n = 2 + 3
 
m : Integer
m = -70 + n

$13 : {\mathbb Z}$

$4 : {\mathbb Z}$

$k:=4$

$k : {\mathbb Z}$

$(2+3) : {\mathbb Z}$

$n:=2+3$

$n : {\mathbb Z}$

fun : Integer -> Integer
fun x = x + m
 
g : Integer -> Integer
g x = -x + k
 
h : Integer -> Integer
h x = 100 + fun x

$g : {\mathbb Z}\to{\mathbb Z}$

The function $g$ is one of an unending list of possible functions from ${\mathbb Z}$ to ${\mathbb Z}$ that we can define. Draw $$ {\mathbb Z}\longrightarrow{\mathbb Z} $$ or $$ \require{AMScd} \begin{CD} {\mathbb Z} \\ @V{{}}VV \\ {\mathbb Z} \end{CD} $$ and then

$({\mathbb Z}\to{\mathbb Z}) : {\rm Type}$

F : (Integer -> Integer) -> Integer
F f = 5000 + f k

Draw $$ ({\mathbb Z}\to{\mathbb Z})\longrightarrow{\mathbb Z} $$ or $$ \require{AMScd} \begin{CD} ({\mathbb Z}\to{\mathbb Z}) \\ @V{{}}VV \\ {\mathbb Z} \end{CD} $$ and then

$(({\mathbb Z}\to{\mathbb Z})\to{\mathbb Z}) : {\rm Type}$

Actualy, in this system we have

${\rm Type}:{\rm Type}$

and we so may draw $$ {\rm Type} $$ and write

${\mathbb Z}:{\rm Type}$

Idris syntax

Outline