Differences

This shows you the differences between two versions of the page.

--- drawing_arrows_and_coding_functions [2016/09/21 16:52]
nikolaj
+++ drawing_arrows_and_coding_functions [2016/10/15 14:42]
nikolaj
@@ Line 2: / Line 2: @@
 | [[Outline]] $\blacktriangleright$ Drawing arrows and coding functions $\blacktriangleright$ [[A type system as a model for some concepts]] |
 ==== Guide ====
-== What will eventually be used here ==
+=== Type system ===
+A main part of a type system is a collection of names that stand for so called types. We will draw a lot of simple pictures with those types "lying around".
-Four languages:
+>do int and maybe string
-- proper cat'ish drawing
+== Intuitive introductory example ==
-$$
-\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
-=== Intuitive introductory example ===
 Here some type judgements and also some drawings.
 == The type Type ==
 We draw graph pictures that display parts of our type system.
+>Make a more elaborate picture with a circle and some element, and an outer circle for Type.
+>Later, draw a similar picture wiht a function (+ element wise maps of it)
+>
 E.g. the type of integers are part of our system and may we draw the vertex
 $$