Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
created homotopy level
However, the instiki-table does not come out correctly yet. It did before I added the third column. These tables are the most delicate things. I never know why sometimes they display correctly and sometimes not.
The table at the bottom of the entry does not appear as table when seen in my firefox, but as a hard to read list. By the way title in the title of this nForum post.
title in the title
I know what you mean ;-) I have fixed it.
I just made typo in the typo :)
The table is fixed.
Thanks, Toby!
Can you explain what you did to fix it? Is it that the horizontal line of minus-signs is shorter?
Do you know what the rules of the game are? Which syntax rule did my original table violate?
First, I copied and pasted the table into a text editor with a larger window size, so that each row would actually fit into one row. Then it became obvious that one of the horizontal lines was supposed to be a vertical line, so I changed it. Then I added a bit to the groupoid column, which ironically made some of the rows even longer, so that they no longer fit into one row even in my larger window!
Then it became obvious that one of the horizontal lines was supposed to be a vertical line
Oh, okay, so I guess I had an evident typo in there. Thanks.
I’ve created h-set, h-prop, and equivalence in homotopy type theory, and added corresponding material to contractible type — several definitions in all cases, along with semantic interpretations in model categories. I also moved the theorem “decidable $\Rightarrow$ set” from set to h-set.
Right now I am having trouble parsing this here, in hSet:
$\array{Paths_A + (0\to A\times A)^{(Paths_A\to A\times A)}\\ \downarrow\\ A\times A}$Is “0” the inital type? What’s the purpose of it here? What is the “+”?
Ah, never mind, I get it from the text below. Maybe I may add some comments on how to read this?
Sure.
I thought it odd to say that any two elements of an h-set are equal or not when describing an inherently constructive theory. And the point is not that you can say this but that this is all that you can say. So I edited this remark in h-set.
made a start at adding references:
These as examples of the actual use of “hlevel”:
Guillaume Brunerie, Truncations and truncated higher inductive types (2012) [blog post]
This one for completeness, though it doesn’t say “hlevel”:
and then the single reference that used to be here (but was just dead link) I have polished up to:
but I haven’t actually seen this text.
added pointer (here and elsewhere) to:
added the original reference:
1 to 18 of 18