An Introduction to Homotopy Type Theory

  • July 28, 2014 · 7:00 PM
  • Mixrank

Few are those who have ventured into the land of Homotopy Type Theory and returned to tell the tale, but our fellow Typo Jack Fox is one of them, and he's willing to share his adventures with us.

Jack's description: Background and review of Martin-Löf type theory leading up to HoTT. Material covers the introduction, first 2 chapters, and appendices of The Hott Book. These slides http://www.slideshare.net/jackfoxy/type-theory-and-practical-application form the basis of the talk, though I reserve the right to fold, spindle, mutilate, or insert any and all slides at any time leading up to and during the presentation.

The code *1111 will gain you admission through the front gate at Mixrank.

Join or login to comment.

  • Jack F.

    I fixed a major blunder on my slides. http://www.slideshare.net/jackfoxy/homotopy-type-therory The family signature is very much a simple function signature. I have more to say about this, which I hope to get up on my blog before the very interesting upcoming subtyping meetup http://www.meetup.com/SF-Types-Theorems-and-Programming-Languages/events/200656362/

    September 1

  • Sergei W.

    I found an interesting dissertation on the topic of intuitionistic logic. Difficult to obtain but still exists online:
    https://web.archive.org/web/20040325142957/http://www.mathematik.uni-muenchen.de/~weich/diss/diss.pdf

    The thesis develops certain efficient methods of deciding whether a formula is provable or not in
    propositional intuitionistic logic.

    August 20

  • Vlad P.

    Well, the question about two-valued intuitionistic logic, I think, was pretty legitimate. If you are in a topos, and your subobject classifier is 1+1, you are in a boolean topos, period.

    July 28, 2014

    • Sergei W.

      We didn't have only two logical values; we had full intuitionistic logic, and the two boolean values were just some of the values we can play with in this logic. Intuitionistic logic cannot be 1-to-1 mapped onto any finite set of truth values. I have been playing with the idea of proving/disproving intuitionistic theorems by computations in a specially designed set of truth values. Right now, my best guess is that, given an intuitionistic formula with a few variables, one can construct a finite truth-values model that will be sufficient for proving or disproving this formula. For example, A or (not A) can be disproved by using just three truth values (0, 1, undefined).

      July 29, 2014

    • Vlad P.

      a three valued logic is an example of intuitionistic logic, fyi.

      July 31

  • Jack F.

    1 · July 29, 2014

  • Ian Z.

    ZFC rules! <runs for cover/>

    July 23, 2014

    • Ian Z.

      I'm sure my unapologetically classical mathematical education is to blame, but I am more confused than ever.

      July 28, 2014

    • Vlad P.

      Ian, it may make sense to discuss this stuff at BACAT, and go deeper into the foundations. We can dedicate our September meeting to these issues. (I disagree regarding ZFC, although it's definitely a sound foundation.)

      July 28, 2014

  • Steven S.

    The slides are great! Hope someone's recording a video of the event :)

    July 28, 2014

  • Jon A S.

    this stuff is soooo over my head.

    when i grow up, i want to KNOW homotopy type theory.

    1 · July 6, 2014

    • Dave D.

      Likewise. Reading the preso slides right now, can't make it tonight =(

      July 28, 2014

  • Adrian K.

    I'm still working through my befuddlement that equality can be different in different directions. What does that mean in practical terms? Will we be enlightened?

    1 · July 22, 2014

    • Sergei W.

      But his slides have very little text, and he didn't include any pictures that are worth a thousand words.

      July 26, 2014

    • Sergei W.

      He wrote a report that seems to be useful,
      http://www.cs.nott.ac...­
      http://www.cs.nott.ac...­
      http://www.cs.nott.ac...­

      July 26, 2014

  • Sergei W.

    I watched Voevodsky's presentation linked in Jack's slides, - very inspirational! http://video.ias.edu/node/6395

    1 · July 7, 2014

  • A former member
    A former member

    Thanks for offering to teach us about this. I've been curious about it for a while. If possible could you include some exercises for the group?

    July 6, 2014

    • Jack F.

      I'll include some.

      July 7, 2014

People in this
Meetup are also in:

Create a Meetup Group and meet new people

Get started Learn more
Allison

Meetup has allowed me to meet people I wouldn't have met naturally - they're totally different than me.

Allison, started Women's Adventure Travel

Sign up

Meetup members, Log in

By clicking "Sign up" or "Sign up using Facebook", you confirm that you accept our Terms of Service & Privacy Policy