- MathNotebook
- MathConcepts
- StudyMath
- Geometry
- Logic
- Bott periodicity
- CategoryTheory
- FieldWithOneElement
- MathDiscovery
- Math Connections
Epistemology - m a t h 4 w i s d o m - g m a i l
- +370 607 27 665
*My work is in the Public Domain for all to share freely.*
- 读物 书 影片 维基百科
Introduction E9F5FC Questions FFFFC0 Software |
See: Krasauskas Kulikauskas, Univalence Axiom
同伦类型论 . . . Homotopy type theory - Study the kinds of equivalences. Associate them to the relationship between level and metalevel.
- Relate spectral sequences, exact sequences and divisions of everything.
- Understand what homotopy type theory has to say about the homotopy groups of spheres and thus Bott periodicity.
- What is the relationship between loops - identity paths in Homotopy Type Theory - and strings in string theory?
HOTTest Summer School Calendar Rijke. Introduction to Homotopy Type Theory. - 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.
书 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 维基百科 读物 - 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.
游戏 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 |

This page was last changed on September 08, 2023, at 10:18 AM