Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: univalent foundations for mathematics

Bottom of Page

1 to 29 of 29

  1.  

  1. Page created, but author did not leave any comments.

    Egbert Rijke

    v1, current

    • CommentRowNumber2.
    • CommentAuthorEgbertRijke
    • CommentTimeAug 4th 2020
    I set up the page with an initial layout, but it needs more work.
    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeAug 4th 2020

    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.

    diff, v2, current

    • CommentRowNumber4.
    • CommentAuthorEgbertRijke
    • CommentTimeAug 4th 2020
    I will add that sentence, and I will also add a note that more general higher inductive types are generally not considered to be a part of unimath.
    • CommentRowNumber5.
    • CommentAuthorEgbertRijke
    • CommentTimeAug 4th 2020
    Should there be a section containing a brief exposition of the most basic concepts of UF, namely equivalences, contractible types, propositions, sets, homotopy levels, and so on?

    If so, should it be a separate section, or should it go under the current "In HoTT" subsection.
    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeAug 4th 2020
    • (edited Aug 4th 2020)

    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.

    • CommentRowNumber7.
    • CommentAuthorEgbertRijke
    • CommentTimeAug 4th 2020
    I wrote something. It can be improved
    • CommentRowNumber8.
    • CommentAuthorEgbertRijke
    • CommentTimeAug 4th 2020
    BTW is it possible to get notifications from discussions on the nforum?
    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeAug 4th 2020

    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.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeAug 4th 2020
    • (edited Aug 4th 2020)

    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:𝒰A,B \colon \mathcal{U}” and “the canonical map (A=B)→(A≃B)(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!

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeAug 5th 2020

    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.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeAug 5th 2020

    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,

    1. univalent\,universes in type theory

    2. object classifiers in (elementary) ∞-toposes

    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,

    1. that there exists a type universe TypeType (also often denoted 𝒰\mathcal{U}) which reflects types and their equivalences, in that for any two types A,BA,B in that universe, them being equivalent as types is equivalent to them being equivalent (“equal”) as terms of type TypeType;

      the usual formal syntax for this statement of the univalence axiom is the famous expression

      (A≃B)equivalence as types≃;univalence;(A=B)equivalence as termsin the type universe \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) }

    2. that there exists an object classifier ObjectObject which reflects objects and their equivalences, in that for any two objects A,BA,B them being equivalent as objects is equivalent to their classifying maps to ObjectObject being equivalent (homotopic).

    diff, v7, current

    • CommentRowNumber13.
    • CommentAuthorEgbertRijke
    • CommentTimeAug 5th 2020
    @Mike, actually I decided to not include that sentence for the reason you cited :)
    • CommentRowNumber14.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 6th 2020

    Swapped (left/right) the order of the “famous expression”, and made the equivalence between the two sides a ⟶≃\stackrel{\simeq}{\longrightarrow}, rather than just ≃\simeq.

    diff, v8, current

    • CommentRowNumber15.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 6th 2020

    Reverted to \simeq, as the stackrel inside the underset seems to break something, though it renders fine in a latex file on my computer.

    diff, v8, current

    • CommentRowNumber16.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 6th 2020
    • (edited Aug 6th 2020)

    Reverted back to how it was, still breaking with (A≃B)(A\simeq B) on RHS. Will need to play in Sandbox when it’s not being used. But added doi link for David C’s Modal homotopy type theory.

    diff, v8, current

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeAug 6th 2020

    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”.

    • CommentRowNumber18.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 6th 2020

    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.

    • CommentRowNumber19.
    • CommentAuthorAli Caglayan
    • CommentTimeAug 6th 2020

    I am not sure that the statement of univalence is really correct here. Given terms AA and BB of the object classifier 𝒰\mathcal{U}, we have a map idtoequiv\mathsf{idtoequiv} which takes a path p:A=Bp : A = B and maps it to an equivalence A≃BA \simeq B. This is done by transporting along the path. The univalence axiom says that idtoequiv\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.

    • CommentRowNumber20.
    • CommentAuthorEgbertRijke
    • CommentTimeAug 7th 2020
    • (edited Aug 7th 2020)

    @Ali, any fiberwise equivalence (A=B)≃(A≃B)(A=B)\simeq(A\simeq B) indexed by A,B:𝒰A,B:\mathcal{U} implies that any fiberwise map (A=B)→(A≃B)(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 (Σ (B:𝒰)A=B)→(Σ (B:𝒰)A≃B)(\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)≃(A≃B)(A=B)\simeq(A\simeq B) for all A,B:𝒰A,B:\mathcal{U} is equivalent to Voevodsky’s axiom that used idtoequiv\mathsf{idtoequiv}, and therefore it is correct.

    • CommentRowNumber21.
    • CommentAuthorEgbertRijke
    • CommentTimeAug 7th 2020

    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.

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeAug 8th 2020

    Re #21: I think this is not the place to bring in cohesion!

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeAug 8th 2020

    The problem is that this passage in the entry (currently)

    the type of nn-dimensional vector spaces is simply the classifying space of the general linear group GL(n)GL(n)

    is misleading: The standard reading of “classifying space of the general linear group GL(n)GL(n)” refers to GL(n)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.

    • CommentRowNumber24.
    • CommentAuthorUlrik
    • CommentTimeAug 8th 2020

    Fix the ambiguity of the classifying space of the general linear group by adding a restriction to discrete fields. Include cyclically ordered sets as the classifying space of cyclic groups.

    diff, v9, current

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeAug 8th 2020

    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).

    diff, v10, current

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeJun 16th 2022

    Have Hilbert spaces been formalized in HoTT?

    (Is there a way to look up which subjects have?)

    • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeJun 16th 2022
    • CommentRowNumber28.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 17th 2022

    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?

    • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeJun 17th 2022

    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

  1.