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

Discussion Tag Cloud

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 > nLab General Discussions: HoTT Open Problems: Kenzo Verification

Bottom of Page

1 to 2 of 2

  1.  
    • CommentRowNumber1.
    • CommentAuthorbubble-07
    • CommentTimeSep 6th 2017

    I see that on the open problems in Homotopy Type Theory page, the question “Can we verify computational algebraic topology using HoTT?” is listed, with a link to Kenzo. I did some digging, and a presentation by Heras et al. seems to suggest that the Basic Perturbation Lemma has been proved in Coq (without univalence, HITs or quotient types to get around using setoids, etc.) Given that the Basic Perturbation Lemma is somewhat central to Kenzo’s operation, what would we expect/hope to gain from formalizing it again in book HoTT?

    Looking beyond the BPL, what other formalization efforts would help fulfill the stated goal?

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeSep 6th 2017

    I’m not sure what whoever stated that problem had in mind, but what I would find more interesting is a formalization in which the “algebraic topology” that Kenzo is talking about is related somehow to the synthetic homotopy theory of HoTT.

1 to 2 of 2

  1.