===== Foundational temp1 =====
| [[Drawing arrows and coding functions]] $\succ$ Foundational temp1 $\succ$ [[Foundational temp1b]] |
==== Guide ====

(Note) [[Logic]]

(Note) [[Specifying syntax]]

>**Remark**: With the Framework entries, I go up in complexity. Then, with the entries with mathematical content, I start with abstract and go to concrete.

(Framework) [[Intuitionistic propositional logic]]

(Note) [[Predicate logic]]

-----

(Note) [[First-order theory of groups]]

>todo

(Framework) [[First-order Peano arithmetic]]

>todo

-----

(Framework) [[Set theory]]

Explanation of axiomatics, in particular ZFC and also the Grothendieck-Tarski axiom (a large cardinal axiom).

Discussion of basic concepts such as the [[Unordered pair]].

-----

(Framework) [[Category theory]]

>**Todo**: 
>Split [[Category theory]] in two. I.e. make a (Framework) entry on Category theory, axiomized directly in logic and another (Note) entry for Category theory within type theory.

-----

(Note) [[Type theory]]

>todo

(Type) [[Type]]

(Type) [[Function type]]

(Type) [[Product type]]

>**Todo**: Introduce in a chain of entries more and more expressible type theories. The guideline being that each entry is a "faithful subset" of the next.

-----
=== Sequel of ===
[[Drawing arrows and coding functions]]