Search Results
| Search type | Search syntax |
|---|---|
| Tags | [tag] |
| Exact | "words here" |
| Author |
user:1234 user:me (yours) |
| Score |
score:3 (3+) score:0 (none) |
| Answers |
answers:3 (3+) answers:0 (none) isaccepted:yes hasaccepted:no inquestion:1234 |
| Views | views:250 |
| Code | code:"if (foo != bar)" |
| Sections |
title:apples body:"apples oranges" |
| URL | url:"*.example.com" |
| Saves | in:saves |
| Status |
closed:yes duplicate:no migrated:no wiki:no |
| Types |
is:question is:answer |
| Exclude |
-[tag] -apples |
| For more details on advanced search visit our help page | |
Results tagged with homotopy-type-theory
Search options not deleted
user 49
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.
2
votes
Construction of the necklace by homotopy type theory
My guess would be
Inductive Necklace (n:nat) :=
| strand : Circle -> Necklace
| bead : forall (k:nat), k<n -> Sphere2 -> Necklace
| attach : forall (k:nat) (p:k<n), strand base = bead k p base2.
- 66.8k
9
votes
A pointless circle in HoTT
Francois' answer is good; let me add a bit more. Homotopy type theory is synthetic homotopy theory, which means that the "spaces" in question are not the same sort of "spaces" that you find in point- …
- 66.8k
7
votes
Accepted
Functional programing and intensional type theory
GHC doesn't eat extensional dependent type theory. The type theory of GHC has some fancy bells and whistles that allow you to fake some things you can do with dependent types, but it isn't truly depe …
- 66.8k
6
votes
Accepted
Models for Higher Inductive Types in Homotopy Type Theory
https://arxiv.org/abs/1705.07088 . I've updated the nLab page.
There are also some slides available at my web page.
10
votes
Accepted
Checking the functoriality of an expression involving dependent sum and product
You are right that $(-)^{\mathsf \Pi}$ is not functorial on the arrow category of $\mathcal{C}$. However, it is functorial on the category whose objects are arrows in $\mathcal{C}$ and whose morphism …
- 66.8k
7
votes
Accepted
Defining (infinity,1)-categories in HoTT using only an interval type
The shape/tope type theory is indeed just a "convenience". When I first suggested this approach to synthetic $(\infty,1)$-categories, I took the approach you describe with a simple axiomatic interval …
- 66.8k
10
votes
Accepted
Homotopy type theory: why are $0:\mathbb N$ and $\mathrm{succ}(0):\mathbb N$ not judgemental...
Daniel's answer is correct that the judgmental distinctness of $0$ and $\mathsf{succ}(m)$ is not what justifies a definition by pattern-matching. However, it is still a meaningful question of how to …
- 66.8k
2
votes
Small complete categories in HoTT+LEM
Let's try to fix the "other side" instead: can we modify the proof to give an embedding $2^{C(a,z)} \hookrightarrow C(a,z)$? The embedding $2^{C_1} \hookrightarrow C(a,z)$ in the original proof follo …
- 66.8k
13
votes
Practical example in using (homotopy) type theory
The answers and comments on this question show that there is still a ton of misinformation out there about HoTT.
The short answer (but much more time-consuming for you) is that you should read the Ho …
- 66.8k
7
votes
Accepted
Construct higher inductive types with only generalized algebraic data types and non-truncate...
No, it is not.
One can do a lot with just homotopy pushouts/coequalizers (I assume this is what you mean by "non-truncated quotients"). For instance, Egbert Rijke showed in The join construction that …
- 66.8k
12
votes
Accepted
Uniqueness Principle for function types
It is not true "by construction". Remember that at this point in the theory a "function" is an abstract undefined thing, not something "defined by its action on inputs" as it is in set theory. The o …
- 66.8k
5
votes
Question about higher inductive types and computational rules
If I understand the question correctly, one answer is that the rules of type theory are not (supposed to be) arbitrarily chosen independently of each other like the axioms of set theory are. They com …
- 66.8k
1
vote
Question about higher inductive types and computational rules
A different answer is that one of the purposes of higher inductive types is to define homotopy types containing nontrivial paths. The judgmental equalities coming from computation rules cannot give r …
- 66.8k
5
votes
How do you define the strict infinity groupoids in Homotopy Type Theory?
Here's a partial answer to a related question. In classical stable homotopy theory, a spectrum is equivalent to a "strict" one (arising from a chain complex) if and only if it admits the structure of …
- 66.8k
21
votes
Role of univalence in homotopy group calculations
"Isomorphic structures are equal" is a cute slogan, but it sometimes gets in the way because it sounds like it's saying that it forces isomorphic structures to be related by the pre-existing notion of …
- 66.8k