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.
Thanks for starting this.
Have made some minor edits:
de-capilalized the entry title, to comply with our running convention
touched the formatting throughout (section layout etc.)
added references
touched the wording at some places. Nothing major, but please check.
Where it says (further hyperlinks added by me):
The UniMath library also uses type in type, which leads to an inconsistency via Girard’s paradox.
some text should be added, lest this sounds funny. I suppose it could go as follows, but I let you choose how to deal with this:
The UniMath project also assumes the type in type-axiom. Strictly speaking, this makes the system inconsistent, due to Girard’s paradox. But the idea is that in practice the inconsistencies are readily avoided, so that the axiom serves as a convenient hack.
It would certainly be good to have, if you have the energy.
Since I had turned your section “In type theory” to a subsection of the “Idea”-section, and since what you are envisioning now is content that goes beyond the first idea, I suggest you open a new top-level section (please use double hash for top-level though! otherwise there is some bug). Maybe “Details” or the like.
Thanks, Egbert.
I never used notifications here, but on the top left of this nForum page, you see the words “Discussion feeds” and under that “RSS2” and “ATOM”. That should provide what you need.
Egbert, on your latest additions in Overview of the basic concepts:
I like this text – but is it an explanation of the entry’s title topic?
I imagine these technical explanations would work well in the entry univalence axiom (where they are largely missing).
But here, let’s imagine a reader who does Not already know what univalent foundations are. Maybe, if it helps, imagine speaking to the crowd on Twitter. Now for such interested but ignorant laypeople, how could we explain what “univalent foundations” is all about?!
It won’t help them to be given “$A,B \colon \mathcal{U}$” and “the canonical map $(A = B) \to (A \simeq B)$” – because anyone for whom these strings of symbols constitute a message already knows about univalent foundations!
Do you see what I mean?
We need to step back here. The reader who is going to profit from this entry will want to know:
What is “foundations” in the first place?
What are foundations like before they were univalent?
Why is/was that not satisfactory?
What is it that univalent foundations adds to the picture, and why?
Maybe for starters, let’s imagine a reader who does already know about formal mathematics in type theory, but does not appreciate HoTT and univalence. Think of XenaProject or the like. Now let’s make the entry explain the idea, the point and the main technical fine-print to such readers!
will also add a note that more general higher inductive types are generally not considered to be a part of unimath.
If by “unimath” you mean the library UniMath, then sure. But I don’t see any justification for excluding HITs from “univalent foundations for mathematics” in the general sense of the latter term.
I went ahead and tried my hand on an informal explanation as I was suggesting in #10.
Currently it reads as follows:
A univalent foundations for mathematics refers to any foundational system in which universes are object classifiers, or, equivalently, satisfy the univalence axiom.
Specifically, this applies to mathematical foundations in (a) dependent type theory, or in (b) topos theory, respectively, which – apart from exactly such fine-print on the existence and nature of universes – correspond to each other under the syntax/semantics-relation between type theory and category theory.
Here, univalent foundations is in contrast to other (earlier) approaches of laying foundations in type theories or toposes, that have (only) a universe of propositions or (only) a subobject classifier, respectively, hence where only a truncated sub-class of all types/objects is reflected in the universe.
The basic idea of univalent foundations is, simply, to allow for universes that reflect all types/objects. Or rather – to avoid the notorious inconsistencies of the form of Russell’s paradox/Girard’s paradox – universes that reflect all those types/objects that are “small” compared to the universe. It is this technical subtlety – due to which a type/object may not be reflected in a given universe (namely if it is too large) but if it is, then it is so essentially _uni_quely – which motivates the term “_uni_valent”.
The term “univalent foundations” as such was coined by Voevodsky 11, much popularized with the textbook UFIAS 12, and is usually taken to refer to mathematical foundations based on Martin-Löf dependent type theory, or similar, with the univalence axiom imposed on the type universe. But the existence of (the categorical semantics of) such “univalent type universes” in higher analogues of toposes (“∞-toposes”) was observed (and published) earlier in Lurie 09, Sec. 6.1.6, there called _object classifiers in _ and attributed to yet earlier private conversation with Charles Rezk.
That both concepts,
do indeed correspond to each other was understood from the beginning (see Shulman 12a, lecture 3, slide 3, for the statement); based on proofs in special cases Shulman 12b. Full proof appeared in Shulman 19.
Concretely, what makes univalent foundations univalent is the condition, respectively,
that there exists a type universe $Type$ (also often denoted $\mathcal{U}$) which reflects types and their equivalences, in that for any two types $A,B$ in that universe, them being equivalent as types is equivalent to them being equivalent (“equal”) as terms of type $Type$;
the usual formal syntax for this statement of the univalence axiom is the famous expression
$\underset{ \color{blue} \text{equivalence as types} }{ (A \simeq B) } \underset{ \color{blue} ;\;\text{univalence};\; }{ \simeq } \underset{ \color{blue} \text{equivalence as terms} \atop \text{in the type universe} }{ ( A = B) }$that there exists an object classifier $Object$ which reflects objects and their equivalences, in that for any two objects $A,B$ them being equivalent as objects is equivalent to their classifying maps to $Object$ being equivalent (homotopic).
David, I think it’s okay how it is: For the Idea-section, it’s good to suppress technical detail if it doesn’t further the understanding of the basic idea. Few readers who don’t already know univalent foundations would be helped at this point with knowing that there is a preferred direction to this equivalence.
If you want to add detailed explanation, it should go further down into the technical part – such as expanding the paragraph that talks about “the canonical map”.
Yeah, it’s not that crucial. There was an issue with the two lines of blue text: only one was blue (at least, after I was fiddling with it), so I made them both blue. I presume that was your intention, as it works that way on my local TeX installation, just not in the nLab’s iTeX it seems.
I am not sure that the statement of univalence is really correct here. Given terms $A$ and $B$ of the object classifier $\mathcal{U}$, we have a map $\mathsf{idtoequiv}$ which takes a path $p : A = B$ and maps it to an equivalence $A \simeq B$. This is done by transporting along the path. The univalence axiom says that $\mathsf{idtoequiv}$ is an equivalence.
Secondly, it is written that the classifying space for GL(n) can be taken as the type of vector spaces. This type is a 1-type so perhaps it would be good to mention that GL(n) is a discrete group. It is unclear at the moment if the homotopy type of the topological group GL(n) can be expressed in book HoTT. In fact, this seems to be related to a question in classical algebraic topology which is to determine the attaching maps of the (complex/real) grassmannians. That, to my knowledge, is only known for real and complex projective spaces where the attaching maps are induced from the tautological bundles. The other attaching maps, the ones that stick schubert cells together are somewhat non-trivial and there have been various efforts to detect them using secondary cohomology operations.
In short, it should be mentioned that GL(n) is a disctete group and the not the homotopy type of the topological group which is probably very non-trivial.
@Ali, any fiberwise equivalence $(A=B)\simeq(A\simeq B)$ indexed by $A,B:\mathcal{U}$ implies that any fiberwise map $(A=B)\to(A\simeq B)$ is an equivalence, via the fundamental theorem of identity types. This is because any fiberwise equivalence induces an equivalence $(\Sigma_{(B:\mathcal{U})}A=B)\to (\Sigma_{(B:\mathcal{U})}A\simeq B)$, and the former type is contractible. So the statement $(A=B)\simeq(A\simeq B)$ for all $A,B:\mathcal{U}$ is equivalent to Voevodsky’s axiom that used $\mathsf{idtoequiv}$, and therefore it is correct.
The homotopy type of GL(n) is just the shape of the discrete GL(n), which is definable in Book HoTT as the nullification at the Dedekind reals. This is indeed one approach to define the Grassmannians.
Re #21: I think this is not the place to bring in cohesion!
The problem is that this passage in the entry (currently)
the type of $n$-dimensional vector spaces is simply the classifying space of the general linear group $GL(n)$
is misleading: The standard reading of “classifying space of the general linear group $GL(n)$” refers to $GL(n)$ with its cohesive structure.
To fix this, one could either add a qualifier “discrete” here, as Ali suggested in #19, or replace by an example that does not require mentioning cohesion in order to do it justice.
Thanks. I changed the link discrete field to point to discrete topology (currently discrete field redirects to field which discusses the constructive notion of “discrete field” that is not really what is meant).
Have Hilbert spaces been formalized in HoTT?
(Is there a way to look up which subjects have?)
added pointer to:
Re #26, the community had a useful habit of including “in homotopy type theory” in the title of their papers, as with many at mathematics presented in homotopy type theory. I can’t see anything about Hilbert spaces though.
Might that axiomatisation of HIlb allow for a more synthetic treatment?
Thanks. Right, it does not seem to exist.
I was after the actual construction of Hilbert spaces, specifically of the space of Fredholm operators on a separable Hilbert space. So the axiomatic description would not help me here. On the other hand, I’d really need this for cohesive HoTT with a real line type, and I gather they won’t have looked into this at any of the active formalization projects.
1 to 29 of 29