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
2
votes
1
answer
133
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
0
votes
1
answer
44
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.
- 395
-1
votes
2
answers
165
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
2
votes
1
answer
49
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
1
answer
79
views
For any module with vector set $V$ and scalar set $C$, must there exist a set $X$ such that $V$ and $(X → C)$ are isomorphic?
Here's some evidence that suggests the affirmative to my question. There exists an isomorphism between:
$\mathbb{R}^{n}$ and $(\mathbb{N}^{<n} \to \mathbb{R}$)
$\mathbb{R}^{\infty}$ and ($\mathbb{...
2
votes
2
answers
114
views
HoTT and isomorphisms
I have heard that Homotopy Type Theory makes it so that isomorphic objects are “equal”. I wonder how this squares with a lot of mathematical examples from Algebra and Set Theory, where the nature of ...
- 2,049
3
votes
1
answer
64
views
Why aren't $\infty$-groupoids commutative in HoTT?
I'm trying to read through HoTT, but I'm confused by the path induction principle, it seems too strong at the first glance. I tried "proving" that all suitable paths commute, and it looks ...
- 7,585
1
vote
1
answer
56
views
Is the set-indexed wedge of connected $1$-types a $1$-type?
We are working in homotopy type theory.
Given a type $I$ and a family of pointed types $P : \prod i : I, \sum T : Type, T$, we can define the wedge product $\bigvee\limits_{i : I} P(i)$ as a certain ...
- 32.2k
0
votes
0
answers
108
views
What are the axioms of homotopy type theory?
The primitive notions of Zermelo-Fraenkel set theory are those of set and membership, i.e. we don't define what we mean by 'set' neither what we mean by '$\in$', rather, the axioms define what we mean ...
- 326
4
votes
2
answers
217
views
LEM and the curry-howard correspondence
The curry-howard correspondence rests upon constructive/intuitionistic logic. Proof checkers only work because they are guaranteed to halt. Proof checkers are built on the simply typed lambda calculus ...
user590921
0
votes
0
answers
92
views
Classicalities of Homotopy Type Theory
What are statements of HoTT that are not provable therein and thus may or may not be true in specific models, specifically models in $(\infty,1)$- topoi? I've also seen the term "classicalities&...
- 63
6
votes
1
answer
236
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 ...
- 63
3
votes
0
answers
196
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 ...
- 275
3
votes
2
answers
116
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 ...
- 740
1
vote
0
answers
124
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,323