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.
237
questions
5
votes
1
answer
102
views
What does it mean for a model category to present a higher category
A model category serves as an abstract/ axiomatic framework for homotopy theory. A higher category, in particular an $(\infty,1)$ category, I'm using the model of quasicategories, is a category with ...
- 53
3
votes
0
answers
92
views
What is the essence of infinity category theory?
*I understand that there are similar questions on this site and on the web, but I've failed to find any that give a satisfactorily plain enough answer for me to understand, given my background, and ...
- 245
2
votes
2
answers
83
views
What's the difference between a section and a dependent function?
I'm reading Introduction to Homotopy Type Theory by Egbert Rijke and get confused by the notions of a section and a dependent function.
A section is defined as:
Definition 1.2.2 Consider a type family ...
- 730
1
vote
0
answers
119
views
What can we say about the collection of sets $\{s_{ij}\}$ for some particular topos $T$?
Let $X$ be some space and let $T$ be topos on $X$ (e.g. Grohtendieck topos on the topological space).
Topos $T$ is the category of sheaves ${S_i}$, where each sheaf $S_i$ maps each open subset $O_j$ ...
- 1,265
0
votes
1
answer
105
views
Circularity in the proof of uniqueness principle for product types in HoTT book
This is possibly something I've overlooked while reading the HoTT book (section 1.5), on defining the product types and proving the uniqueness principle for it (every element of a product type is a ...
0
votes
1
answer
53
views
What collections of sets are appropriate for the "HoTT: Logic of spaces" and are they models?
There is very nice article https://arxiv.org/abs/1703.03007 "Homotopy type theory: the logic of space" which provides mapping among 1) Types of Homotopy Type Theory; 2) objects and morphisms ...
- 1,265
0
votes
0
answers
41
views
How category of diffeological spaces is related to the classifying category of HoTT? Maybe they are the same?
I am trying to read "Homotopy Type Theory: The Logic of Space" https://www.cambridge.org/core/books/abs/new-spaces-in-mathematics/homotopy-type-theory-the-logic-of-space/...
- 1,265
2
votes
0
answers
49
views
violation of Church Rosser with sum types
On https://ncatlab.org/nlab/show/sum+type the following $\eta$-reduction rule is given for sum types:
$$\mbox{match}(p,x.c[\mbox{inl}(x)/z],y.c[\mbox{inr}(y)/z]) \rightarrow_{\eta} c[p/z]$$
This rule ...
- 636
1
vote
1
answer
48
views
Interpretation of HoTT in the Reedy model structure on bisimplicial sets [closed]
I was trying to understand the interpretation of HoTT in the Reedy model structure on bisimplicial sets. While going through, it suggests to think of bisimplicial sets as having a "spatial" ...
- 539
14
votes
3
answers
512
views
Help! I don't believe in the identity elimination rule for Martin-Löf type theory/HoTT!
I was watching this video this video "$\infty$-Category Theory for Undergraduates" by Emily Riehl, and was onboard with everything except the path induction principle for identity types (27:...
- 8,363
2
votes
1
answer
90
views
Is it fair to say that Martin Löf Type Theory is doing the same for maths as what type theory did for programming languages?
Let me clarify what I mean.
I am currently writing a dissertation on ML/Homotopy type theory as someone who is more of a theoretical computer scientist than an Algebraist. My dissertation is focused ...
24
votes
3
answers
2k
views
Approaching Type theory and Category Theory as a starting point in the study of mathematics?
I'm a Computer Engineering student, with interest in Type Theory and Category Theory and i have a more pedagogical/philosophical question about these areas.
It seems that many researchers in Type ...
- 365
2
votes
1
answer
74
views
On iterated sigma type
Just to make sure I understand the notation in the excerpt below (from Corfield's "Modal Homotopy Type Theory") correctly, is the "sum" over $x:Activity, y:Achievement$" the ...
user1048887
1
vote
1
answer
93
views
Why is the circle not contractible in homotopy type theory?
I know that the circle type is not supposed to be contractible in homotopy type theory. But by the definition of contractible, it seems like it is.
Define the circle type $S^1$ as the higher inductive ...
- 187
1
vote
2
answers
69
views
What is the point of "typal" computation rules?
The (recently created) page titled integers type on ncatlab.org, in the section "As the inductive type generated by an element and an equivalence of types", gives two different forms of the ...
- 187
1
vote
0
answers
60
views
How does one prove that constructive type theory is isomorphism-invariant?
In his paper Structuralism, Invariance and Univalence (pdf), Steve Awodey makes the following claim about constructive type theory:
The system of type theory has the important property that any ...
1
vote
1
answer
38
views
univalence and indiscernibility
Given $A, B: U$ (where $U$ is a universe), define $\mathsf{Indis}(A, B)$ to be $\prod_{Q: U \rightarrow U} Q(A) \leftrightarrow Q(B)$. (This just says that $A$ and $B$ are in a certain sense ...
- 636
1
vote
1
answer
71
views
sum types in MLTT without universes
Suppose that $X$ and $Y$ are types that do not depend on anything else. Let $i$ be the usual function of type $X \rightarrow X+Y$ and $j$ be the usual function of type $Y \rightarrow X+Y$ discussed in ...
- 636
2
votes
0
answers
99
views
getting new results with universes
One remarkable thing about introducing a universe U (or many universes) into Martin-Lof Type Theory is that it allows us to show that certain types are inhabited that we would not otherwise be able to ...
- 636
2
votes
1
answer
80
views
An application of path induction
Does the rule of path induction (based or unbased, I don't care) allow us to infer
$$u:A, \ v:A, \ p:u=_A v \vdash t: p = \mbox{refl}(u) \hskip 1 cm (*)$$
for some term $t$? It seems to me that this ...
- 636
0
votes
0
answers
76
views
Is there algebra (algebraic manipulation) of simplicial sets?
Is there algebra of simplicial sets? For example, symbolic representation of simplicial sets and operations on those representations that allow to construct new simplicial set from existing one – join,...
- 1,265
1
vote
1
answer
57
views
defintional equality types
If $a$ and $b$ are definitionally equal terms of type $A$ - i.e., $a$ and $b$ can be $\beta \eta$ reduced to identical terms - what follows about the structure of the identity type $a=_A b$? For ...
- 636
5
votes
1
answer
147
views
What's wrong with this "proof" involving' $n$-connectedness in HoTT?
okay, this is silly, but I can't for the life of me figure out what's wrong with the following "proof":
Claim: if $B$ is an $(n-1)$-type, then $(n\text{-conn}(A) \to B) \simeq (\text{isCntr}(...
- 1,890
2
votes
1
answer
57
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
1
answer
142
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.
...
- 45
4
votes
1
answer
214
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 ...
- 41
5
votes
0
answers
172
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
15
votes
3
answers
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
4
votes
1
answer
109
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 ...
- 43
8
votes
0
answers
94
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 ...
3
votes
1
answer
122
views
What are canonical injections in Martin Lof type theory
In the following paragraph from Martin Lof's 1972 paper...
If $A$ and $B$ are types, then so is there disjoint union $A + B$, which is the type of objects of form $i(a)$ with $a:A$ or $j(b)$ with $b:...
- 379
0
votes
1
answer
119
views
Transport property
This question is prompted by Example 2.4.9 of the HoTT book. It is stated that, "for any $p:x =_A y$ and $P: A \to \mathcal{U}$ the function $\text{transport}^P(p,-): P(x) \to P(y)$ has a quasi-...
- 209
1
vote
1
answer
36
views
Defining the n-glob as a HIT
I'm trying to define n-globs, for each n. I'm trying to do this in terms of an indexed family of higher inductive types. I think I have a working definition but it is almost intractable and hard to ...
- 1,890
4
votes
0
answers
158
views
There's Homotopy Type Theory so why not "Homotopy Set Theory?"
If you have "Homotopy Type Theory" than does a more traditional "Homotopy Set Theory" exist too?
I think the simplest axiomization would be something like ZFC extended with a set ...
- 1,276
1
vote
1
answer
95
views
Homotopy Type Theory Path Lifting Property
Lemma 2.3.2 of the HoTT book states a path lifting property.
I want to give a formal proof, in the sense that I want to inhabit a particular type, rather than just assume by path induction that $p \...
- 209
1
vote
1
answer
99
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,890
1
vote
1
answer
74
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
2
votes
1
answer
33
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
4
votes
1
answer
185
views
Isomorphism vs. equivalence of types and homotopy vs. equality of functions
I am trying to build an understanding of the Univalence Axiom in HoTT and I am slightly confused about some definitions.
If I was asked after reading of Chapter 1 of the HoTT book to formulate a ...
- 2,778
6
votes
1
answer
315
views
What is problematic with formalizing higher category theory directly in HoTT
This is a soft-question. But please let me know if its not suitable. My question is essentially what the title asks but I want to elaborate on a few things.
I know Emily Riehl uses a type theory to ...
- 1,890
2
votes
1
answer
211
views
Is there a distinction between rules of inference and axioms in Homotopy Type Theory (HoTT)?
I'm taking rules of inference to be metalinguistic and to describe when you can write down a certain syntactic expression in the object-language given that you already have others written down (e.g. &...
- 393
3
votes
3
answers
170
views
Categorical Intuition of Path Induction
I am trying to understand path induction from the trinitarian point of view. So far I understand the informal intuition of path induction from a homotopical and computational point of view. But I am ...
- 1,890
1
vote
0
answers
78
views
Proof relevant relation
Let $$ac : \left( \prod_{(x:A)}\sum_{(y:B)}R(x,y) \right) \rightarrow\left( \sum_{(f : A \rightarrow B)}\prod_{(x:A)}R(x,f(x)) \right)$$
defined by $$ac(g) :\equiv \Big( \lambda x.pr_1(g(x)), \lambda ...
- 202
2
votes
1
answer
238
views
Recursor and induction functions in dependent type theory
I'm reading HoTT book and I'm not sure if I really understand how the recursor function is related to the induction function. It is stated that product types are said to be :
a degenerate example of ...
- 202
1
vote
1
answer
93
views
Propositional Uniqueness for Coproduct Types?
I'm working through the HoTT book and have just finished the section on coproducts. In short, I am wondering if there is a uniqueness principle for coproduct types. I can not find mention of one in ...
- 1,890
8
votes
2
answers
426
views
Object Classifier implies Univalence in Type Theory?
There is a correspondence between univalence in Type Theory and object classifiers in $\infty$-toposes. This, for example, is suggested in the article Univalent Foundations for Mathematics on nlab.
...
- 83
0
votes
1
answer
65
views
Definition of a map of (pre)spectra in HoTT
I'm trying to pick up some homotopy theory by reading various HoTT sources (I find it much easier than reading classical homotopy theory books). In Floris Van Doorn's PhD thesis he defines (pre)...
- 10.6k
3
votes
1
answer
105
views
How to show the double cover of $S^1$ is a circle in HoTT
Consider the family $E : S^1 \to \mathcal{U}$ so that
$E(\mathtt{base}) = \mathbf{2}$
$\text{apd}_E(\mathtt{loop}) = \mathtt{ua}(\lnot)$
where, of course, $\lnot : \mathbf{2} \simeq \mathbf{2}$ ...
- 36.7k
1
vote
1
answer
240
views
Ordinary mathematical uses of Axiom K
Context. In what follows, we work in Martin-Löf type theory (MLTT). We denote dependent product types by $\forall$, the identity type over a type $T$ by $\equiv_T$, and let $U$ stand in for arbitrary ...
- 9,897
1
vote
2
answers
116
views
Translating the induction principle from verbal form into rigorous one
According to the HoTT book [6.9], the propositional truncation $||A||$ of a type $A$ can be viewed as a higher inductive type generated by
A map $|-|: A \to ||A||$
A path in $x = y$ for any $x,y: ||A|...
- 4,606