Andy Melnikov (nponeccop) wrote,
Andy Melnikov

New foundations must provide a way to work constructively not only with sets but also with higher analogs of sets.

The objects of set-theoretic mathematics which most closely correspond to "higher sets" are higher groupoids. By Grothendieck's insight groupoids of all levels may be considered as homotopy types.

What we usually call "category-level" mathematics in fact works with structures on groupoids. It is easy to see that a category is a groupoid level analog of a partially ordered set.

It was originally assumed that Martin-Lof theory is something like a constructive set theory. Types were interpreted as sets and constructions on types as corresponding constructions on sets.

The first hint that Martin-Lof type theory may have something to do with homotopy types appeared in 1996 when Martin Hofmann and Thomas Streicher constructed a new semantics for a version of this theory which interpreted types not as sets but as groupoids.

Univalent Foundations of Mathematics is Vladimir Voevodsky’s new program for a comprehensive, computational foundation for mathematics based on the homotopical interpretation of type theory. The type theoretic univalence axiom relates propositional equality on the universe with homotopy equivalence of small types. The program is currently being implemented with the help of the automated proof assistant Coq. The Univalent Foundations program is closely tied to homotopy type theory.
Tags: fp, programming

  • Post a new comment


    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.