wikipedia pages
2 views
Skip to first unread message
Vladimir Voevodsky
Nov 30, 2014, 7:59:04 AM11/30/14
to homotopytypetheory, Prof. Vladimir Voevodsky
Hello,
looking at the wikipedia page for homotopy type theory I see the following:
In mathematical logic and computer science, homotopy type theory (HoTT) attempts to give an account of the semantics of intensional type theory using the framework of (abstract) homotopy theory, in particular Quillen model categories and weak factorization systems.
and
HoTT allows mathematical proofs to be translated into a computer programming language for computer proof assistants much more easily than before. This approach offers the potential for computers to check difficult proofs.[1]
These two statements are incompatible. Either we say as it really is that HoTT started with the construction of a univalent model of the Martin-Lof type theory by Vladimir Voevodsky in 2009 and move the stuff about abstract homotopy theory and Quillen model structures in a section describing one of the branches of HoTT or we remove any mention about proof assistants and formalization of mathematics from the page and I start distancing myself from HoTT.
Vladimir.
Peter LeFanu Lumsdaine
Nov 30, 2014, 8:36:33 AM11/30/14
to Vladimir Voevodsky, homotopytypetheory
I agree, the Wikipedia article is currently somewhat inaccurate and inconsistent. But it’s Wikipedia, not an official history on the HoTT website or something — on the one hand, any of us can change it if we have the time, but on the other, all it should be taken as representing is the views of some small random selection of people at some small random selection of times. It would be a great shame if you (or anyone else) turned away from any part of the field because someone once wrote a few misrepresentative paragraphs on Wikpedia.
–p.
Steve Awodey
Nov 30, 2014, 8:51:15 AM11/30/14
to Vladimir Voevodsky, homotopytypetheory
we cannot really control what wikipedia says — anyone can write anything there.
I myself have not written anything there, although I did once delete some stuff that seemed way bad.
Steve
--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
Bas Spitters
Nov 30, 2014, 9:15:42 AM11/30/14
to Steve Awodey, Vladimir Voevodsky, homotopytypetheory
There is this carefully written text at the back of the book.
Perhaps it can be of use in writing the text in wikipedia:
---
Homotopy type theory is a new branch of mathematics that combines
aspects of several
different fields in a surprising way. It is based on a recently
discovered connection be-
tween homotopy theory and type theory. It touches on topics as
seemingly distant as the
homotopy groups of spheres, the algorithms for type checking, and the
definition of
weak ∞-groupoids.
Homotopy type theory brings new ideas into the very foundation of
mathematics. On
the one hand, there is Voevodsky’s subtle and beautiful univalence
axiom. The univalence
axiom implies, in particular, that isomorphic structures can be
identified, a principle that
mathematicians have been happily using on workdays, despite its
incompatibility with
the “official” doctrines of conventional foundations. On the other
hand, we have higher
inductive types, which provide direct, logical descriptions of some of
the basic spaces
and constructions of homotopy theory: spheres, cylinders, truncations,
localizations,
etc. Both ideas are impossible to capture directly in classical
set-theoretic foundations,
but when combined in homotopy type theory, they permit an entirely new
kind of “logic
of homotopy types”.
This suggests a new conception of foundations of mathematics, with
intrinsic homotopi-
cal content, an “invariant” conception of the objects of mathematics —
and convenient
machine implementations, which can serve as a practical aid to the
working mathemati-
cian. This is the Univalent Foundations program.
The present book is intended as a first systematic exposition of the
basics of univalent
foundations, and a collection of examples of this new style of
reasoning — but without
requiring the reader to know or learn any formal logic, or to use any
computer proof
assistant. We believe that univalent foundations will eventually
become a viable alter-
native to set theory as the “implicit foundation” for the unformalized
mathematics done
by most mathematicians.
---
Perhaps it can be of use in writing the text in wikipedia:
---
Homotopy type theory is a new branch of mathematics that combines
aspects of several
different fields in a surprising way. It is based on a recently
discovered connection be-
tween homotopy theory and type theory. It touches on topics as
seemingly distant as the
homotopy groups of spheres, the algorithms for type checking, and the
definition of
weak ∞-groupoids.
Homotopy type theory brings new ideas into the very foundation of
mathematics. On
the one hand, there is Voevodsky’s subtle and beautiful univalence
axiom. The univalence
axiom implies, in particular, that isomorphic structures can be
identified, a principle that
mathematicians have been happily using on workdays, despite its
incompatibility with
the “official” doctrines of conventional foundations. On the other
hand, we have higher
inductive types, which provide direct, logical descriptions of some of
the basic spaces
and constructions of homotopy theory: spheres, cylinders, truncations,
localizations,
etc. Both ideas are impossible to capture directly in classical
set-theoretic foundations,
but when combined in homotopy type theory, they permit an entirely new
kind of “logic
of homotopy types”.
This suggests a new conception of foundations of mathematics, with
intrinsic homotopi-
cal content, an “invariant” conception of the objects of mathematics —
and convenient
machine implementations, which can serve as a practical aid to the
working mathemati-
cian. This is the Univalent Foundations program.
The present book is intended as a first systematic exposition of the
basics of univalent
foundations, and a collection of examples of this new style of
reasoning — but without
requiring the reader to know or learn any formal logic, or to use any
computer proof
assistant. We believe that univalent foundations will eventually
become a viable alter-
native to set theory as the “implicit foundation” for the unformalized
mathematics done
by most mathematicians.
---
Reply all
Reply to author
Forward
0 new messages