The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Dear all,

Many of you already know it: one week ago, something terribly sad
happened: Vladimir Voevodsky, Fields medalist and key initiator of the
Homotopy Type Theory foundation of mathematics passed away at the age
of 51 [1].

His visionary belief in the foundational impact of the
types-as-spaces, equality-as-path correspondence [2][3], his
Univalence Axiom, and his reconstruction of propositions and sets from
a general notion of homotopy levels contributed to provide a new
foundational look at type theory, at equality, at extensionality, and
at mathematics in general. His vision and driving force contributed to
connect communities of mathematicians, logicians, and computer
scientists. The various events he co-organized or participated in over
the last years fostered a large corpus of new results encompassing the
backgrounds of researchers from these communities: higher inductive
types, so natural for representing quotients types or for representing
the algebraic essence of geometric structures; cubical type theory for
both another view at equality based on abstracting over a dimension
and for providing a computational content to univalence; and many
other ideas and connections who cross-benefited to the fields above.

Vladimir Voevodsky discovered Coq in the mid-late 2000. About it, he
said: "I started playing with Coq while thinking about the model in
Coq of homotopy types and I started to discover that I can do all
kinds of things which I was working before without having any
foundational investment so to speak and then I came up and I said `ok,
here we have a new foundation of mathematics', we can dispose of that
theory as a foundational system and do everything in this new
foundation" [4].

In Coq, he started the Univalent Foundations formalization [5] about
which a school and a workshop is going to be held in December 2017 [6].
The initial version of the Univalent Foundations formalization itself
stimulated the development of libraries for Homotopy Type Theory
(HoTT) in Coq [7], Agda [8] and Lean [9].

Homotopy Type Theory is at the core of the work of various research
teams world-wide. For instance, one of them directly involved in the
development of Coq is the Coq-HoTT project [10] which in particular
investigates among others the meta-theory and implementation of
definitional proof-irrelevance and higher inductive types in the
context of Coq.

Digressing about higher inductive types, I cannot resist at including
one of the first e-mails that Vladimir sent on coq-club, almost
exactly 8 years ago, witnessing his typical ingenuous-looking attempts
at expressing essential concepts in the context of Coq (see [11] for
the full thread):
<<
Is there a way in Coq to make definitions such as:

Inductive I1 : Type := x0 : I1 | x1 : I1 | i : eq x0 x1 .

 or

Inductive Impl : Type := P1: Prop | P2: Prop | impl: P1 -> P2 .

?

V.
>>

More practically, Vladimir Voevodsky also said about using Coq: "I
have a lot of wishes in terms of getting this proof assistant to work
better, but at least I don’t have to go home and worry about having
made a mistake in my work" [2].

There is indeed a long and wide road ahead for proof assistants. Let's
continue implementing our intuitions and dreams: a revolution is on
the march at the frontier of computer science, logic, and mathematics,
and Vladimir's spirit and endearingly fresh mindset will continue to
accompany us.

[1] https://www.ias.edu/news/2017/vladimir-voevodsky
[2] The Origins and Motivations of Univalent Foundations,
    https://www.ias.edu/ideas/2014/voevodsky-origins
[3] 
http://smf4.emath.fr/Publications/Gazette/2014/142/smf_gazette_142_87-94.pdf 
(p.91)
[4] http://icm2014seoul.over-blog.com/videos-en-preambule.html (28'45")
[5] https://github.com/UniMath/UniMath
[6] https://unimath.github.io/bham2017
[7] https://github.com/HoTT/HoTT
[8] https://github.com/HoTT/HoTT-Agda
[9] https://github.com/leanprover/lean/wiki/HoTT-Library
[10] http://coqhott.gforge.inria.fr/
[11] https://sympa.inria.fr/sympa/arc/coq-club/2009-10/msg00025.html