# Questions tagged [homotopy-type-theory]

For questions about homotopy type theory, including the homotopy theoretic interpretation of type theory or univalent type theory, univalence axiom, higher inductive types or related.

248 questions
Filter by
Sorted by
Tagged with
130 views

### Definite description in homotopy type theory

I asked this question there and I have been suggested to ask it here. In a paper by David Corfield, we have an account of definite description in homotopy type theory. The author gives the following ...
• 308
42 views

### Internal vs External in type theory

I'm learning type theory, and at one point in the HoTT book, is mentionned "external" constructions. I was wondering what precisely means internal/external in type thoery.
• 329
164 views

### What is a "type" in type theory?

Types are taken as atomic in type theories like homotopy type theory. But what is the best way to conceptualize what a type is? Is it appropriate to think of them as a property that defines a category?...
• 101
48 views

### Circularity in the definition of natural numbers with homotopy type theory

I am reading HoTT's book, I am interested in this theory because it is said that it works as a foundation of mathematics, so I want to see how this foundation works. I am interested in the definition ...
• 326
1 vote
77 views

• 1,947
63 views

### In Homotopy Type Theory, do $x, y$ exist such that $x = y$ is inhabited but $x \not\equiv y$?

I'm new to Homotopy Type Theory and am trying to understand the difference between judgemental and propositional equality. To my understanding, if $x,y: A$ for any type $A$ and $x \equiv y$, then one ...
1 vote
148 views

### Proving that W-algebra homomorphisms are contractible

I don't understand the conclusion of the proof of Theorem 5.4.7 of the Homotopy Type Theory text and would like a more detailed explanation of how it works. Here's my attempt at divining an answer. ...
• 47
255 views

### The first-order metatheory of HoTT

Does there exist a (say, simply typed) first-order theory which axiomatizes a universe of $\infty$-groupoids, in a similar manner to how ZFC can be considered as an axiomatization of the universe of ...
• 141
188 views

### Reference for basic metatheory of Martin-Löf type theory

Section A.4 of the HoTT book states that the metatheoretic properties of Martin-Löf type theory (such as normalization and canonicity properties) can be proved using “standard techniques from type ...
• 792
1k views

### In homotopy type theory, what are the intermediate values along a path?

I'm having a hard time understanding how the continuous notion of a path applies to homotopy type theory. I understand that from topology, a path is a continuous function $f : [0,1] \to X$ from the ...
• 375
130 views

### In homotopy type theory, why is function extensionality usually considered an axiom?

My understanding is that function extensionality follows from univalence. But I often see both function extensionality and univalence assumed as axioms, e.g., here. Wouldn't it be better to have fewer ...
112 views

### Is every homotopy equivalence a fibration over the interval?

It is a well known fact from homotopy theory that if $X\to Y$ is a Hurewicz fibration and $y_0,y_1$ are two points of $Y$ connected by a path $y_0\sim y_1$, then the fibers over $y_0$ and $y_1$ are ...
133 views

• 209
1 vote
108 views

### HoTT Book: Proof of Lemma 4.1.1 and exerices 2.17, using univalence

I have a question about a certain method of proof used in the HoTT book. This question might just boil down to how univalence is used in practice. The method of proof I have in mind can be seen in one ...
• 1,947
1 vote
76 views

### Indiscernability of identicals (HoTT)

In 1.12 of the HoTT book it is mentioned that it is a simple exercise to show that indiscernability of identicals follows from path induction. I am getting the sense that it is a special case but I am ...
• 209
34 views

### Proving a proposition by inhabiting a type

I am working through HoTT and it was suggested (on page 43) that the reader prove the following proposition, if not(A or B) then (not A) and (not B) by exhibiting an element of the type \$(A+B \to 0) \...
• 209