Logic, Curry-Howard-Lambek, Homotopy type theory, Category theory
Understand type theory in terms of amounts and units.
Understand type theory
- Understand logic, proofs, propositions in terms of type theory.
- When are two types the same?
- Contraction, exchange, etc. are simply conditions that come from expressing sets as lists. What is gained by a list? Integers. Why integers?
Develop my own perspective
- Develop my ideas on answers, amounts, units in terms of type theory.
- Develop my ideas on variables and their manifestations in terms of type theory.
- Understand the equation X=X in terms of ideas of equality from type theory.
- Describe the mathematics of names (terms, symbols, labels).
Readings
Videos
Intuitionistic type theory has 3 finite types:
- type 0 has no terms and means "false"
- type 1 has 1 canonical term and means "true"
- type 2 has 2 terms which are 2 choices
- Type theory defines incomparables and comparables. Like units are combined (internal relations, sets, inner sums). Unlike unites are listed (orders, explicit external relationships, products). Thus this is the distinction between sets and lists. Commutativity and noncommutativity express this in terms of sums. Thus we are ever going back and forth between modes, external and internal, expressed as modes within modes.
- Type is question, and term is answer.
- A type is the precondition for a discussion of equality or inequality.
Equality
Readings
Type theory