Introduction E9F5FC

Questions FFFFC0

• View
• Edit
• History
• Print

同伦类型论 . . . Homotopy type theory

HOTTest Summer School Calendar

Rijke. Introduction to Homotopy Type Theory.

• 2019 Summer School Book

HOTTest Summer School, Videos

• Lecture 1 Structure of dependent type theory. Dependent function types, rules for {$\Pi$} types. Rijke 1-2.
• Lecture 2 Inductive types. Rijke 3-4.
• Lecture 3 Identity type. Rijke 5.
• Lecture 4 Universes. Rijke 6. Propositions as types, Curry-Howard interpretation. Rijke 7.
• Lecture 5 Equivalences: Homotopies. Equivalences as bi-invertible maps. Identifications in Sigma-types. Preview of functionality and univalence. Rijke 7.

Worksheet 1

书

Textbooks on logic and type theory

• Logic and Proof
• Girard. Proofs and Types
• Bengt Nordström, Kent Petersson, Jan M. Smith. Programming in Martin-Löf's Type Theory: An Introduction.

Course books

• Homotopy type theory book
• Robert Harper. Homotopy Type Theory Lecture Notes

维基百科

Type theory

• Dependent type (and dependent function)
• Simply typed lambda calculus
• Intuitionistic type theory

Homotopy type theory

• Homotopy

读物

• Krysztof Kapulkin, Peter Lefanu Lumsdaine. The Simplicial Model of Univalent Foundations (After Voevodsky).
• Univalence axiom at nLab
• What is the univalence axiom?
• The Homotopy Hypothesis John Baez
• Talks by Thierry Coquand
  • Univalent Foundation and Constructive Mathematics and Part 2
  • Leeds tutorial, Part 2 and 3
• Homotopy Type Theory and Voevodsky's Univalent Foundations, Alvaro Pelayo, Michael A. Warren
• Homotopy Type Theory: Book

影片

• An Intuitive Introduction to Motivic Homotopy Theory Vladimir Voevodsky [2002]
• V: George Shabat. Galois, Grothendieck and Voevodsky.

游戏

• The HoTT Game

Community

• Vilniaus universitetas. Linas Laibinis domisi Voevodskiu ir t.t.

Concepts:

• Different levels of equivalences
• Paths between points (homotopies) and equivalence of homotopies

Adjoints

• In Shulman, how are dependent sum and dependent product adjoints?
• In Shulman, see discussion of space and adjoint string and local topos.

笔记

• John C. Baez. The Homotopy Hypothesis.
• Egbert Rijke. Introduction to Homotopy Type Theory.
• Substitution for variables - binding and scope
• Types are specifications are programs
• Communicating by algorithm and certain shared assumptions. Discover those assumptions.
• Term M (program - that when it runs) in type A (program - it runs the way A says it runs)
• Naturality in homotopy type theory breaks down when we try to do type theory in type theory.
• https://mathoverflow.net/questions/118857/forcing-in-homotopy-type-theory
• Shulman. Homotopy type theory: The logic of space.
• Compare parametrization t and (1-t) in definitions of homotopy and in definition of simplexes in R^n.

https://github.com/FrozenWinters/stlc SLTC project where Astra formalises the categorical semantics of function types in Agda.

Induction argument on truncation levels uses the level below (for identities) and the level above (which we're trying to reach). Similarly, the recurrence relation relates the level xP_n(x) with the level below and the level above.

An empty type has no evidence for it, is not true. A nonempty type, as a proposition, is true. The notion of empty or nonempty is relevant for the sevensome, for describing {$\forall \wedge \exists$}.

Every type has a unique name. Every universe is a type with a unique name. Every term in a type should have a unique name. So why can't we have a universe of unique names for all of the terms, types and universes? And if we can, then don't we run into a paradox? Or not?

• Types indicate comparability which is a condition for equality.

https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory

For different type theories we can construct different categorical models.

• What is the common requirements for the additional structures to be valid semantic models of a type theory?

observational (a posteriori) and definitional (a priori) judgments as in type theory