概论

数学

发现

Andrius Kulikauskas

  • ms@ms.lt
  • +370 607 27 665
  • My work is in the Public Domain for all to share freely.

用中文

  • 读物 书 影片 维基百科

Software

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

Keisti - Įkelti - Istorija - Spausdinti - Naujausi keitimai -
Search:
Šis puslapis paskutinį kartą keistas September 04, 2021, at 02:49 PM