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
Filter by
Sorted by
Tagged with
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 ...
Kaa1el's user avatar
  • 411
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 ...
Andy Manion's user avatar
  • 1,454
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$ ...
aws's user avatar
  • 3,836
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 ...
wlad's user avatar
  • 4,823
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$...
user3840170's user avatar
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 ...
Ben Sprott's user avatar
  • 1,281
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$,...
Madeleine Birchfield's user avatar
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 $...
Madeleine Birchfield's user avatar
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. ...
Student's user avatar
  • 5,008
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}$, ...
Daniel Smith's user avatar
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$ (...
Mathemologist's user avatar
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 ...
CuriousKid7's user avatar
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)...
Peter Heinig's user avatar
  • 6,001
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 $\...
Berci's user avatar
  • 201
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$, ...
Madeleine Birchfield's user avatar
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 ...
Alexander Praehauser's user avatar
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 ...
HuiFang's user avatar
  • 79
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 ...
Madeleine Birchfield's user avatar
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 ...
Qfwfq's user avatar
  • 22.7k