Questions tagged [homotopy-type-theory]
The homotopy interpretation of constructive dependent type theory, the univalence axiom, higher inductive types, internal languages of higher toposes, univalent foundations for mathematics, and implementations of such theories in proof assistants.
19
questions with no upvoted or accepted answers
25
votes
0
answers
4k
views
What's the point of cubical type theory?
I have been following through the development of homotopy type theory since 2013 because I was really interested in the foundation of mathematics. The novel idea of combining programming with homotopy ...
10
votes
0
answers
308
views
Is there a definition of an $\infty$-groupoid in HoTT whose terms are $n$-manifolds and whose higher morphisms are diffeomorphisms/isotopies/etc?
Suppose you want to work with TQFTs in homotopy type theory (HoTT). Working with $(\infty,n)$-categories, or even $(\infty,1)$-categories, is something that I gather is too difficult for HoTT at the ...
7
votes
0
answers
166
views
How does nullification of $K(\mathbb{Z}, 2)$ compare to 1-truncation?
Let $B$ be a type (or space). A type (or space) is $B$-null if the canonical map $X \to X^B$ is an equivalence. The $B$-nullification of an arbitrary type $X$ is a $B$-null type $\bigcirc_B X$ ...
7
votes
0
answers
233
views
New Foundations in a Homotopy/Intuitionistic Type Theory form?
New Foundations is a famously odd set theory suggested by Quine in the 1930s which:
Features a universal set.
Disproves the axiom of choice.
Proves the existence of an infinite set by a trivial ...
6
votes
0
answers
153
views
Inductive type constructors with the defined type appearing in non-strictly positive position
In the HoTT book §5.6 ‘The general syntax of inductive definitions’ there is a proof that the existence of an inductive type $T$ with a constructor $t : ((T \to \mathsf{Prop}) \to \mathsf{Prop}) \to T$...
3
votes
0
answers
141
views
Homotopy type theory for semantics
It looks like I have been building up a theory that might require looking closely at Homotopy Type Theory vs. Category Theory with respect to semantics. I am considering two types of semantics that ...
3
votes
0
answers
66
views
Discreteness of the higher inductive-inductive Cauchy real numbers in real cohesive homotopy type theory
We work in cohesive homotopy type theory with propositional resizing, so that there is only one type of Dedekind real numbers $\mathbb{R}$ up to equivalence, and Mike Shulman's axiom $\mathbb{R}\flat$,...
3
votes
0
answers
265
views
Principle of unique choice in homotopy type theory
In the MathOverflow thread Mathematics without the principle of unique choice, Mike Shulman defines the principle of unique choice to be
if $R$ is a relation between two sets $A$, $B$, and for every $...
3
votes
0
answers
358
views
Conversion of proofs between HoTT and ZFC
HoTT provides a foundation of math that remains mysterious for
many mathematicians including me. Hence this question.
There are several implementations of math based on ZFC, an
example being MetaMath. ...
2
votes
0
answers
67
views
Relation of top and bottom types given multiple universes
This is something that I haven't seen mentioned in any literature.
In a type theory (extensional, intuitionistic, Martin Lof variant), given two ordered Tarski Universes such that $U_i < U_{i+1}$, ...
2
votes
0
answers
207
views
A map that names itself
Call the walking arrow $\Delta_{1}$, containing exactly one nontrivial 1-cell $[0<1] : 0 \to 1$. I am interested in a map $\Phi : \Delta_{1} \to \mathrm{Type}$, such that $\Phi [0<1] = \Phi$ (...
2
votes
0
answers
210
views
Categorical semantics of the identity type
In Appendix B of the article Simplicial Model of Univ. Foundations, Definition B.1.3 specifies the structure for identity types in a contextual category $\mathcal{C}$ (which in particular is equipped ...
2
votes
0
answers
2k
views
How can one define "punctured torus" in Homotopy Type Theory? Is its fundamental group the free product of the integers with themselves?
Questions.
Has the beautiful old idea, in part already known to Gauß, of a punctured torus surface (take, if you will, the classical set-theoretic definition as the meaning of the latter three words)...
2
votes
0
answers
408
views
A potential definition of weak $\omega$-categories
This question was inspired by the Homotopy Type Theory Book.
Might we define a weak $\omega$-category as described below?
Is any similar approach already considered in the literature?
Let $\...
1
vote
0
answers
73
views
Directly proving the extensionality principle for product types without quasi-inverses
In section 2.6 of the Univalent Foundations Project's Homotopy Type Theory book, the extensionality principle of product types is proven by showing that for all elements $a:A$, $a':A$, $b:A$, $b':A$, ...
1
vote
0
answers
230
views
Understanding the double negation modality under the "propositions as types" paradigm
$\DeclareMathOperator\Hom{Hom}$I'm trying to understand the double negation modality under the "propositions as types" paradigm, but I'm running into an apparent contradiction: let $T$ be a ...
1
vote
0
answers
179
views
Synthetic type theory for virtual double category and its higher categories
For some monad T on a virtual equipment, the paper A unified framework for generalized multicategories by Cruttwell and Shulman (arXiv:0907.2460) proposes the normalized T-monoid.
Another paper, by ...
0
votes
0
answers
83
views
Univalence and higher inductive types in the lambda calculus model of type theory
In appendix A1 of the homotopy type theory book by the Univalent Foundations Project, the authors give a formal presentation of Martin-Löf type theory in lambda calculus. However, they did not give ...
0
votes
0
answers
213
views
Is there a foundational approach that takes "structure" as primitive?
As per the title, I'd be curious to know if there have been attempts at constructing a foundation of mathematics taking, somehow, purely the notion of "structure" as primitive, maybe via a system of ...