===== Outline =====
| [[An apple pie from scratch]] $\succ$ Outline  $\succ$ [[Drawing arrows and coding functions]] |
==== Guide ====
Here is an outline structure (work in progress):

=== Concepts in the incarnation of a programming language ===
  * Assume knowledge of integers $-2,-1,0,1,2,3$ with binary operations $+,-,*$. 
  * More on that languages syntax and examples (which are instances of relevant concepts to be discussed later)
=== Computation and logic (presented bottom-up) ===
  * Comment on syntax
  * Type theories: Simple type theory $\to$ Polymorphic type theory $\to$ Dependent type theory
  * Formal logic: Intuitionist logic $\to$ First order logic (here, at the latest, it might be good to introduce the non-computing language, i.e. go away from the programming language and use a formal logic, as is traditional, in a descriptive fashion)
  * Comment on curry-Howard correspondence
  * Axiomatization of category theory within dependent type theory, plus comment on first order axiomatization
  * Axiomatization of set theory within first order logic
  * Informal discussion of the very first constructions in those frameworks, respectively
  * Comment on how cats and set can be used to study type theory and logic itself
  * 
=== Mathematical core (presented top-down) ===
  * Formal definitions from the main body of this wiki. The **Set** entries can be thought of as defining sets which ZFC shows to be non-empty. Some category theoretical definitions use sets (e.g. when setting up a category of sets, for which we wanted to add a large cardinal axiom), but conversely the set entries are independent of those (but of course a notion of categories can and is defined within ZFC). 

=== Physics ===

Eventually, make a list of mutually properly distinct physical frameworks - i.e. mathematical theories used in physics, usually coming with some state space and dynamics, see [[Perspective]]. 
In the latter sense, they must be exhaustively specified, 
of course, together with a concise list of their respective axioms. 
Some frameworks contain black boxes that are further given insight into in more detailed theories. 
Here, when it comes to physics, I tend to like to have the rougher theories first.

| 'that list' |

Now one can reference real life systems and associate mathematical models in this and that framework with them.
Develop them like this:

| mechanics |

>todo: examples of experiments

| ... phenomenological thermodynamics |

>todo: examples of experiments

(Phenomenological thermodynamics leads to a lot of basic chemistry)

| electronics |

>todo: examples of experiments

| electromagnetic field theory |

-----

==== Entries ====
^ Preface ^
| [[An apple pie from scratch]] |
| [[Guideline]] |
| [[Outline]] (this entry) |

**Logical prerequisites**
^ Meta ^
| [[On syntax]] |
| Symbols |
^ Types, terms and programming ^
| up to dependent type theory (?MLTT, etc.) |
| type of natural numbers |
| type of categories |
| informal Curry-Howard correspondence |
| [[Foundational temp1]] |
^ Formal logic ^
| Intuitionistic logic (independent of type theory) |
| First order logic (i.e. adding LEM to Intuitionistic logic) |
| Axioms for set theory (e.g. GT-set-theory, and then U= type of sets) |

**Mathematical core**

>todo: the following line of "apple pie from scratch" entries have some gaps
>
>I have neither been able to find a good n-category basis instead of the 1-category approach I take here
>nor have I formalized "up to iso" anywhere (this point is relate to the one above)

^ **Formal part** ^
| [[On category theory basics]] |
| [[On universal morphisms]] |
| [[Foundational temp3]] |
| [[Foundational temp4]] |
| ... |

| ... mathematics of statistical physics |
| [[On universal morphisms]] |

=== References ===

-----
=== Sequel of ===
[[An apple pie from scratch]]
=== Related ===
[[An apple pie from scratch]]