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 10605
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.
12
votes
Accepted
Delooping in homotopy type theory
The definition you gave is not of an $A_\infty$-space, but just of $A_1$-space. As Charles noted, these two classes of spaces are very different in general. For example, there are also higher isomorph …
- 4,780
4
votes
Accepted
How to proceed with a type-theoretic proof that $\Sigma \mathbb{S}^1 \simeq \mathbb{S}^2$?
I'm not sure if it is the most elegant way, but it is certainly the most direct. So, we need to define the image of $\mathrm {surf}$ as an element of $refl_{\mathrm N} = refl_{\mathrm N}$. We proceed …
- 4,780
3
votes
(Co)limits of locally cartesian closed categories
I was talking about the following tentative argument. The 2-category of distributors (also called profunctors) $\mathrm{Dist}$ has (small) categories for objects. For $C,D:\mathrm{Dist}$ the 2-categor …
- 4,780
1
vote
Homotopy type theory: Are the hierarchy of Type_k universes isomorphic?
The Univalence axiom states that homotopy equivalent types are equal. That doesn't mean the hierarchy is collapsible: that would require judgemental and not Leibniz equality. The very point of HoTT is …
- 4,780
6
votes
Accepted
Can Homotopy Type Theory or algebraic geometry deal with homotopy fibers in terms of families?
Yes, there is a certain sense in which your statements are true. As Mike Shulman and Qiaochu Yuan said, the strict fiber of a map cannot be defined in HoTT and doesn't make sense, but you can work fro …
- 4,780
4
votes
The groupoid of algebraic expressions and proofs
I don't have any direct reference for the notion that you are describing, however the notions of $E_n$-algebras and (topological) operads are very close. Firstly, you should note that you need equalit …
- 4,780