Recent Changes

Friday, June 19

Friday, April 3

Friday, May 30

  1. page Home edited ... Welcome to the wiki of the special year on Univalent Foundations of Mathematics 2012/2013 at t…
    ...
    Welcome to the wiki of the special year on Univalent Foundations of Mathematics 2012/2013 at the Institute for Advanced Study in Princeton, NJ, coorganized by Steve Awodey, Thierry Coquand and Vladimir Voevodsky.
    This wiki contains various material relevant to this special program.
    Note: Now that the special program is over, there is a new wiki dedicated to the subject of homotopy type theory and univalent foundations, which should be used instead of this one (and content migrated over as possible). It can be found here.
    Organization
    A list of the participants to the special year is available at IAS program participants
    (view changes)
    8:02 am

Thursday, October 31

  1. 6:19 am

Saturday, August 24

  1. page Open Problems edited ... Here are problems related to type theory and univalent foundations which are not just re-proof…
    ...
    Here are problems related to type theory and univalent foundations which are not just re-proofs of theorems from classical mathematics.
    Define the notion of a (semi-) simplicial type in type theory. Here is a description.
    ...
    h-level n-1). (Didn't Nicolai do this?)
    Let TT^+ be the intensional type theory with a sequence of universes + for each n>0, an axiom asserting that there are types strictly of h-level n. Show that the addition of axioms asserting that each universe is univalent does not increase the logical strength (in the proof theoretic sense) or perhaps show that it does.
    Is there a Quillen model structure on semi-simplicial sets (with semi-simplicial Kan fibrations) making it Quillen equivalent to simplicial sets (with Kan fibrations)?
    ...
    Prove that the torus (with the HIT definition involving a 2-dimensional path) is equivalent to a product of two circles.
    Study the fundamental group / loop space of a wedge of circles indexed by an arbitrary set A. If A has decidable equality, then you can prove that the loop space is equivalent to the free group on A (see here). If A does not have decidable equality, it is most likely still true that the fundamental group of the wedge of circles is equivalent to the free group (I haven’t formalized it yet), but the loop space seems more complicated and does not even seem to be a set.
    Prove that every precategory is equivalent (in some sense) to a category (where equality on objects is equivalent to isomorphism in the category). The previous open problem is an easy corollary of this one, you just have to turn the one-object category with G as set of arrows into a category and you get a K(G,1).
    Show that the homotopy groups of spheres are all finite except for those of the form π_n(S^n) or π_{4n−1}(S^(2n)) (for positive n), when the group is the product of Z with a finite abelian group.
    Closed formalization problems :)
    ...
    Prove that if a function A -> B induces a bijection on connected components and for any base point induces an equivalence between loop spaces, then it is an equivalence (solved by Dan)
    Prove the Freudenthal suspension theorem (solved by Peter L. and Dan).
    Prove that every precategory is equivalent (in some sense) to a category (where equality on objects is equivalent to isomorphism in the category). (solved by Benedikt and Chris K.)
    (view changes)
    12:24 pm

Sunday, June 30

  1. page Semi-simplicial types edited ... CL.pl {CL.pl} , the prover for coherent logic (requires SWI-Prolog) X.in {X.in} , a formaliza…
    ...
    CL.pl {CL.pl} , the prover for coherent logic (requires SWI-Prolog)
    X.in {X.in} , a formalization of the model in coherent logic
    X.mod,X.model {X.model} , the model (edges, filledges, fill1 and fill2, day by day)day, generated by
    X.v {X.v} , a Coq script verifying the proof that no homotopy equivalence between the fibers can exist in the model
    Finite-dimensional parts
    (view changes)
    12:55 pm
  2. file X.model uploaded
    12:51 pm
  3. page X.mod edited {X.mod}
    {X.mod}
    (view changes)
    12:45 pm
  4. page Semi-simplicial types edited ... Update 4/15: A note on a presheaf model for simplicial sets {countermodel.pdf} by Marc Bezem…
    ...
    Update 4/15: A note on a presheaf model for simplicial sets {countermodel.pdf} by Marc Bezem and Thierry Coquand
    Update 6/24: Accompanying files to Update 4/15:
    X.in {X.in} , a formalization of the model in coherent logic
    CL.pl {CL.pl} , the prover for coherent logic (requires SWI-Prolog)
    X.in {X.in} , a formalization of the model in coherent logic
    X.mod, the model (edges, fill and fill2, day by day) generated by the prover from input X.in

    X.v {X.v} , a Coq script verifying the proof that no homotopy equivalence between the fibers can exist in the model
    Finite-dimensional parts
    (view changes)
    12:38 pm
  5. file X.mod uploaded
    12:26 pm

More