newbie questions about homotopy theory & advantage of UF/Coq

[ric...@math.northwestern.edu]

Hi, I'm a homotopy theorist and a HOL Light programmer and I'm really excited by Vladimir's leadership in the formal proofs world.  But I'm having a lot of trouble understanding the HoTT book.  Can we go through this recent popular article?  It sounds really great:
http://blogs.scientificamerican.com/guest-blog/2013/10/01/voevodskys-mathematical-revolution/

   [Coq] was based on something called Martin-Löf type theory, and he
   just couldn’t get his head around it.[...] He realized that all
   this type theory stuff could be translated to be equivalent to
   homotopy theory,

I would really like to understand that!  I apologize if this is clearly explained in the HoTT book.  Maybe that's all anyone has to explain to me right now, and my questions below can wait.

   “Set-theoretic approach to foundations of mathematics work well
   until one starts to think about categories since categories cannot
   be properly considered as sets with structures due to the required
   invariance of categorical constructions with respect to
   equivalences rather than isomorphisms of categories.”

OK, I see that Vladimir's Univalence Axiom is coming in here to provide the invariance.  But if UF/Coq only good for category theory?  I would hope that UF/Coq was more useful than that.  I can think of a lot of ways that HOL Light makes it hard to formalize pure math, but these problems don't (I think???) have much to do with category theory.  Rob Arthan, a stable homotopy theorist and HOL programmer told me that the stirring intro to Andrew's Type Theory is overselling the case, that HOL is better than ZFC in formalizing math, but it's far from perfect.

   Rapidly, he figured out that every proof system but one was
   inadequate for what he had in mind. And that last one — Coq — he
   couldn’t understand.

Why is that?  The only advantage that I know that Coq has over HOL Light is type quantification, which you need to define things with universal properties, like fibration. 

   Essentially, you have to give [your proof assistant] the same
   education you got — except that you have to do it in a far more
   exacting way.

Sure, I've done plenty of that in HOL Light (see
http://www.math.northwestern.edu/~richter/RichterHilbertAxiomGeometry.tar.gz
which is a bit more recent than the version in the HOL Light distribution) and seen others do a lot more, e.g. John Harrison has 19,000 lines in topology.ml in a directory Multivariate that's 8,452 KB. 

   But this approach circumvents all that labor.

I can't imagine how, unless lots of UF/Coq people have already done the labor. 

   Not only that, but the language the computer understands is far
   closer to natural mathematical language.

Sure, and any type theory would be, but what I really want to learn is how UF/Coq is closer to natural mathematical language than HOL.  Let me crudely describe an enduring headache in HOL.  Our sets are either types or "subsets" of types, and you can make function types alpha->beta for types alpha & beta, but given sets A & B, there is no type A->B, so you have define your function from A to B on the whole type, and that causes trouble.  Is this problem fixed in Coq with dependent types, or in UF somehow?  John Harrison quotes Bob Solovay as saying that Coq's dependent types are too hard for mortals to understand.  Do Coq's dependent types become usable if we're also using UF?

   In fact, Voevodsky says, it’s a bit like playing a video game. You
   interact with the computer. “You tell the computer, try this, and
   it tries it, and it gives you back the result of its actions,”
   Voevodsky says. “Sometimes it’s unexpected what comes out of
   it. It’s fun.”

That's true for any proof assistant, and I've spent lots of time playing this video game, and part of the game is that I don't really understand the difference between REWRITE_TAC, SIMP_TAC, MESON_TAC and MP_TAC.  I have a "feel" for the difference from many hours playing the video game.  Is there something about UF/Coq that makes these automated provers more usable, powerful, or describable?

   He also predicts that this will lead to a blossoming of
   collaboration, pointing out that right now, collaboration requires
   an enormous trust, because it’s too much work to carefully check
   your collaborator’s work. With computer verification, the computer
   does all that for you, so you can collaborate with anyone and know
   that what they produce is solid. That creates the possibility of
   mathematicians doing large-scale collaborative projects that have
   been impractical until now.

This sounds great, and also Vladimir's hope/prediction in Wired that we'll soon formalize our paper before submitting them, but I think there's a somewhat different advantage of proof assistants.  I think math is really about proofs that humans can understand, and that human mathematicians take great joy in understanding such proofs.  I think it's quite easy in the modern pure math world for folks to not really prove their theorem, there's so much pressure to publish, or show our cutting edge fields are growth industries that can attract talented workers.  I'm not going to say that's bad, but I think that way you lose some the joy of really understanding the proofs.  I'm hoping that our proof assistants will restore this joy that we've maybe lost some of.  Partly with that in mind, I've worked pretty hard to write readable code, starting with Freek W's miz3.ml, which I generalized to readable.ml.  John H is a big proponent of readable code, and he makes fun of the usual HOL Light coding as EAR_OF_BAT_TAC.  Do you think that Coq/UF is particularly readable code, or have you made good advances in readability? 

--
Best,
Bill

[Michael Shulman]

Keep in mind that popular science articles are generally written by journalists, not scientists, and hence are liable to contain inaccuracies and exaggerated claims. A better introduction for a mathematician is Awodey's survey paper:
http://www.andrew.cmu.edu/user/awodey/preprints/TTH.pdf
or the HoTT book. If you can bring up specific things in the book that are causing you difficulty, people might be able to help explain.

--
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/groups/opt_out.

[Gershom Bazerman]

On 1/1/14, 12:03 AM, ric...@math.northwestern.edu wrote:
>
> Why is that? The only advantage that I know that Coq has over HOL
> Light is type quantification, which you need to define things with
> universal properties, like fibration.

I'm writing as a relative novice (though I do help organize the NYC HoTT
reading group), so hesitant to weigh in. However, it seems to me that
the questions you present are A) unfortunately based on a popularization
of the work, and B) relate to bigger questions about the relationship of
proof assistants in different families (the HOL family vs. the
Martin-L�f derived family including both Coq and Agda), and questions in
particular relating not just to "usability" but to the nature of their
approach and foundations. So I'd like to try to explain what I find
compelling about HoTT and what the point seems to be to me, at least.
The decent points in what you'll find below are probably all better and
more clearly presented in the introduction to the HoTT book. The rotten
points are my fault entirely.

One useful reference may be another popularization, but one from "the
horse's mouth" so to speak, which is Voevodsky's lecture at the
Heidelberg Laureate forum, which I found gave a more serious summary of
his aims:

http://www.heidelberg-laureate-forum.org/blog/video/lecture-thursday-september-26-vladimir-voevodsky/

But beyond that, I think that it is worth examining what Martin-L�f was
up to in the first place in deriving his intuitionistic type theory. His
lectures on the meaning of logical constants are very rich and I've
reviewed them many times:

http://www.ae-info.org/attach/User/Martin-L%C3%B6f_Per/OtherInformation/article.pdf

What HOL-derived systems give us are exactly what it "says on the box"
-- attempts to automate and formalize traditional proofs in which we can
then define the whole of traditional mathematics.

The intuitionistic type theory project has been different from the start
-- an attempt to provide _foundations_ for mathematics, of which
automated proof systems then became a logical outgrowth. HOL exists
because we have programmed it. Martin-L�f type theory exists prior to
and absent any particular implementations of theorem provers based on
it. These foundations were, as originally conceived, perhaps not to be
of mathematics as we had traditionally practiced it, but rather
mathematics on a constructivist basis, which might mean changing the
mathematics themselves as we went along.

With all due hand-waving, MLTT does not give a "partitioned" system
where on the one hand we have a logical meta-system which we use to
reason about mathematical objects "external" to it, but rather a
"unitary" or "monist" system in which everything we construct is at once
a type/term/proof/mathematical object. Thus we do not build a system to
reason about mathematics, but rather we have a mathematical system that
(we hope) itself already contains (or contains the potential for) all of
mathematics, have we the wit to express it.

That's already the (or at least "a") intuitionist project, as I see it,
well prior to the introduction of Homotopy Type Theory.

What HoTT itself now brings to the table is the remarkable coincidence
(of course nothing in math is 'just' a coincidence) that under the
proper interpretation, we can also treat intuitionistic types as
_spaces_ and so a (or perhaps "the") natural setting for understanding
type theory is itself topology, and conversely a (perhaps "the") natural
formalization of homotopy theory should be in type theoretic language.
So by chapter 2 of the HoTT book, we can, using purely pen-and-paper
methods, use MLTT to encode a value that gives witness to
Eckmann-Hilton. We do not do this by defining objects to "represent"
loop spaces, then encoding facts about such objects, then using the
rules of our system to chain these facts together. Rather, we do this by
recognizing that we _already_ have a representation of loop spaces given
by MLTT, in the form of equality types at given points, and that the
"facts" about these spaces are provided by the rules MLTT already gives
us for working with such types!

From the above "coincidence" there have now been derived extensions to
MLTT (such as the univalence axiom and higher inductive types). There
has also been introduced a way to _truncate_ our infinity groupoid of
types and recover not only intuitionistic, but classical mathematics!
This latter was quite a revelation for me.

If what you want is a better proof assistant, then Coq, Isabelle, Twelf,
Agda, etc. are all perhaps more suited for some purposes and less so for
others. There are matters of tooling and taste involved.

The work on HoTT is rather about mathematics (and type theory, and
logic, and programming -- after all, they're all the same thing!), and
an attempt to formulate it "internally." Ultimately one would hope this
will lead to better proof assistants and easier proofs. There are
already some proofs (such as the above mentioned Eckmann-Hilton) that
are clearly elegant in this framework. With time, I would hope there
will be many others.

On the "tactics" question, note that Agda doesn't really have tactics at
the moment. Rather it encourages setting up everything "just right" to
begin with. Since Agda also is based in MLTT, a great deal of the HoTT
work has been translated to Agda as well. You may find reviewing the
repository along with the book a worthwhile experience.

Cheers,
Gershom

[Bas Spitters]

In addition to what has been said:

1. UF will provide us with a semantic understanding of inductive types.

A lot has already been done, see for instance the papers by Voevodsky and by Awodey, Gambino and Sojakova.

2. Roughly, hSets in HoTT now provide a model intuitionistic HOL. This should make it easier to import proofs from the HOL family.
3. > Rob Arthan, a stable homotopy theorist and HOL programmer told me that the stirring intro to Andrew's Type Theory is overselling the case, that HOL is better than ZFC in formalizing math, but it's far from perfect.

Which introduction are you referring to? What were Rob Arthan's arguments?

[Michael Shulman]

On Wed, Jan 1, 2014 at 6:02 AM, Bas Spitters <b.a.w.s...@gmail.com> wrote:
> 1. UF will provide us with a semantic understanding of inductive types.
> A lot has already been done, see for instance the papers by Voevodsky and by
> Awodey, Gambino and Sojakova.

I don't see how this is a selling point of HoTT to someone not already
familiar with it, since we already had a set-theoretic semantic
understanding of inductive types. What exactly do you mean?

[Vladimir Voevodsky]

Hi Bill,

my I ask you please to be careful with statements such as

I I'm really excited by Vladimir's leadership in the formal proofs world.

There are many people involved in the univalent foundations project now and some of them are exploring directions which I did not do any work on and which I would not claim a leadership position in. Some have moved well beyond the ideas which I have introduced (i.e. Thierry Coquand and his group in their work on the cubical sets model). While a do consider myself to be the founder of the univalent foundations project and will probably retain one of the leading roles in it for a while it is incorrect to consider me to be *the* leader of the project (leave alone of the formal proofs world as whole). 

Let me crudely describe an enduring headache in HOL.  Our sets are either types or "subsets" of types, and you can make function types alpha->beta for types alpha & beta, but given sets A & B, there is no type A->B, so you have define your function from A to B on the whole type, and that causes trouble.  Is this problem fixed in Coq with dependent types, or in UF somehow? 

Yes, definitely it is fixed in UF. In UF every set is a type (but not every type is a set). 

John Harrison quotes Bob Solovay as saying that Coq's dependent types are too hard for mortals to understand.  Do Coq's dependent types become usable if we're also using UF? 

Yes. That's precisely what I have mentioned in the interview - that I could not understand Coq until I have invented the univalent model. With this model in mind the type theory of Coq becomes intuitive (except for some "details" such as a baroque universe management or weird rules for general fix point definitions but those can be simply avoided as it is done in Foundations library).

Is there something about UF/Coq that makes these automated provers more usable, powerful, or describable? 

Which automated provers?

Do you think that Coq/UF is particularly readable code, or have you made good advances in readability?  

There are various opinions on this. I find Coq used in the style of my Foundations library (with very little automation) to be quite readable especially when one can follow the code line-by-line in something like Proof General or CoqIDE. One of the things I plan to do today is to continue reading the RezkCompletion library written by others and I am looking forward to it as to something which is easier and more fun than reading a usual math paper. 

Vladimir.

 

On Jan 1, 2014, at 12:03 AM, ric...@math.northwestern.edu wrote:

Hi, I'm a homotopy theorist and a HOL Light programmer and   But I'm having a lot of trouble understanding the HoTT book.  Can we go through this recent popular article?  It sounds really great:

[Vladimir Voevodsky]

On Jan 1, 2014, at 3:38 AM, Gershom Bazerman wrote:

From the above "coincidence" there have now been derived extensions to MLTT (such as the univalence axiom and higher inductive types). There has also been introduced a way to _truncate_ our infinity groupoid of types and recover not only intuitionistic, but classical mathematics! This latter was quite a revelation for me.

There seems to be a lot of confusion around the issue of classical mathematics in UF. The ability to encode classical mathematics using UF has nothing to do with truncations. It requires (for proper formulation of the law of excluded middle) to have the notion of h-levels (which can be defined using basic MLTT) but it does not require truncations. 

V.

[Bas Spitters]

I was thinking about the recent bug in Coq's implementation:

--- Vladimir's variant ---

Variable Heq : (False -> False) = True.

Fixpoint contradiction (u : True) : False :=

contradiction (

match Heq in (_ = T) return T with

| eq_refl => fun f:False => match f with end

end

).

Definition c : False := contradiction ( I ) .
---

And the difficulties with the set-theoretic encoding of Coq's Prop:
E.g.
http://www.lix.polytechnique.fr/~werner/publis/cc.pdf

IIRC this was what Solovay was wondering about, but I may be mistaken.

[Michael Shulman]

On Wed, Jan 1, 2014 at 8:47 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> There seems to be a lot of confusion around the issue of classical
> mathematics in UF. The ability to encode classical mathematics using UF has
> nothing to do with truncations. It requires (for proper formulation of the
> law of excluded middle) to have the notion of h-levels (which can be defined
> using basic MLTT) but it does not require truncations.

However, although hsets and hpropositions (being hlevels 0 and -1) can
be *defined* in unaltered MLTT, they do not yet give classical
mathematics, since there is no way to construct things such as
quotients and hpropsitional disjunction. Truncations are a natural
way to obtain those things, although there are others.

[Kevin Watkins]

Since I haven't seen it mentioned yet: the reference to "UF/Coq" in the title of the original question looks a bit strange to me.  Coq is a tool that has been used to develop some aspects of UF formally, but it's not the only one.  You aren't obligated to buy into Coq if you want to do UF.

[Bill Richter]

Thanks, Vladimir, and thanks to everyone else who responded.

Yes. That's precisely what I have mentioned in the interview - that
I could not understand Coq until I have invented the univalent
model. With this model in mind the type theory of Coq becomes

intuitive [...] Yes, definitely it is fixed in UF. In UF every set

is a type (but not every type is a set).

I'm really happy to hear this. So homotopy theory fixes the problem Bob Solovay noted with Coq. So I need to learn how homotopy theory makes Coq intuitive. Do you think the HoTT book the best source for this, or Steve's paper? http://www.andrew.cmu.edu/user/awodey/preprints/TTH.pdf
I haven't had much luck with either paper, but I haven't tried very hard.

(except for some "details" such as a baroque universe management or
weird rules for general fix point definitions but those can be
simply avoided as it is done in Foundations library).

Excellent, I don't need to know this now, but I'll keep it mind.

it is incorrect to consider me to be *the* leader of the project
(leave alone of the formal proofs world as whole)

I apologize for my carelessness. I didn't mean to slight your coworkers. What I meant is that it's fantastic that a top-rated mathematician like you has taken such a public interest in formal proofs, being written up in Wired and Time. So of course I now need to learn about your work, and the work of everyone else in the UF project.

> Is there something about UF/Coq that makes these automated

> provers more usable, powerful, or describable?=20

Which automated provers?

Sorry for being unclear. Automated provers is probably the wrong term. I was referring to the HOL Light "automated provers" REWRITE_TAC, SIMP_TAC, MESON_TAC and MP_TAC. I know something about what they do, and from many happy hours spent playing the video game, I I have a "feel" for the difference between them. But I don't know exactly. I've been told that other HOLs (e.g. HOL4) are different. Here are some vague thoughts:

MESON_TAC will prove first order logic results "automatically", but it's not supposed to be good at equational reasoning. So for many FOL tasks (I think working under quantifiers) you have to use REWRITE_TAC, which in a sense just blindly substitutes. REWRITE_TAC usually performs more rewriting than ONCE_REWRITE_TAC, but I've written code where ONCE_REWRITE_TAC worked and REWRITE_TAC. SIMP_TAC is a much more powerful version of REWRITE_TAC, sort of a combination of REWRITE_TAC and MESON_TAC. However I've been surprised recently that MESON_TAC will prove things for me that SIMP_TAC won't. My question was: Is there something about UF/Coq that makes these "automated provers" more usable, powerful, or describable?

Just to clarify, let me give a simple example of what I mean, from HilbertAxiom_read.ml from
http://www.math.northwestern.edu/~richter/RichterHilbertAxiomGeometry.tar.gz
partly to bring up code readability, as that's something else I wanted to discuss.
fol = MESON_TAC, simplify = SIMP_TAC

let SegmentSubtraction = theorem `;
∀ A B C A' B' C'. B ∈ Open (A,C) ∧ B' ∈ Open (A',C') ⇒
seg A B ≡ seg A' B' ⇒ seg A C ≡ seg A' C'
⇒ seg B C ≡ seg B' C'

proof
intro_TAC ∀ A B C A' B' C', H1, H2, H3;
¬(A = B) ∧ ¬(A = C) ∧ Collinear A B C ∧ Segment (seg A' C') ∧ Segment (seg B' C') [Distinct] by fol H1 B1' SEGMENT;
consider Q such that
B ∈ Open (A,Q) ∧ seg B Q ≡ seg B' C' [defQ] by fol - C1OppositeRay;
seg A Q ≡ seg A' C' [AQ_A'C'] by fol H1 H2 - C3;
¬(A = Q) ∧ Collinear A B Q ∧ A ∉ Open (C,B) ∧ A ∉ Open (Q,B) []
proof simplify defQ B1' ∉; fol defQ B1' H1 B3'; qed;
C ∈ ray A B ━ {A} ∧ Q ∈ ray A B ━ {A} [] by fol Distinct - IN_Ray IN_DIFF IN_SING;
C = Q [] by fol Distinct - AQ_A'C' H3 C1;
fol defQ -;
qed;
`;;

The point is that we could write down proofs of the various steps, but I don't have to, but MESON_TAC and SIMP_TAC will "automatically" create proofs using the list results they're given. I assume there's a lot of this "automation" going on in Coq.

I find Coq used in the style of my Foundations library (with very
little automation) to be quite readable especially when one can
follow the code line-by-line in something like Proof General or
CoqIDE.

That's really great.

One of the things I plan to do today is to continue reading the
RezkCompletion library written by others and I am looking forward
to it as to something which is easier and more fun than reading a
usual math paper.

I'm happy to hear that Charles's work is getting coded up. Let me quickly respond to everyone else, and thanks again to them for graciously responding to me.

Gershom, I'll look at Martin-Löf's paper and read the rest of your interesting post
http://www.ae-info.org/attach/User/Martin-L%C3%B6f_Per/OtherInformation/article.pdf

Bas, I was referring to the preface of Peter Andrews's book To Truth Through Proof:

PA> Both type theory (otherwise known as HOL) and axiomatic set theory
PA> [ZC/FOL] can be used [to formalize math], and it is really an
PA> accident of intellectual history that at present mostly logicians
PA> and mathematicians are more familiar with axiomatic set theory
PA> than with type theory. It is hoped that this book will help
PA> remedy this situation. [... experts recognize that HOL is better
PA> than ZC/FOL] for formalizing what mathematicians actually do.

Rob Arthan explained to me that HOL was better than ZC/FOL but it wasn't good enough. The only argument Rob actually made is that HOL Light and most HOLs don't have Coq's type quantification which you need to define universal properties like fibration. I can think of other problems. Sets are represented in HOL by terms of type
alpha->bool
we're supposed to say that a subset of alpha is the same thing as a function alpha->bool. But they're not the same thing, and I keep wondering when this is going to cause a problem.

KW> You aren't obligated to buy into Coq if you want to do UF.

Kevin, that's pretty interesting. Could one build UF on top of HOL Light? I would think not, but it would be cool if you could. Perhaps you mean that UF is math rather than code?

--
Best,
Bill

[Vladimir Voevodsky]

On Jan 2, 2014, at 11:44 AM, Bill Richter wrote:

> I'm really happy to hear this. So homotopy theory fixes the problem Bob Solovay noted with Coq. So I need to learn how homotopy theory makes Coq intuitive. Do you think the HoTT book the best source for this, or Steve's paper? http://www.andrew.cmu.edu/user/awodey/preprints/TTH.pdf
> I haven't had much luck with either paper, but I haven't tried very hard.

Although it is definitely true that one can learn UF without learning Coq in your case I would strongly suggest that you install Coq and start a project of converting your HilbertAxiom stuff into Coq using univalent framework. I can help you with it by email. I think just going one line at a time over what you have done and translating it into UF-Coq will be much more efficient than having more general discussions.

Vladimir.

[Michael Shulman]

On Thu, Jan 2, 2014 at 8:44 AM, Bill Richter
<ric...@math.northwestern.edu> wrote:
> So homotopy theory fixes the problem Bob Solovay noted with Coq.

I would hesitate to proclaim this to the world before receiving
confirmation from Solovay himself. (-: It is true that homotopy type
theory has made dependent type theory easier to understand for many of
us mathematicians, although many of us were already familiar with
homotopy theory -- conversely, it may be the case that it has made
homotopy theory easier to understand for some dependent type
theorists. (-:

> Do you think the HoTT book the best source for this, or Steve's paper? http://www.andrew.cmu.edu/user/awodey/preprints/TTH.pdf

I suggest trying both, and asking for help whenever you get stuck. We
are still learning how to explain HoTT to newcomers, and it's
difficult because everyone comes in with a different background and
assumptions. Your feedback may help us improve the exposition for
other people coming from the HOL world.

Note, however, that neither are aimed at people interested in computer
formalization. As Vladimir says, if that's your main goal, then you
might be well-served by exploring the existing HoTT libraries
(http://homotopytypetheory.org/coq/) and trying to use it for a
project of your own.

> I find Coq used in the style of my Foundations library (with very
> little automation) to be quite readable especially when one can
> follow the code line-by-line in something like Proof General or
> CoqIDE.
>
> That's really great.

However, it is worth emphasizing that preferences differ. Others of
us working on the project find other styles of using Coq, such as that
used in the HoTT/HoTT library (which uses more automation), to be more
readable.

It's also not entirely clear to me how much the *readability* of Coq
code is influenced by HoTT specifically, versus other factors (such as
use of automation, typeclasses, etc.). One thing that we can say is
that various facts (such as homotopy-theoretic calculations) admit
different "synthetic" proofs by using HoTT which are much easier to
understand when formalized than a formalization of the usual
"classical" proof of the analogous fact would be. This is not really
comparing apples to apples, but it is still an advantage of HoTT for
the purposes of formalization.

> One of the things I plan to do today is to continue reading the
> RezkCompletion library written by others and I am looking forward
> to it as to something which is easier and more fun than reading a
> usual math paper.
>
> I'm happy to hear that Charles's work is getting coded up.

Just to clarify: RezkCompletion is not about Charles Rezk's work; we
just named the "Rezk completion" after him because it's inspired by
his notion of complete Segal space from homotopy theory.

> Sets are represented in HOL by terms of type
> alpha->bool
> we're supposed to say that a subset of alpha is the same thing as a function alpha->bool. But they're not the same thing, and I keep wondering when this
is going to cause a problem.

This has to do more with the difference between "material" and
"structural" sets than it does with HOL or HoTT.

Structural sets are the ones used in practice by most mathematicans;
they are just a collection of featureless "points" on which we can
impose structure (such as a group, a topological space, etc.). It
doesn't make sense to ask whether one abstractly given structural set
is a subset of another one.

Material sets are specified as subcollections of some pre-existing
collection of objects with definite identity (such as an ambient
structural set). The "sets" of ZFC are material, and one has to mimic
structural sets by forgetting about the internal identities of their
elements. However, there are other axiomatic set theories (such as
ETCS) whose basic "sets" are structural, and in which one can find
material sets as subsets of these.

Type theory in this regard is more like ETCS. The "types which are
sets" that Vladimir mentioned are structural sets, not material ones;
while subsets of those can be treated as material sets. In any case,
a subset of a structural set X can always be identified with its
characteristic function X -> prop (where prop may or may not be bool,
depending on whether you assume LEM), and this never causes any
problems.

> KW> You aren't obligated to buy into Coq if you want to do UF.
>
> Kevin, that's pretty interesting. Could one build UF on top of HOL Light? I would think not, but it would be cool if you could. Perhaps you mean that UF is math rather than code?

UF/HoTT *is* math rather than code, but furthermore it can be
formalized in any proof assistant which supports intensional dependent
type theory. This does not, I believe, include HOL, but in addition
to Coq, a lot of formalization of UF/HoTT has also been done in Agda.

Mike

[Bill Richter]

start a project of converting your HilbertAxiom stuff into Coq
using univalent framework. I can help you with it by email.

Thanks, Vladimir! I'll do it. I'm grateful to you for your help. I starting installing Coq. I also downloaded Foundations-master.zip from https://github.com/vladimirias/Foundations.

But I think my real problem is the homotopy theory. As a homotopy theorist, I'm practically from the 1960s: Toda's book, the classical Adams spectral sequence and Poincare complexes, although I can do model categories. I'm guessing from Michael's web page http://home.sandiego.edu/~shulman/papers/index.html or Steve Awodey's paper that HoTT is using a very different kind of homotopy theory. I don't know anything about your homotopy theory for schemes, étale cohomology, or your Fields medal solution of the Milnor conjecture. Can you recommend some homotopy theory that I need to learn in order to see the connection with Martin-Lof type theory? Can I understand your homotopy theory/Martin-Lof type theory connection with only my 1960s skills?

This is way off-topic, but since Coq uses ocaml, maybe somebody knows the answer. I have a HOL Light file readable.ml that's a "parser" that turns strings into tactics proofs, and it's based on some ocaml code

let exec = ignore o Toploop.execute_phrase false Format.std_formatter
o !Toploop.parse_toplevel_phrase o Lexing.from_string;;

that I believe folks on the ocaml newgroup said I shouldn't be using. They definitely said don't use Obj.magic. Is there some way to do my "parsing" with camlp? Here's a real dumb question: The basic Scheme exercise is to write a Scheme interpreter inside Scheme. That's easy because Scheme has a quote feature. Is it possible, or easy, to perform this exercise in ocaml? Write an ocaml interpreter inside ocaml? Do you need camlp for that?

--
Best,
Bill

[Bas Spitters]

A possibility would be to help formalize the book, or make the exercises:

https://github.com/HoTT/HoTT/blob/master/contrib/HoTTBook.v
https://github.com/HoTT/HoTT/blob/master/contrib/HoTTBookExercises.v

[Thomas Streicher]

> Thanks, Vladimir, and thanks to everyone else who responded.
> Yes. That's precisely what I have mentioned in the interview - that
> I could not understand Coq until I have invented the univalent
> model. With this model in mind the type theory of Coq becomes
> intuitive [...] Yes, definitely it is fixed in UF. In UF every set
> is a type (but not every type is a set).

There is no reason not to believe Vladimir that HIS way of
understanding type theory was via homotopy theory. But that seems to
be a very individual feature :-)

Type theory is by now almost 45 years old and I think most people have
understood it via its naive set theoretic semantics which you find
e.g. in Martin-Loef's Bibliopolis book or in the books by Beeson and
Troelstra & van Dalen just to refer to the most accessible sources.
Since Bob Seely (and others I guess) in the 1980s observed that the
semantics of extensional type theory is given by locally cartesian
closed categories it was clear that every elementary topos with a
natural numbers object gives rise to a model of type theory.
Interpreting Prop as \Omega of the topos gives also rise to a model of
the calculus of constructions, albeit a proof irrelevant one.

Around 1995 it was observed that there are proof relevant models of
CoC where Prop is interpreted as the collection of partial equivalence
relations on a partial combinatory algebra (e.g. natural numbers with
Kleene application). I learnt this from a talk by Martin Hyland in 1985
who attributed this to Eugenio Moggi, at least for the case of polymorphic
lambda calculus. But the extension to CoC is sort of immediate and was
observed by many people including myself (in my Thesis and the subsequent
book).

In my Habil Thesis I gave a model of intensional type theory using the
glueing (or "sconing") of realizability models. But this still validated
uniqueness of identity proofs (actually, my eliminator K). To overcome
this Martin Hofmann and I introduced the groupoid model which was the first
model of univalence. We certainly didn't have the univalence axiom but
we observed that propositional equality coincided with being isomorphic
(actually, this was the motivation for looking at groupoids at all).
The simplicial sets model is doubtlessly much more nontrivial.
But it contains the naive set-theoretic model as a submodel and thus
is fairly classical since you don't get outside it as long as you
don't consider universes!

I think that simplicial sets and alike are good for modeling "equality
as isomorphism". This is compatible with type theory but not with set
theory or topos theory (with its built in proof irrelevance!). However,
the simplicial set model doesn't account for the constructivity features
of type theory which are much better captured by the above mentioned
realizability models.

This summer I speculated about building the groupoid model in type theory.
In discussion with Steve Awodey it got clear to me that one needs
function extensionality for this purpose. So one can construct the
groupoid model inside realizability models of extensional type theory
but not in intensional type theory itself. Not very surprising after all
since we know that Univalence entails Function Extensionality.
If you want to read more about this latter aspect you may read
http://www.mathematik.tu-darmstadt.de/~streicher/Barcelona_abstract.pdf.

In any case I don't think that homotopy models are the only way to
understand type theory though they seem to be the canonical way for
realizing "equality of types as isomorphism".

Thomas

[Altenkirch Thorsten]

On 04/01/2014 11:33, "Thomas Streicher"

<stre...@mathematik.tu-darmstadt.de> wrote:

>> Thanks, Vladimir, and thanks to everyone else who responded.
>> Yes. That's precisely what I have mentioned in the interview - that
>> I could not understand Coq until I have invented the univalent
>> model. With this model in mind the type theory of Coq becomes
>> intuitive [...] Yes, definitely it is fixed in UF. In UF every set
>> is a type (but not every type is a set).
>
>There is no reason not to believe Vladimir that HIS way of
>understanding type theory was via homotopy theory. But that seems to
>be a very individual feature :-)

Indeed, I agree. Personally, I have a much better understanding of Type
Theory than Homotopy Theory. Actually for me it rather works the other way
around: the encoding of Homotopy Theory in Type Theory gives me some idea
what Homotopy Theory is about.

>Type theory is by now almost 45 years old and I think most people have
>understood it via its naive set theoretic semantics which you find

What is the "naïve set theoretic semantics"? Set theory seems to be a dead
end, the idea that all mathematical concepts can be modelled by properties
of some sort of trees seems rather alien and arbitrary to me. As a
computer scientist with a particular fondness for typed functional
programming a "naïve type theoretic semantics" seems much more natural.
And indeed, its primitive concepts are functions, records and enumerations
which have a very direct understanding in how you use them when writing
programs.

The higher-dimensional features of Homotopy Type Theory arise naturally in
such an understanding. The question is how to we model the type of
equalities. While as a first approximation we may think that there is at
most one equality proof this view doesn't hold after a closer inspection.
In particular we don't want to model equality of types as the equality of
their names but by an extensional equivalence with some natural
properties. Hence, I think that what is called homotopy type theory can
arise just from a naïve type theoretic semantics and the fact that this
corresponds to notions in Homotopy Theory is an interesting coincidence.

As a consequence I think that the name "Homotopy Type Theory" is a bit of
a misnomer because it emphasize one particular approach to Type Theory. I
think Higher Dimensional Type Theory would be better.

>I think that simplicial sets and alike are good for modeling "equality
>as isomorphism". This is compatible with type theory but not with set
>theory or topos theory (with its built in proof irrelevance!). However,
>the simplicial set model doesn't account for the constructivity features
>of type theory which are much better captured by the above mentioned
>realizability models.

It seems that Thierry is claiming that cubical sets are better suited for
this. I still have to digest the paper...

>
>This summer I speculated about building the groupoid model in type theory.
>In discussion with Steve Awodey it got clear to me that one needs
>function extensionality for this purpose. So one can construct the
>groupoid model inside realizability models of extensional type theory
>but not in intensional type theory itself. Not very surprising after all
>since we know that Univalence entails Function Extensionality.
>If you want to read more about this latter aspect you may read
>http://www.mathematik.tu-darmstadt.de/~streicher/Barcelona_abstract.pdf.
>
>In any case I don't think that homotopy models are the only way to
>understand type theory though they seem to be the canonical way for
>realizing "equality of types as isomorphism".

So farŠ

Thorsten


>
>Thomas

>
>--
>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/groups/opt_out.

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.

[Vladimir Voevodsky]

On Jan 4, 2014, at 12:08 AM, Bill Richter <ric...@math.northwestern.edu> wrote:

> start a project of converting your HilbertAxiom stuff into Coq
> using univalent framework. I can help you with it by email.
>
> Thanks, Vladimir! I'll do it. I'm grateful to you for your help. I starting installing Coq. I also downloaded Foundations-master.zip from https://github.com/vladimirias/Foundations.
>
> But I think my real problem is the homotopy theory. As a homotopy theorist, I'm practically from the 1960s: Toda's book, the classical Adams spectral sequence and Poincare complexes, although I can do model categories. I'm guessing from Michael's web page http://home.sandiego.edu/~shulman/papers/index.html or Steve Awodey's paper that HoTT is using a very different kind of homotopy theory. I don't know anything about your homotopy theory for schemes, étale cohomology, or your Fields medal solution of the Milnor conjecture. Can you recommend some homotopy theory that I need to learn in order to see the connection with Martin-Lof type theory? Can I understand your homotopy theory/Martin-Lof type theory connection with only my 1960s skills?

Yes, one definitely can. One does not need to know what a model category is in order to understand univalent semantics.

All you need is the usual homotopy category of topological spaces or, to be more precise and technical, of Kan simplicial sets. It is also good to know what an LCCC (Locally Cartesian Closed Category) is.

V.

[Martin Escardo]

On 04/01/14 11:33, Thomas Streicher wrote:
> There is no reason not to believe Vladimir that HIS way of
> understanding type theory was via homotopy theory. But that seems to
> be a very individual feature :-)

Thorsten gave his alternative way of seeing things.

Here is my own alternative understanding, which is not incompatible
with Thorsten's or Vladimir's, but doesn't come from the same
"intuitions" (intuition = all we know, digested in our own particular
way).

Understanding MLTT via set theory, while helpful in some respects, is
misleading, particularly when it comes to understanding when two types
are equal. We can't say that they are equal if they have the same
elements: there is no mode of expression in type theory available to
formulate this.

So, it is not that "having the same elements" is the wrong notion of
equality for types.

To say that two types are equal if they have the same elements is "not
even wrong": there is no way to say that in type theory.

So one would say (following algebra and category theory) that two
types are "equal" means, by definition, that they are isomorphic. But
then we find a problem: the notion of isomorphism in type theory is
proof relevant (i.e. not an hproposition).

Vladimir says "no problem". Work with equivalence, which is logically
equivalent to isomorphism, but proof-irrelevant. (Great insight.)

We then happily take equivalence to be our notion of type equality, by
definition. (Equivalance = proof-irrelevant MLTT formulation of
isomorphism, without any need to extend MLTT with any axioms to
formulate that.)

What is bold about the univalence axiom is not that is says (roughly)
that isomorphic types are equal. This would indeed be rather bold (and
false) in the set-theoretical understanding of MLTT.

What is bold about the univalence axiom is that it posits that the
type of equivalences satisfies Martin-Loef's J-induction principle.

It is at this stage that one can say that both the set-theoretical and
the computational intuitions of type theory fail to foresee the
univalence axiom.

What we learn from the consistency of the univalence axiom is that
Martin-Loef's inductive definition of equality, when applied to the
universe, fails to characterize type equality as understood in the
set-theoretical interpretation of types (i.e. having the same
elements). But this of course is not surprising.

What is surprising is that equivalence (in some models, such as Kan
simplicial sets and Kan cubical sets) satisfies the J induction
principle.

That is, what Martin-Loef intended to capture equality, actually
captures equivalence in some (mathematically interesting!) models.

From a public relations perspective, the slogan "univalence =
isomorphic types are equal" is rather misleading.

What is going on is that what MLTT defines as equality (identity
types) can be consistently modelled as equivalence.

What is more interesting, is that this actually is computationally
consistent, after the cubical-set model.

In summary, my view is that univalence gives an induction principle for
equivalence, rather than postulate that equality means isomorphism.

Martin

[Altenkirch Thorsten]

I agree with everything you say, Martin. However, a minor clarification:

On 04/01/2014 20:39, "Martin Escardo" <m.es...@cs.bham.ac.uk> wrote:

>Vladimir says "no problem". Work with equivalence, which is logically
>equivalent to isomorphism, but proof-irrelevant. (Great insight.)

This is potentially misleading, equivalence itself is not proof-irrelevant
but the property of a function being an equivalence is.

T.

[Martin Escardo]

On 04/01/14 21:38, Altenkirch Thorsten wrote:
> I agree with everything you say, Martin. However, a minor clarification:
>
> On 04/01/2014 20:39, "Martin Escardo" <m.es...@cs.bham.ac.uk> wrote:
>
>> Vladimir says "no problem". Work with equivalence, which is logically
>> equivalent to isomorphism, but proof-irrelevant. (Great insight.)
>
> This is potentially misleading, equivalence itself is not proof-irrelevant
> but the property of a function being an equivalence is.

Apologies for the imprecision.

Glad to see we agree.

Best,
Martin

[Bill Richter]

Yes, one definitely can [understand the homotopy theory/Martin-Lof
type theory connection with only 1960s homotopy theory skills].

Thanks, Vladimir. I'm happy with model categories (essential for fiberwise homotopy theory and even the unstable homotopy theory in Whitehead's book), LCCCs (or at least, closed monoidal categories) and simplicial sets (I like to say that there are two good model cats for topological spaces, the Strom model cat & simplicial sets, but the Quillen model cat for spaces is only good for stating results). BTW I just made and installed Coq at NWU (in /tmp, where I can't keep it), but I'm getting errors installing it on my home machine (where I bet I don't have enough libraries installed). I'll ask for help on Coq Club.

To everyone else: this is a fascinating discussion, but it's not giving me what I want. I want to explain to my HOL teammates (esp. John Harrison) that
1) 1960s homotopy theory explains Coq dependent types and that
2) therefore Coq/UF is a far superior proof assistant to HOL Light.
And I need a simple explanation of 1 & 2, because my HOL teammates know even less homotopy theory than I do. I know Vladimir says both 1 & 2 are true, but he's the genius, and that doesn't mean it's obvious. If I had to make a wild guess right now, I'd guess that 1 is not true, and instead, the way-past-1960s homotopy theory folks are doing nowadays (e.g. the n-categories of Michael and my coauthor John Baez) just happen to be related to complicated type theories. But I think that fields make progress when the "normal scientists" (like us) work their tails off to make the visions of the "paradigm shifters" (like Vladimir) come true (to use Kuhn's terminology). Maybe this forum isn't the right place to discuss this. If anyone interested in working with me on why 1 & 2 are true, maybe we should discuss this off-line. I like what Michael wrote

MS> We are still learning how to explain HoTT to newcomers, and it's
MS> difficult because everyone comes in with a different background
MS> and assumptions. Your feedback may help us improve the exposition
MS> for other people coming from the HOL world.

As well, Vladimir graciously offered to help me port my HOL code http://www.math.northwestern.edu/~richter/RichterHilbertAxiomGeometry.tar.gz
to Coq/UF, but if someone else wants to teach me instead, that would be fine.

--
Best,
Bill

[Vladimir Voevodsky]

On Jan 4, 2014, at 4:38 PM, Altenkirch Thorsten <psz...@exmail.nottingham.ac.uk> wrote:

> I agree with everything you say, Martin. However, a minor clarification:
>
> On 04/01/2014 20:39, "Martin Escardo" <m.es...@cs.bham.ac.uk> wrote:
>
>> Vladimir says "no problem". Work with equivalence, which is logically
>> equivalent to isomorphism, but proof-irrelevant. (Great insight.)
>
> This is potentially misleading, equivalence itself is not proof-irrelevant
> but the property of a function being an equivalence is.
>
> T.

Right. This is the only place in Martin's exposition which was somewhat confusing.

V.

[Martin Escardo]

Apologies again.

Let me develop Thorsten's remark for the record.

Let's say that f:X->Y is an isomorphism if we are in possession of
g:Y->X which is both a pointwise left and right inverse of f [homotopy
theorists will favour a different terminology for this notion]. We say
that f:X->Y is an equivalence if its fibers are contractible (see
other possible equivalent definitions in the HoTT book).

When I say that one works with equivalences rather isomorphisms I mean
that one works with maps f:X->Y which are equivalences. The point is
that "f is an equivalence" is always an hproposition but "f is an
isomorphism" is not necessarily an hproposition, although both are
logically equivalent (each one implies the other). This insight is due
to Vladimir, and makes sense in MLTT before we consider any model of
MLTT.

Martin

[Vladimir Voevodsky]

If we want to be precise historically then this insight is not due to me. As was pointed out to me recently by Max Kontsevich the fact tat in order to obtain correct notion of a homotopy equivalence one needs to consider two homotopies + 1 secondary homotopy was known to classics of homotopy theory starting with, probably, Boardman and Vogt. He also pointed out that if one applies this definition of weak equivalence to the map to the point then one recovers precisely "iscontr".

The precise statement which Max referred to is as follows - if one takes the free topological category generated by two objects, two morphisms in the opposite directions, two homotopies and one secondary homotopy as in the "correct" definition of a weak equivalence then the Hom-spaces of this topological category are contractible. If one does not consider a secondary homotopy or if one considers two secondary homotopies then one gets a topological category which is not contractible.

I did however had to re-invent it for UF and was not sure how to prove isapropiscontr constructively until I have developed quite a bit of the Foundations library (including gradth).


V.

PS By the way I am not sure what is the definition of a "free topological category" and would be quite curious to know.

[Martin Escardo]

It is interesting to see that this insight comes (again!) from a
homotopy theory route.

What I have in mind is the insight that "f:X->Y is an isomomorphism"
has a logically equivalent, proof-irrelevant, definition in
intensional MLTT. It is interesting that intuition from homotopy
theory can lead you to such a construction, which can be written down
in MLTT and makes sense on its own, even if homotopy theory hadn't
been invented/discovered to explain it.

Martin

[Michael Shulman]

I believe that 1 is true, or at least that a 1960s understanding of homotopy theory can aid in understanding dependent types. The homotopy theory notions used in chapter two of the book are quite basic. Those of us who like and are familiar with n-categories often talk about HoTT in that language, but it isn't at all necessary.

I am more doubtful about your point 2 however. Coq is a superior proof assistant for doing homotopy type theory because it uses intensional dependent type theory, which is what HoTT is based on. But I don't see why the homotopy interpretation would make it a superior proof assistant in all ways. Or is what you mean that Coq is superior for other reasons, but isn't usable until you understand dependent types, which the homotopy interpretation helps with?

[Bill Richter]

I believe that 1 is true, or at least that a 1960s understanding of
homotopy theory can aid in understanding dependent types. The
homotopy theory notions used in chapter two of the book are quite
basic.

Thanks, Michael. Let me use your earlier recommendation to explain my problem:
http://www.andrew.cmu.edu/user/awodey/preprints/TTH.pdf
Let's go to Steve's conclusions on p 15:

3. Conclusion: The logic of homotopy

An important and lively research program in current homotopy theory
is the pursuit (again following Grothendieck [Gro83]) of a general
concept of "stack," subsuming sheaves of homotopy types, higher
groupoids, quasi-categories, and the like. [...] The homotopy
interpretation of Martin-Lof type theory into Quillen model
categories, and the related results on type-theoretic constructions
of higher groupoids, are analogous to the basic results
interpreting extensional type theory and higher-order logic in (1-)
toposes. They clearly indicate that the logic of higher
toposes---i.e., the logic of homotopy---is, rather remarkably, a
form of intensional type theory.

This is completely incomprehensible to me, and I suspect, to any 1960s-era homotopy theorist. I'll believe that Steve's stacks and toposes are important, and that I could probably learn this stuff, but I doubt I could explain it to John Harrison. It seems to me that the HoTT book (which I apologize for not having read more carefully) is written in the same far-from-1960s-era-homotopy style:

For instance, interpreting types as sheaves helps explain the
intuitionistic nature of type-theoretic logic, [...]
Indeed, higher-dimensional category theory (particularly the theory
of weak infty-groupoids) is now known to be intimately connected
to homotopy theory, as proposed by Grothendieck and now being
studied intensely by mathematicians of both sorts.

Now to Vladimir, talking about sheaves is like breathing, as he's an algebraic geometer, and sheaves are quite simple compared to schemes, the fundamental object according to Hartshorne's book on Algebraic Geometry. I don't know this stuff. I read Hartshorne's other book on Euclid and Hilbert's axioms.

--
Best,
Bill

[Michael Shulman]

If I may quote my sentence following the one you quoted:

> Those of us who like and are familiar with n-categories often talk about HoTT in that language, but it isn't at all necessary.

The sentence you quoted from the book is from the introduction.  Have you tried chapter 2 as I suggested?

[Bill Richter]

Have you tried chapter 2 as I suggested?

Thanks, Michael. No, I have not tried very hard to read Chapter 2, or any part of the HoTT book. If I spent 2 weeks doing nothing but reading the first two chapters, I bet I could say something a lot more intelligent than I'm saying now. But I just paged through Chapter 2 now. I can see the words fibrations and homotopies, which is great, but Chapter 2 starts and ends with Steve's stuff that I find so forbidding:

The central new idea in homotopy type theory is that types can be
regarded as spaces in homotopy theory, or higher-dimensional
groupoids in category theory.

The actual homotopical interpretation, with identity types as path
spaces, and type families as fibrations, is due to [AW09], who used
the formalism of Quillen model categories. An interpretation in
(strict) ∞-groupoids was also given in the thesis [War08].

I didn't think, though, that I could jump right to Chapter 2. I thought I needed to read Chapter 1 first, and the intro seems to agree:

A reader who is familiar with Martin-Lof type theory can quickly
skim it to pick up the particulars of the theory we are using.
However, readers without experience in type theory will need to
read Chapter 1, as there are many subtle differences between type
theory and other foundations such as set theory.

And that would tend to say that I need to understand dependent types before understanding its homotopy theory interpretation. Would you agree?

Anyway, I think my problem with the HoTT book right now has much less to do with homotopy theory than the fact that the type theory in Chapter 1 looks so different from the type theory I learned in HOL, and I'm not really an expert yet on HOL type theory. I'm just not at all familiar with Martin-Lof type theory (Isn't that MLTT?).

--
Best,
Bill

[Michael Shulman]

The introduction to chapter 2 gives some explanation of the homotopy interpretation in intended-to-be-elementary language, which is why I mentioned it. To read all of chapter 2, yes, you should read chapter 1 first. Chapter 1 is about MLTT. My hope would be that from chapter 1 you can get sufficient understanding of DTT to be able to understand chapter 2, which would then help get a deeper understanding of dependent types. But it's impossible to say until you try. So maybe we should put this conversation on hold until you've actually tried to read the book.

[Bill Richter]

Thanks for the tips on reading Chapters 1 & 2, Michael.

So maybe we should put this conversation on hold until you've
actually tried to read the book.

Right. But let me make a conjecture now: the connection between UF/Coq and 1960s style homotopy theory is a lot harder to see, and more interesting & productive, than anyone has explained here yet.

--
Best,
Bill

[Vladimir Voevodsky]

On Jan 5, 2014, at 1:06 PM, Michael Shulman wrote:

I believe that 1 is true, or at least that a 1960s understanding of homotopy theory can aid in understanding dependent types. The homotopy theory notions used in chapter two of the book are quite basic. Those of us who like and are familiar with n-categories often talk about HoTT in that language, but it isn't at all necessary.

I am more doubtful about your point 2 however. Coq is a superior proof assistant for doing homotopy type theory because it uses intensional dependent type theory, which is what HoTT is based on. But I don't see why the homotopy interpretation would make it a superior proof assistant in all ways. Or is what you mean that Coq is superior for other reasons, but isn't usable until you understand dependent types, which the homotopy interpretation helps with?

Let's be precise here. Homotopy theory is needed not so much to understand dependent types (which can be understood on the example of propositional functions) but to understand:

1. Martin-Lof Identity Types.

2. Universes.

Without homotopy theory it is impossible to understand these two ingredients.

Vladimir.

[Vladimir Voevodsky]

BTW I can also suggest to have a look at my "Experimental library" paper which was recently posted to the arXiv. It's just 15pp and contains a few basic ideas which might be helpful in understanding UF-Coq.

V.

[Bill Richter]

Thanks, Vladimir. I'll try to learn about Martin-Lof Identity Types and Universes, and try to grasp the homotopy theory connection. I skimmed your paper http://arxiv.org/pdf/1401.0053.pdf, and it looks like a "users guide" to writing formal proofs using UF/Coq. And that sounds like a paper that will be very valuable to me when I start porting my Hilbert code to UF/Coq. Speaking of which, I installed coq on my account at NWU and I got on Coq-club, sent a bug report for my make failure on my home machine, and got one response.

Michael, I'm trying to make a contribution in a subject I know almost nothing about. Until yesterday, I didn't even know that Coq was based on LCF and ocaml, just like HOL Light. My half-butted idea is that nobody has yet explained how my subject, 1960s-era homotopy theory, gives a powerful explanation of why UF/Coq is great. My only reason for believing this is that
1) I think Vladimir is a genius, and geniuses often don't explain themselves very well, and
2) I have some intuition about formal proofs from a few years writing HOL Light proofs,
Since you're one of the authors HoTT book, I could see my half-butted idea rubbing you the wrong way, but I plead for tolerance. If I'm right, we're all better off, and if I'm wrong, I'll retract my error, and either way, my first step is, as you & Charles advised me, to read the first two chapters of the HoTT book.

--
Best,
Bill

[Alexis Hazell]

ric...@math.northwestern.edu writes:

> My half-butted idea is that nobody has yet explained how my subject,
> 1960s-era homotopy theory, gives a powerful explanation of why UF/Coq
> is great.

As someone who is very much an amateur in all this - I welcome any
corrections! - my thoughts are:

* As others have said, Coq is but one proof tool one can use for
UF/HoTT; Agda is another:

https://github.com/HoTT/HoTT-Agda

I believe there are pros and cons to using either. In any case, however,
it seems to me a distinction needs to be made between UF/HoTT, as areas
of mathematics, versus Coq / Agda etc., as tools used to research and
develop those areas.

* As far as I can tell, homotopy theory doesn't so much /explain/ UF,
but is instead applied to / combined with MLTT, to create the notion of
'types-as-spaces', and HoTT as a generalisation of that, /within/ the UF
program. I found this blog post to be quite enlightening:

"What's the big deal with HoTT?"
https://existentialtype.wordpress.com/2013/06/22/whats-the-big-deal-with-hott/

Hope I've not confused things further!


Alexis.

[Altenkirch Thorsten]

On 02/01/2014 16:44, "Bill Richter" <ric...@math.northwestern.edu> wrote:

>Thanks, Vladimir, and thanks to everyone else who responded.
>
> Yes. That's precisely what I have mentioned in the interview - that
> I could not understand Coq until I have invented the univalent
> model. With this model in mind the type theory of Coq becomes
> intuitive [...] Yes, definitely it is fixed in UF. In UF every set
> is a type (but not every type is a set).
>

>I'm really happy to hear this. So homotopy theory fixes the problem Bob
>Solovay noted with Coq.

What was the problem Soloway noted with Coq?

Thorsten

[Bas Spitters]

There was a discussion about the Miquel Werner paper in 2005 on coq-club. Solovay noticed a possible problem in the set-theoretical interpretation of universes (Prop:Type and Set:Type). Unfortunately, I cannot reach coq-club archives currently.

[Altenkirch Thorsten]

On 06/01/2014 03:25, "Alexis Hazell" <alexis...@gmail.com> wrote:

>
>ric...@math.northwestern.edu writes:
>
>> My half-butted idea is that nobody has yet explained how my subject,
>> 1960s-era homotopy theory, gives a powerful explanation of why UF/Coq
>> is great.
>
>As someone who is very much an amateur in all this - I welcome any
>corrections! - my thoughts are:
>
>* As others have said, Coq is but one proof tool one can use for
>UF/HoTT; Agda is another:
>
>https://github.com/HoTT/HoTT-Agda
>
>I believe there are pros and cons to using either. In any case, however,
>it seems to me a distinction needs to be made between UF/HoTT, as areas
>of mathematics, versus Coq / Agda etc., as tools used to research and
>develop those areas.

While nobody asked for it - here is an attempt at a comparison of Coq and
Agda:

In general Coq is the more mature tool while Agda is more recent and
experimental.

Agda emphasizes dependently typed programming which gives you a very
direct and often very readable notion of (proof-)terms. On the other hand
Agda doesn't yet support tactic based proof development (hopefully this
can be emulated by improved support for proof by reflection).

Agda implements pattern matching which makes many type theoretic
constructions much more readable and intuitive but has the disadvantage
that out-of-the-box it justifies uniqueness of equality proofs which is
incompatible with HoTT. However, there is an (experimental) flag without-K
which should rule this out (pattern matching without K is currently an
active area of research - see the Agda mailing list).

Agda directly supports more flexible type definitions, e.g.
inductive-recursive and inductive-inductive definition which allow you to
introduce user defined universes. Also Agda allows mixed
inductive-coinductive definitions very directly, even though again this is
an area of active experimentation.

Agda enforces termination via a termination checker which is more flexible
but I think less principled than Coq's approach. Most of Coq could be
reduced to a core theory only using eliminators - it is less clear how to
do this for Agda.

Agda implements universes very explicitely via (usually hidden) level
parameters. This is in principle more flexible than Coq's universe
inference but it adds lot of chatter to universe generic constructions
which frequently renders them unreadable.

Agda's syntax and approach to hidden arguments is more modern than the
corresponding baroque features in Coq.

Higher inductive types were first experimentally implemented in Agda (by
Dan Licata) using some existing features of Agda. However, I think Coq has
caught up on this now.

I cc this to the Agda and Coq lists. Hope I haven't started a flame war.
:-)

>
>* As far as I can tell, homotopy theory doesn't so much /explain/ UF,
>but is instead applied to / combined with MLTT, to create the notion of
>'types-as-spaces', and HoTT as a generalisation of that, /within/ the UF
>program. I found this blog post to be quite enlightening:
>
>"What's the big deal with HoTT?"
>https://existentialtype.wordpress.com/2013/06/22/whats-the-big-deal-with-h
>ott/
>
>Hope I've not confused things further!
>
>
>Alexis.
>

[Andrej Bauer]

On Sun, Jan 5, 2014 at 8:29 PM, Bill Richter
<ric...@math.northwestern.edu> wrote:
> I can see the words fibrations and homotopies, which is great, but Chapter 2 starts and ends with Steve's stuff that I find so forbidding:
>
> The central new idea in homotopy type theory is that types can be
> regarded as spaces in homotopy theory, or higher-dimensional
> groupoids in category theory.
>
> The actual homotopical interpretation, with identity types as path
> spaces, and type families as fibrations, is due to [AW09], who used
> the formalism of Quillen model categories. An interpretation in
> (strict) ∞-groupoids was also given in the thesis [War08].

That is an extremely selective way of reading the book. Just following
the first sentence, which you quoted, there are two pages of
introduction that speak in terms of "naive old-style" homotopy theory.
You should be able to just read all of that without effort until you
get to the relationship between the identity types and path spaces
around formula (2.0.1). Have you tried? It takes 5 minutes.

Regarding the sentence from the end of the chapter, that one is of
course not relevant to someone who wants to learn the stuff, as it
appears in the Notes. The book never uses Quillen models, sheaves, or
n-categories in a formal sense. All these notions are only mentioned
in historical notes and various introductions that try to give an
overview and an intuition to those who already know the stuff.
Similarly, the begining of Chapter 2 tries to give an overview to
those who already know "old" homotopy theory, but the mathematical
development does not rely in any way on these explanations. Similarly,
the introduction to Chapter 8 gives a blitz course in "old" homotopy
(targeted at computer scientists) that you could use to decypher what
the type theory is doing. Just ignore any sentence that mentions
n-categories, shaves or infinity-groupoids -- the mathematical
development does *not* rely on these notions.

With kind regards,

Andrej

[Bill Richter]

Thanks, Andrej. I only meant to give the impression that I'm floundering trying to read the HoTT book. I didn't mean to say that I had read the HoTT book carefully and had intelligent criticisms. Let me make another "floundering" comment:

As Mike S advised me, I started reading the HoTT book, and I'm struck by what I'm not hearing. Can you HoTT book authors write a short article explaining Coq/UF to experienced HOL programmers? It seems to me that the HoTT book is written for mathematicians who know nothing of type theory or formal proofs. For such an audience, the HoTT book might be a very good exposition. So I want to see
1) a "diff" between Coq/UF and HOL,
2) an explanation of why constructivism is useful and needed in writing formal proofs for the non-constructivist math that pure mathematicians use in their papers (LEM + AC).

As to 2, I sorta understand that Vladimir's Univalent axiom requires constructivism. But it seems sheer brilliance to me that this UF constructivism would help formalize non-constructivist papers. I speak in pure ignorance, and eventually I'll know a lot more, and maybe be able to write this short paper myself.

--
Best,
Bill

[Andrej Bauer]

> 1) a "diff" between Coq/UF and HOL,

For that I'd first ask whether you already know a "diff" between Coq
and HOL? In any case, someone else ought to comment, as I am not
familiar with HOL.

In any case, it's perfectly reasonable to expect that mathematics can
be formalized in HOL too (and it has been!). Asking "how should be set
up foundations of mathematics?" is *not* a mathematical question. In
principle we could use any foundation that is formally sufficient for
development of the usual kind of math. For instance, someone might be
crazy enough to suggest that we start with Sheffer stroke as the basic
logical connective.

It is a question about *design*, so we must necessarily think about
what the criteria of success are. Is the formalization for humans or
computers, or both? Is it targeted at set theorists or topologists or
algebraists? Programmers (the good ones) learned a long time ago that
there is no such thing as "the best programming language" and that it
is pointless to dream about having just one. A similar situation may
arise with formalization of mathematics, if and when it becomes
mainstream, although one would hope for a certain degree of
interoperability (certainly greater than what we now have in terms of
interoperability of software systems). Vladimir emphasises this point
often, namely that the ought to be a universally agreed upon way of
checking proofs (but not necessarily developing them).

> 2) an explanation of why constructivism is useful and needed in writing formal proofs for the non-constructivist math that pure mathematicians use in their papers (LEM + AC).

Certainly it is not "needed". But in my opinion pure mathematicians
who write papers using LEM + AC, and who for the most part can't even
tell where they used either of those, are not gods to be bowed to. It
is much more productive to teach them how to clean up their logic and
to try to improve the general mental hygiene of mathematical
community. I wouldn't even start with LEM or AC, I'd start with
teaching everyine the difference between bound and free variables, and
the benefits of lambda-calculus notation over 18th century notation
that pervades analysis and creates untold confusion.

> As to 2, I sorta understand that Vladimir's Univalent axiom requires constructivism. But it seems sheer brilliance to me that this UF constructivism would help formalize non-constructivist papers. I speak in pure ignorance, and eventually I'll know a lot more, and maybe be able to write this short paper myself.

If you only view constructivism as a necessary evil, then you might
indeed wonder why care about it. I very much like the answer Mike
Shulman once gave to "Why worry about the axiom of choice?", see
http://mathoverflow.net/questions/22927/why-worry-about-the-axiom-of-choice/22938#22938

With kind regards,

Andrej

[Vladimir Voevodsky]

On Jan 10, 2014, at 8:36 AM, Bill Richter <ric...@math.northwestern.edu> wrote:

> Thanks, Andrej. I only meant to give the impression that I'm floundering trying to read the HoTT book. I didn't mean to say that I had read the HoTT book carefully and had intelligent criticisms. Let me make another "floundering" comment:
>
> As Mike S advised me, I started reading the HoTT book, and I'm struck by what I'm not hearing. Can you HoTT book authors write a short article explaining Coq/UF to experienced HOL programmers? It seems to me that the HoTT book is written for mathematicians who know nothing of type theory or formal proofs. For such an audience, the HoTT book might be a very good exposition. So I want to see
> 1) a "diff" between Coq/UF and HOL,
> 2) an explanation of why constructivism is useful and needed in writing formal proofs for the non-constructivist math that pure mathematicians use in their papers (LEM + AC).
>
> As to 2, I sorta understand that Vladimir's Univalent axiom requires constructivism.

It does not require constructivism. We have already said that it is fully compatible with the law of excluded middle (for propositions) and axiom of choice (for sets).

We work constructively because UF enables, unexpectedly, to do many things constructively and we are exploring this new ability.

V.

[Michael Shulman]

It sounds like no one here knows enough about HOL to give you a direct
comparison. (Any counterexamples, please speak up!) So as I see it,
you have two options:

1. You can find someone else who can give you a direct comparison
between HOL and dependent type theory (MLTT/CIC) of the sort that
undelies Coq and Agda. Then you can come back and read chapter 2 of
the HoTT book, or other expository articles and blog posts written by
homotopy type theorists, which explain what the homotopy
interpretation adds to DTT.

2. You can put HOL aside for a little while and read chapter 1 of the
HoTT book which introduces DTT to a mathematician who, as you say,
knows nothing of type theory or formal proofs. I don't see why it
should be a problem that this explanation assumes *less* than you
already know, as long as you don't come in with a preexisting
insistence that it mention HOL. If you also want to see a formal
description of DTT, there is one in, among many other places, appendix
A of the HoTT book. Then you can use your newly acquired
understanding of DTT, along with your existing knowledge of HOL, to
compare them yourself, and thence proceed as in (1).

>> As to 2, I sorta understand that Vladimir's Univalent axiom requires constructivism.
>
> It does not require constructivism. We have already said that it is fully compatible with the law of excluded middle (for propositions) and axiom of choice (for sets).

However, it can *seem* to a type-theoretic constructivist that it
requires constructivism, because it is incompatible with a statement
that they may be used to thinking of as LEM (Corollary 3.2.7 in the
book). So it will probably be a long time before this myth dies
out....

Mike

[Matthieu Sozeau]

Dear all,

I think I have a little bit of knowledge I can share (please anyone more
knowledgeable correct me if I’m wrong):

- HOL is polymorphically typed but all types are inhabited, i.e.
you can’t see propositions as types as you can’t represent absurdity
as the empty type (with no introduction rule).
- HOL is “simply”-typed, so there is no dependency of types on values,
again, that breaks propositions as types.
- HOL is inherently classical as it represents truth values as booleans,
for which you obviously have EM.
- Quantifiers are a notion derived from Hilbert’s epsilon operator (again,
very classical), the other primitives being implication and polymorphic equality.
Equality is axiomatized there (congruent etc).
In Coq/Agda, the dependent function space is taken as primitive (subsumes
the arrow), there is no epsilon and equality and the existential quantifier
are notions derived from a general formation rule for inductive types but
that's a moving target. E.g. Agda uses a judgment to specify *definitional*
equality while Coq relies on the notion of conversion and *propositional* equality
derives from the definitional one in those two, while OTT defines propositional
equality in terms of other type/term constructors and HoTT sheds new light on
possible redefinitions of equality…

Constructive logic being an extension of classical logic [1], one can still do
classical reasoning in MLTT. But one can’t mimick the constructivist features
as easily in HOL as far as I know (but I have no proof of that). I would suspect
though, that the extensionality principles that derive from univalence, e.g.
that isomorphic types are equal are all valid for *sets* in HOL. Larry Paulson has
a nice introduction to the theory of HOL (Isabelle/HOL actually) in [2. sec 2.2 on],
there might be more detailed ones. HoTT might actually be a way to bring the ease
of use of HOL to MLTT while benefiting from its constructive features (that’s rather
informal, sorry :)


Best,
— Matthieu

[1] Classical Mathematics for a Constructive World - Russell O’Connor - http://arxiv.org/abs/1008.1213
[2] Mechanizing Coinduction and Corecursion in Higher-order Logic- Larry Paulson - http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-304.pdf

[Vladimir Voevodsky]

Thank you Matthieu! I guess I now know more about HOL then before :)

Can you explain what you mean by the word "polymorphic" in your outline?

V.

PS I have not assimilated yet your email about le on nat. I'll write to you about it when I do.

[Bas Spitters]

> HoTT might actually be a way to bring the ease of use of HOL to MLTT while benefiting from its constructive features

Yes, that's one of the things that excites me too about HoTT. hSets indeed form a PiW-pretopos, hence a model of iHOL (either with universe polymorphism, or with resizing).

It seems that developing basic mathematics such as abstract algebra and category theory is difficult in HOL. It is possible in Coq, but pleasant in homotopy type theory.

Also, quotients have recently been introduced to Isabelle/HOL. Homotopy type theory provides them in Coq.

Bas

[Steve Awodey]

On Jan 10, 2014, at 4:03 PM, Bas Spitters <b.a.w.s...@gmail.com> wrote:

> HoTT might actually be a way to bring the ease of use of HOL to MLTT while benefiting from its constructive features

Yes, that's one of the things that excites me too about HoTT. hSets indeed form a PiW-pretopos, hence a model of iHOL (either with universe polymorphism, or with resizing).

one just needs a topos, so propositional resizing suffices.

right?

Steve

[Bas Spitters]

Right. Thm 10.1.12

[Bill Richter]

Can you explain what you mean by the word "polymorphic" in your
outline?

Vladimir, I'm happy to answer this question, as I'm hoping to help mediate between the UF/Coq and HOL communities. I'm sure you know about polymorphic from Coq, but call it something different. It basically means a variable type. Here's from some code of mine, where I showed that we can redefine functions in HOL in order to prove that the Cartesian product has the usual universal property. I was surprised that I had to do this myself:

let FUNCTION = NewDefinition `;
FUNCTION α ⇔ ∃f s t. α = (t, f, s) ∧
(∀x. x IN s ⇒ f x IN t) ∧ ∀x. x ∉ s ⇒ f x = @y. T`;;

All the variables here have polymorphic types. The types of t & s are arbitrary: call them T and S. The type of f is then S->T, x has type S, and α has type T#(S->T)#S, using the "Cartesian product" type operator #. Notice another feature I assume you have in Coq, type inference. I didn't have to declare the polymorphic types S and T, as HOL can infer all the types above. Eventually I prove what you must think in UF/Coq is perfectly obvious, the theorem

UniversalPropertyProduct
|- ∀M A B α β. α ∈ M → A ∧ β ∈ M → B
⇒ (∃!γ. γ ∈ M → A ∏ B ∧
Pi1 A B ∘ γ = α ∧ Pi2 A B ∘ γ = β)

My guess is that in Coq you avoid the trouble I'm engaging in because of dependent types. Notic

Andrej and Vladimir, I'm really puzzled by what you say about constructivism. Perhaps we're better off for me to not post until I've made a real attempt to read the HoTT book. So feel free to not respond. However:

It does not require constructivism. We have already said that it is
fully compatible with the law of excluded middle (for propositions)
and axiom of choice (for sets).

Vladimir, I heard that, but I understood this to be a deep and surprising result, that you set up constructive models of UF which somehow can be used to prove non-constructive results.

We work constructively because UF enables, unexpectedly, to do many
things constructively and we are exploring this new ability.

Constructivism is of course a fantastic thing for CS folks to pursue. Aren't computers constructive machines? But are you saying that you could formalize normal AC+LEM pure math without constructivism and your Univalent axiom? I think the answer is "no", and because of the deep and surprising result I'm imagining above.

--
Best,
Bill

[Bill Richter]

If you also want to see a formal description of DTT, there is one in,
among many other places, appendix A of the HoTT book.

Thanks, Mike, I'll read it. Now I'd be happy to write a UF/Coq primer for HOL folks, once I learn it, but

It sounds like no one here knows enough about HOL to give you a
direct comparison.

I bet Bas knows enough.

However, it can *seem* to a type-theoretic constructivist that it
requires constructivism, because it is incompatible with a statement
that they may be used to thinking of as LEM (Corollary 3.2.7 in the
book). So it will probably be a long time before this myth dies
out....

What keeps the myth alive for me is on page 9 of the HoTT book:

HoTT> On the other hand, this notion of “or” is so strong that a naive
HoTT> translation of the law of excluded middle is inconsistent with
HoTT> the univalence axiom.

So I think there must be some deep result which says that constructive univalent models can be used to prove non-constructive pure math theorems, and I look forward to learning it.

--
Best,
Bill

[Michael Shulman]

On Fri, Jan 10, 2014 at 8:20 PM, Bill Richter
<ric...@math.northwestern.edu> wrote:
> However, it can *seem* to a type-theoretic constructivist that it
> requires constructivism, because it is incompatible with a statement
> that they may be used to thinking of as LEM (Corollary 3.2.7 in the
> book). So it will probably be a long time before this myth dies
> out....
>
> What keeps the myth alive for me is on page 9 of the HoTT book:
>
> HoTT> On the other hand, this notion of “or” is so strong that a naive
> HoTT> translation of the law of excluded middle is inconsistent with
> HoTT> the univalence axiom.

Did you notice the word "naive"? This sentence is saying exactly the
same thing that I said above.

[Prof Robert Harper]

It may help to mention that the form of "polymorphism" that Bill mentions below is not a semantic concept (i.e., not a type quantifier in the logic), but rather is inherent in the combination of type inference (allowing type information to be omitted, and to characterize the possible valid instances by some form of constraints) and definitions (under the policy that a defined identifier behaves precisely the same as its definition everywhere it occurs). This implies that multiple instances of a defined identifier can "instantiate" the constraints differently at each occurrence. This is exactly what is going on in Matthieu's recent revision of Coq to handle universes properly by employing mine and Pollack's algorithm based on these principles. I would say that the HOL _implementation_ has definitional polymorphism, and the Coq _implementation_ has definitional universe polymorphism, but neither the HOL _logic_ nor the Coq _logic_ has these concepts (i.e., there is no "Pi" over universes in the type theory, just a means of managing definitions flexibly).

Regarding constructivity, it is an unfortunate "social" phenomenon that constructivism is perceived as _opposed to_ classical mathematics. Rather, classical mathematics is an _instance_ of constructive mathematics (a "mode of use" of constructive mathematics) in which one imposes axioms such as LEM for propositions in order to recover classical patterns of reasoning. Alternatively, one may, Bishop-style, reinterpret classical reasoning in constructive form, typically strengthening assumptions or weakening conclusions _from a constructive point of view_ to obtain the same results, but with a more refined interpretation. So, for example, one may prove constructively that there cannot fail to exist infinitely many primes, corresponding to the usual classical argument that starts with "suppose there were only finitely many ...". classically this is entirely equivalent to prove that there are infinitely many primes, but constructively it is weaker. (one can of course prove a constructive form of the original statement as well, but in some situations this is not the case.) (For specialists, I am assuming a concept of constructivism that does not at the outset contradict classical reasoning. I realize that there are forms of "constructivism" that do not satisfy this requirement.)

On the mend,
Bob

[Vladimir Voevodsky]

On Jan 10, 2014, at 11:06 PM, Bill Richter <ric...@math.northwestern.edu> wrote:

> It does not require constructivism. We have already said that it is
> fully compatible with the law of excluded middle (for propositions)
> and axiom of choice (for sets).
>
> Vladimir, I heard that, but I understood this to be a deep and surprising result, that you set up constructive models of UF which somehow can be used to prove non-constructive results.

No. The univalent model is classical. How many times do I have to repeat the same thing?

It is not a deep and surprising result it is a triviality!

V.

[Vladimir Voevodsky]

On Jan 10, 2014, at 11:20 PM, Bill Richter <ric...@math.northwestern.edu> wrote:

> If you also want to see a formal description of DTT, there is one in,
> among many other places, appendix A of the HoTT book.
>
> Thanks, Mike, I'll read it. Now I'd be happy to write a UF/Coq primer for HOL folks, once I learn it, but
>
> It sounds like no one here knows enough about HOL to give you a
> direct comparison.
>
> I bet Bas knows enough.
>
> However, it can *seem* to a type-theoretic constructivist that it
> requires constructivism, because it is incompatible with a statement
> that they may be used to thinking of as LEM (Corollary 3.2.7 in the
> book). So it will probably be a long time before this myth dies
> out....
>
> What keeps the myth alive for me is on page 9 of the HoTT book:
>
> HoTT> On the other hand, this notion of “or” is so strong that a naive
> HoTT> translation of the law of excluded middle is inconsistent with
> HoTT> the univalence axiom.

I think this paragraph needs to be removed. The formulation of LEM in terms of all types (as opposed to in terms of propositions) is not "naive" from the point of view of an average reader.

It may only be possibly classified as "naive" from the point of view of someone who assumes "types as propositions" attitude and there are not many people who do.

Seriously, we need to remove this.

Vladimir.

[Steve Awodey]

well, it’s pretty standard among type theorists, who are part of the target audience.
rather than removing it, we should just clarify the remark, because it does make an interesting point about the (in)compatibility of PAT and UA.
How about this instead:

On the other hand, this notion of “or” is so strong that a naive type-theoretic translation of the law of excluded middle is inconsistent with the univalence axiom.

?

Steve

[Vladimir Voevodsky]

On Jan 11, 2014, at 10:46 AM, Steve Awodey <awo...@cmu.edu> wrote:

> well, it’s pretty standard among type theorists, who are part of the target audience.
> rather than removing it, we should just clarify the remark, because it does make an interesting point about the (in)compatibility of PAT and UA.
> How about this instead:
>
> On the other hand, this notion of “or” is so strong that a naive type-theoretic translation of the law of excluded middle is inconsistent with the univalence axiom.

I would still suggest that we remove it from the intro. We can discuss this kind of ambiguous issues deeper in the text where they do not stop a beginner reader from understanding things.

We do not have any problem with explaining things to people who know type theory. We have problems with explaining things to people who come from classical mathematics. I think this is something we have learned and something we should take into account in making choices about exposition in our introductory texts.

V.

[Martin Escardo]

On 11/01/14 15:14, Vladimir Voevodsky wrote:
>> What keeps the myth alive for me is on page 9 of the HoTT book:
>>

>> HoTT> On the other hand, this notion of �or� is so strong that a naive

>> HoTT> translation of the law of excluded middle is inconsistent with
>> HoTT> the univalence axiom.
>
>
> I think this paragraph needs to be removed. The formulation of LEM in terms of all types (as opposed to in terms of propositions) is not "naive" from the point of view of an average reader.
>
> It may only be possibly classified as "naive" from the point of view of someone who assumes "types as propositions" attitude and there are not many people who do.

Perhaps somebody should write a blog post about this, even though this
is already clarified in the HoTT Book, just to dispel the myth.

For the moment, I write it down here, as some form of public record.

The statement

Pi(X:U). X + �X

is *not* excluded middle.

Rather, it is *global* choice, which is much stronger than choice (in
the sense of ZFC), and in particular much stronger than excluded
middle.

This statement (i.e. type) is fullfiled (i.e. witnessed or "proved")
by a function that finds a point of any non-empty X:U.

The right way to formulate excluded middle, not only in HoTT, but also
already in MLTT, is

Pi(X:U). isProp(X) -> X + �X.

Global choice is inconsistent with univalance, but excluded middle is
consistent, and in fact valid in the model of simplicial
sets.

Moreover, (non-global) choice itself (which implies excluded middle),
is also consistent with univalance, and again valid in the model of
simplicial sets.

This is all clearly explained in the book.

However, given the myths out there, this doesn't prevent one from
trying to make it even more emphatic in the book.

As it has already been said in this discussion, the fact that HoTT
*can* be developed constructively is a *bonus* rather than a price to
pay. HoTT doesn't *have to* be developed constructively. It just
happens that it can, and, that, moreover, more often than not, the
constructive arguments are the more natural ones to consider, when
more than one option is available.

Martin

[Vladimir Voevodsky]

Thank you Martin!

Let me just add that this issue seems to have acquired some viral form. I spoke to one important mathematician a few weeks ago who said that he believes that we can formalize ``some mathematics, probably what is called constructive mathematics" but not all mathematics.

This seems to be one of the lines of resistance to what we do which arose (spontaneously) in the general mathematical ``word of mouth" culture.

V.

On Jan 12, 2014, at 2:36 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

>
>
> On 11/01/14 15:14, Vladimir Voevodsky wrote:
>>> What keeps the myth alive for me is on page 9 of the HoTT book:
>>>

>>> HoTT> On the other hand, this notion of “or” is so strong that a naive

>>> HoTT> translation of the law of excluded middle is inconsistent with
>>> HoTT> the univalence axiom.
>>
>>
>> I think this paragraph needs to be removed. The formulation of LEM in terms of all types (as opposed to in terms of propositions) is not "naive" from the point of view of an average reader.
>>
>> It may only be possibly classified as "naive" from the point of view of someone who assumes "types as propositions" attitude and there are not many people who do.
>
>
> Perhaps somebody should write a blog post about this, even though this
> is already clarified in the HoTT Book, just to dispel the myth.
>
> For the moment, I write it down here, as some form of public record.
>
> The statement
>

> Pi(X:U). X + ¬X

>
> is *not* excluded middle.
>
> Rather, it is *global* choice, which is much stronger than choice (in
> the sense of ZFC), and in particular much stronger than excluded
> middle.
>
> This statement (i.e. type) is fullfiled (i.e. witnessed or "proved")
> by a function that finds a point of any non-empty X:U.
>
> The right way to formulate excluded middle, not only in HoTT, but also
> already in MLTT, is
>

> Pi(X:U). isProp(X) -> X + ¬X.

>
> Global choice is inconsistent with univalance, but excluded middle is
> consistent, and in fact valid in the model of simplicial
> sets.
>
> Moreover, (non-global) choice itself (which implies excluded middle),
> is also consistent with univalance, and again valid in the model of
> simplicial sets.
>
> This is all clearly explained in the book.
>
> However, given the myths out there, this doesn't prevent one from
> trying to make it even more emphatic in the book.
>
> As it has already been said in this discussion, the fact that HoTT
> *can* be developed constructively is a *bonus* rather than a price to
> pay. HoTT doesn't *have to* be developed constructively. It just
> happens that it can, and, that, moreover, more often than not, the
> constructive arguments are the more natural ones to consider, when
> more than one option is available.
>
> Martin
>
>
>
>

[Michael Shulman]

On Sat, Jan 11, 2014 at 7:53 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> We do not have any problem with explaining things to people who know type theory.

I think that insofar as this may be true, it is at least partly
because there were so many of these people at IAS last year and we got
a lot of practice explaining things to them. In particular, that
sentence is serving a purpose, and should not be simply removed.
Indeed, it could not be simply removed without totally rewriting the
rest of the section in which it appears.

It seems to me that that sentence is only problematic to a reader who
fails to notice the word "naive" and also stops reading there without
finishing the section, which goes on to explain

> the "(-1)-truncated law of excluded middle" may be assumed, with many of the same consequences as in classical mathematics.... univalent foundations does not *require* the use of constructive or intuitionistic logic. Most of classical mathematics which depends on the law of excluded middle and the axiom of choice can be performed in univalent foundations, simply by assuming that these two principles hold (in their proper, (-1)-truncated, form).

Perhaps it would be better if we could write the section so that even
a reader who stops halfway through would not come away with a wrong
impression, but I'm not quite sure how to do that.

[Vladimir Voevodsky]

> and also stops reading there without finishing the section,

I think this is precisely what happens. Somebody reads this sentence and more or less thinks ``thanks god, I was right, it really does not affect normal mathematics, I do not have to do all the hard work of really understanding all these pages".

V.

[Martin Escardo]

On 12/01/14 21:26, Vladimir Voevodsky wrote:

> Let me just add that this issue seems to have acquired some viral
> form. I spoke to one important mathematician a few weeks ago who
> said that he believes that we can formalize ``some mathematics,
> probably what is called constructive mathematics" but not all
> mathematics.

> This seems to be one of the lines of resistance to what we do which
> arose (spontaneously) in the general mathematical ``word of mouth"
> culture.

Perhaps this prejudice has its origin in the fact that all previously
known "synthetic theories" (synthetic differential geometry, synthetic
domain theory, synthetic topology, synthetic computability theory)
*do* postulate axioms that contradict excluded middle?

In fact, the traditional developments of such synthetic theories
usually do start by "apologizing" that giving up excluded middle is
the price to pay.

Maybe it is indeed interesting and even surprising after all, perhaps
even for the non-classical mathematicians listening here, in addition
to the classical ones, that there is no such price to pay in the case
of HoTT.

Martin

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

[Steve Awodey]

this is a very useful record, but I think the following needs to be added:

On Jan 12, 2014, at 2:36 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>

> The statement
>
> Pi(X:U). X + ¬X
>
> is *not* excluded middle.


but it clearly IS excluded middle under the usual propositions as types interpretation!
so we really ARE saying something about the (in)compatibility of PAT, UA, and EM.
that’s also worth noting!

[Martin Escardo]

Let's discuss this without reference to HoTT models or axioms.

The interpretation of MLTT in ZF is well known to the PAT people (of
course with Grothendieck universes to model universes), as is often
used as a motivation to "explain" MLTT.

Under this interpretation of MLTT, the above statement cannot be
validated using ZF's excluded middle. It can't be validated even if we
move to ZFC. And it is easy to see that the interpretation of this
statement *is* global choice (giving a function that picks an element
from each non-empty set).

On the other hand, the statement Pi(X:U). isProp X -> X + ¬X is
validated in ZF, and is precisely what is called excluded middle in
ZF.

So I would say that it is indeed naive to regard (Pi(X:U). X + ¬X) as
the MLTT rendering of excluded middle, as the book claims.

(Similarly, what PAT people call choice, which is provable in MLTT, is
not choice under the ZF interpretation of MLTT, and doesn't imply
excluded middle in any sense.)

Martin

[Marc Bezem]

Maybe the negative formulation ("inconsistent") is the culprit. What about modifying:

"On the other hand, this notion of “or” is so strong that a naive translation of the law of excluded middle is inconsistent with the univalence axiom."

into

"On the other hand, this notion of “or” is so strong that one must be careful in formulating the law of excluded middle.
The formulation "for all \emph{propositions} A, either A or not A" is perfectly consistent with the univalence axiom.

(In HoTT, not all types are considered to be propositions)."

Marc

--
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 HomotopyTypeTheory+unsub...@googlegroups.com.

[Altenkirch Thorsten]

I think this is mainly a question of terminology. The same issue show up
with the axiom of choice: we have a type-theoretic one and a propositional
one (the -1 truncated one). In the past when we said axiom of choice in a
type-theoretic context we mean the type-theoretic one which is actually
provable. It seems better that by axiom of choice we mean the
propositional one because this one corresponds to the traditional one and
when we want to refer to the untruncated one we say the "type-theoretic
axiom of choice".

The same reasoning applies to the excluded middle. In the past we used
Pi(X:U). X + ¬X but now we can quantify over Prop instead, which is the
propositional excluded middle which indeed corresponds to the conventional
meaning of excluded middle. And indeed HoTT is compatible with the
propositional excluded middle but not with the type-theoretic one. Hence
when we say "excluded middle" we should refer to the propositional axiom
of choice. If we want to talk about the other one we can say the
"type-theoretic excluded middle" (which is incompatible with univalence).

>--
>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/groups/opt_out.

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.

[Peter Aczel]

I hesitate to add the following point to the discussion with title:

[HoTT] newbie questions about homotopy theory & advantage of UF/Coq

Absolute newbies can perhaps ignore the following!

Once one has got a bit used to HoTT, its type theory and its treatment of logic using `homotopy' propositions one may want to exploit the use of other logics in HoTT.  In particular, although the standard HoTT version of excluded middle is relatively consistent with standard HoTT there may turn out to be good reasons to avoid assuming it as much as possible.  Also, the Curry-Howard propositions-as-types treatment of logic should not be completely dismissed from HoTT, just because it is incompatible with excluded middle in that logic.

[Steve Awodey]

Dear Martin,

I’m well aware that the interpretation of the type theoretic LEM in the form X + - X is actually a strong form of AC in the model — and not just in ZF, but in any topos (my very first paper in 1995 was about this).

But that doesn’t change the fact that it IS the LEM under the PAT reading of type theory — just as AC becomes provabe under that reading.

We agree that it’s more useful to read the type theory in a different way that makes these conditions more meaningful, and allows for other distinctions by also using propositional truncation. But the PAT reading is what it is, whether we like it or not.

Steve

[Steve Awodey]

I agree with Thorsten in general here,probably because we already agreed about this in Princeton after we discussed it there at length.  I say “in general” because the specific solution we came up with then, which is implemented in the book, is to be even more precise and say:

LEM_\infty for  “type theoretic LEM"

LEM = LEM_{-1} for  “(propositional) LEM”

as well as:

AC_\infty  for  “type theoretic AC"

AC = AC_{-1}  for  “(propositional) AC”

There are analogous intermediate conditions LEM_n and AC_n which could also be of interest.

Steve 

[Frédéric Blanqui]

Le 13/01/2014 05:00, Steve Awodey a �crit :

> this is a very useful record, but I think the following needs to be added:
>
> On Jan 12, 2014, at 2:36 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>> The statement
>>

>> Pi(X:U). X + �X

>>
>> is *not* excluded middle.
>
> but it clearly IS excluded middle under the usual propositions as types interpretation!
> so we really ARE saying something about the (in)compatibility of PAT, UA, and EM.

> that�s also worth noting!
>
Hi. What is PAT?

[Martin Escardo]

On 13/01/14 15:40, Steve Awodey wrote:
> But that doesn�t change the fact that it IS the LEM under the PAT reading of type theory � just as AC becomes provabe under that reading.


(It seems strange to call "excluded middle" something that is stronger
than classical choice, not provable in ZFC.)

Martin

[Michael Shulman]

Steve is right -- this is a rehash of an old argument from last year.
PAT is not *wrong*, in fact one can validly interpret logic in any
modality. PAT results from the identity modality, and a more usual
intuitionistic logic from the (-1)-truncation modality. What is wrong
is (at least in the presence of univalence) using the identity
modality to interpret LEM. But the PAT interpretation of logic is
also important.

When writing type-theoretic mathematics in informal English, we are
faced with the problem that ordinary logical language does not provide
a way to specify the modality in use. The solution decided on for the
book was to use adverbs to indicate the modality, e.g. "merely" for
the (-1)-truncation and "purely" for the identity. In the book we
chose that the identity modality would be the default in the absence
of an adverb, but we pointed out that in other contexts one might make
other choices.

This is all discussed at length in section 3.10.

[Vladimir Voevodsky]

Propositions as types does not mean types as propositions!

That propositions can be considered to be types is a great idea which is very important and fruitful. The attempts to reverse it by saying that all types are propositions is much less interesting and mostly simply confusing.

V.

[Peter Aczel]

(It seems strange to call "excluded middle" something that is stronger than classical choice, not provable in ZFC.)

What "excluded middle" means and its strength depends on the logic in which it is expressed.

On 13 January 2014 16:05, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

On 13/01/14 15:40, Steve Awodey wrote:

But that doesn’t change the fact that it IS the LEM under the PAT reading of type theory — just as AC becomes provabe under that reading.

(It seems strange to call "excluded middle" something that is stronger than classical choice, not provable in ZFC.)

Martin

--
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 HomotopyTypeTheory+unsub...@googlegroups.com.

[Frédéric Blanqui]

Thanks for those who sent me the answer: PAT = Propositions As Types.

Le 13/01/2014 17:01, Fr�d�ric Blanqui a �crit :

[Peter Aczel]

Types as propositions may be less interesting for H0TT than propositions as types.  Nevertheless it is a possible logic.  It is interesting that it cannot be classical in HoTT.

--
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.

[Vladimir Voevodsky]

On Jan 13, 2014, at 4:00 AM, Marc Bezem wrote:

> Maybe the negative formulation ("inconsistent") is the culprit. What about modifying:
>
> "On the other hand, this notion of “or” is so strong that a naive translation of the law of excluded middle is inconsistent with the univalence axiom."
>
> into
>
> "On the other hand, this notion of “or” is so strong that one must be careful in formulating the law of excluded middle.
> The formulation "for all \emph{propositions} A, either A or not A" is perfectly consistent with the univalence axiom.
> (In HoTT, not all types are considered to be propositions)."

Yes, this would be much better.

Vladimir.

[Steve Awodey]

I agree that it is strange, but it is out there (and it is in fact the usual meaning of the term “propositions as types”).
We just need to be clear how our interpretation of type theory relates to it and differs from it — but in order to do that, we need to recognize it as another option, if only by way of contrast, rather than dismissing it or reinterpreting it from the start.

[Andrej Bauer]

On Sun, Jan 12, 2014 at 8:36 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> Perhaps somebody should write a blog post about this, even though this
> is already clarified in the HoTT Book, just to dispel the myth.

Maybe like this?

http://math.andrej.com/2014/01/13/univalent-foundations-subsume-classical-mathematics/

[Michael Shulman]

Here is a proposed change to the introduction:

https://github.com/mikeshulman/book/commit/d151e50b9f864ec0053edefdb761227dfc063f0c

We spent a lot of time on small wording details of the introduction
last year, so I am hesitant to touch it at all, but I agree that this
is a problem. So I tried to make the smallest possible change, not
looking only at one sentence but at the narrative exposition of the
whole section.

Let's move discussion of specific changes to the book introduction to github:
https://github.com/HoTT/book/issues/606

[Vladimir Voevodsky]

Let me repeat again - the book is about UF and in the UF the formulation of LEM is isaprop P -> ( coprod P ( P -> empty ) )

So UF is not PAT and we may say something about it but we should not define UF by what it is not.

V.

[Steve Awodey]

yes, of course.
I was not talking about the book — I think the book is quite clear on this point (and even more so with Mike’s proposed revision).
I was talking about Martin’s claim that X + - X is simply “*not* excluded middle”.
It simply *is* excluded middle under PAT, whether one likes it of not.
The fact that this is not compatible with UF — and so also not with the book — is an interesting observation about the relation between UF, PAT, and LEM, which does not go away if we choose to ignore the fact that some people use the PAT interpretation— but now I am just repeating myself.

[Bill Richter]

I am thrilled with the great response I've gotten from everyone on the thread I started

"newbie questions about homotopy theory & advantage of UF/Coq"

but right now I understand very little of what folks are posting, so I wanted to start a new thread, devoted to what I actually want to learn. I'm going on the assumption that UF/Coq is a superior proof assistant to e.g. HOL Light, and I say this with the highest possible regard and admiration for John Harrison, who encouraged my HOL Light. So I want to learn why UF/Coq is superior, and I want to learn how to explain this to HOL programmers before May.

Now Vladimir clearly responded to my needs by writing

VV> I think this paragraph [on page 9 of the HoTT book] needs to be
VV> removed. The formulation of LEM in terms of all types (as opposed
VV> to in terms of propositions) is not "naive" from the point of view
VV> of an average reader.

I don't pretend I to understand the discussion of Vladimir's post, or Mike proposed modification of the HoTT book. What I want to understand is Vladimir response to me:

VV> No. The univalent model is classical. How many times do I have to repeat the same thing?
VV> It is not a deep and surprising result it is a triviality!

That's great, and if it's that easy, I should be able to understand it by reading the HoTT book, right? We don't have to discuss this here. But I'd like someone to explain a different point:

VV> We work constructively because UF enables, unexpectedly, to do
VV> many things constructively and we are exploring this new
VV> ability.

I speak in complete ignorance here, but I'd like understand something here. Let's suppose that we had no interest whatsoever in working constructively, and only wanted to formalize classical pure math. Would we then need UF? Could we write a simpler proof assistant that formalizing classical pure math just as well as UF/Coq does? And would this simpler proof assistant be, in fact, Coq?

I really want you to say this is not true, because my HOL programmers friends think that Coq is too hard to learn!

And I'd like someone to give a simple explanation, if one exists, of why the constructive potential of UF is necessary to produce such a nice classical proof assistant as UF/Coq. If no one has such a simple explanation, then I consider it my highest priority to produce this explanation by May. If someone has such a simple explanation, can I recommend putting it in the introduction to HoTT book?

BTW I'm sorry that I've been such a poor correspondent. In Chicago, we went from -45F windchill to the sidewalks being flooded.

--
Best,
Bill

[Andrej Bauer]

Dear Bill,

your posts will always be in danger of veering off in hott directions.

Regarding UF and classical mathematics, have you seen my blog post at
http://math.andrej.com/2014/01/13/univalent-foundations-subsume-classical-mathematics/
? I try to draw there a clear picture of how UF subsumes classical
math, without going into any details or fine points.

> I speak in complete ignorance here, but I'd like understand something here. Let's suppose that we had no interest whatsoever in working constructively, and only wanted to formalize classical pure math. Would we then need UF? Could we write a simpler proof assistant that formalizing classical pure math just as well as UF/Coq does? And would this simpler proof assistant be, in fact, Coq?

I am not sure the point has come across clearly enogh: constructive
math is *not* in opposition to classical math. It is a generalization.
It just so happens that in UF many important theorems can be proved
without application of excluded middle or the axiom of choice. This is
an *added* benefit.

Surely, any mathematician will admit that theorems should be stated
and proved as economically as possible. So you can understand the
whole UF business as improvement: by *generalizing* the setup from
classical math to UF we can compute homotopy groups, and do category
theory, and construct reals, form free algebras, etc., *more
economically* than before (no use of excluded middle and choice). Some
topics still rely on excluded middle and choice, for instance the
theory of ordinals and cardinals.

There are many benefits to proving things constructively, even if you
are a classical mathematician. It's a bit like proving a theorem
abstractly about any vector space instead of specifically about R^n.
The proof is likely to be more conceptual and the theorem will be more
widely applicable. I feel like we're talking a bit past you. For
instance, have you read that answer of Mike Shulman's to the question
"why worry about axiom of choice"? It precisely addresses your
questions of why a classical mathematician should care about choice.
But you never commented on it, so I do not know what else we can offer
as an answer.

With kind regards,

Andrej

[Bas Spitters]

On Tue, Jan 14, 2014 at 10:04 AM, Andrej Bauer <andrej.bauer@andrej.com> wrote:

> I speak in complete ignorance here, but I'd like understand something here.  Let's suppose that we had no interest whatsoever in working constructively, and only wanted to formalize classical pure math.  Would we then need UF?  Could we write a simpler proof assistant that formalizing classical pure math just as well as UF/Coq does?  And would this simpler proof assistant be, in fact, Coq?

I'll repeat once more what I said before:

hSets indeed form a PiW-pretopos, hence a model of iHOL (either with universe polymorphism, or with resizing).

With excluded middle we can interpret classical HOL, so we are strictly more expressive.

It seems that developing basic mathematics such as abstract algebra and category theory is difficult in HOL.
E.g. apparently one first needs to encode set th in HOL and then use this to do cat th:
http://afp.sourceforge.net/entries/Category2.shtml
"Extensive use is made of the HOLZF theory". "The HOL type ZF axiomatizes ZFC".

Cat th is possible in Coq, but pleasant in homotopy type theory.

For abstract classical mathematics HoTT+LEM should be better than either Coq+LEM or HOL.

Also, quotients have recently been introduced to Isabelle/HOL. Homotopy type theory provides them in Coq.

Best,

Bas

[Vladimir Voevodsky]

Hi Steve,

quoting one of you yesterday's posts:

> But that doesn’t change the fact that it IS the LEM under the PAT reading of type theory — just as AC becomes provabe under that reading.
>
> We agree that it’s more useful to read the type theory in a different way that makes these conditions more meaningful, and allows for other distinctions by also using propositional truncation. But the PAT reading is what it is, whether we like it or not.

I would be very interested in part from the perspective of the history of the ``propositions as types" idea to know what is the original reference for this reading of LEM.

Vladimir.

[Vladimir Voevodsky]

On Jan 14, 2014, at 4:04 AM, Andrej Bauer <andrej...@andrej.com> wrote:

 speak in complete ignorance here, but I'd like understand something here.  Let's suppose that we had no interest whatsoever in working constructively, and only wanted to formalize classical pure math.  Would we then need UF?  

Yes. 

Could we write a simpler proof assistant that formalizing classical pure math just as well as UF/Coq does?  And would this simpler proof assistant be, in fact, Coq?

I do not understand the question. 

The core language of Coq is very simple. I am pretty sure it is simpler than, for example, HOL light. It can be used to express complex things but the language itself is not complex.

V.

[Andrej Bauer]

On Tue, Jan 14, 2014 at 4:52 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> I would be very interested in part from the perspective of the history of the ``propositions as types" idea to know what is the original reference for this reading of LEM.

Well, this reading of LEM comes from the "Propositions = Types" idea
under which first-order logic is translated to type theory according
to

Prop = Type
forall = Pi
or = +
false = 0
imply = ->

Applying the translation of

forall p : Prop, p \/ (p -> false)

is

Pi (p : Type), P + (P -> 0).

So that's it. But you must be asking something else.

With kind regards,

Andrej

[Bas Spitters]

On Tue, Jan 14, 2014 at 5:25 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:

The core language of Coq is very simple. I am pretty sure it is simpler than, for example, HOL light. It can be used to express complex things but the language itself is not complex.

FWIW Freek Wiedijk once did some statistics. I am not sure what to think of these methods, but this seems to be what you are currently discussing.
http://www.cs.ru.nl/~freek/zfc-etc/zfc-etc.pdf

Abstract. This paper presents Automath encodings (which also are valid in LF/lambda-P) of various kinds of foundations of mathematics. Then it compares these encodings according to their size, to find out which foundation is the simplest.
The systems analyzed in this way are two kinds of set theory (ZFC and NF), two systems based on Church's higher order logic (Isabelle/Pure and HOL), three kinds of type theory (the calculus of constructions, Luo's extended calculus of constructions, and Martin-Löf predicative type theory) and one foundation based on category theory.
The conclusions of this paper are that the simplest system is type theory (the calculus of constructions) but that type theories that know about serious mathematics are not simple at all. Set theory is one of the simpler systems too. Higher order logic is the simplest if one looks at the number of concepts (twenty-five) needed to explain the system. On the other side of the scale, category theory is relatively complex, as is Martin-Löf's type theory. [19 pp.]

[Thierry Coquand]

This reading is taken without comment in An Intuitionistic Theory of Types, P. Martin-Löf, 1972
section 3.3.3.
The paper Kolmogorov, 1932, explains why one should not expect LEM to be valid with the reading
of proposition as problem and proof as solution (an early influence of the "propositions as types" idea).

Thierry

[Vladimir Voevodsky]

I mean a bibliographical reference.

V.

[Michael Shulman]

On Mon, Jan 13, 2014 at 7:47 PM, Bill Richter
<ric...@math.northwestern.edu> wrote:
> I speak in complete ignorance here, but I'd like understand something here. Let's suppose that we had no interest whatsoever in working constructively, and only wanted to formalize classical pure math. Would we then need UF?

What does "need" mean? The vast majority of classical mathematics
does not require any particular foundation; most of it can be done
with ZFC or ETCS or HOL or Coq or UF or etc. etc.

There are, however, *advantages* to UF even if you don't care about
being constructive, such as the potential for doing synthetic homotopy
theory, and the ability to automatically and formally transport
structures across isomorphisms.

> And I'd like someone to give a simple explanation, if one exists, of why the constructive potential of UF is necessary to produce such a nice classical proof assistant as UF/Coq.

I think one short answer is "propositions as types". It is easiest to
see that this is the answer if you reword the question as "supposing
we want to produce a nice proof assistant; why are we naturally led to
one which is by default constructive?" There are all sorts of
nicenesses that flow from unifying constructions on types (cartesian
product, function type, dependent sum, etc.) with logical operations
on propositions (conjunction, implication, existential quantification,
etc.). For instance, your type-checking algorithm becomes also a
proof-checking algorithm, your proofs are terms inhabiting a type that
can serve as "certificates" which can be checked much more easily than
they can be produced, and your proofs are also programs which can be
executed. But when you identify propositions with the types of their
proofs, the logic which naturally emerges is constructive.

> If someone has such a simple explanation, can I recommend putting it in the introduction to HoTT book?

Propositions as types, and how it leads to constructivism and its
advantages, are discussed in the introduction to the book, and
expanded on in chapters 1 and 3. It would not be appropriate for the
book to talk about proof assistants in particular, because the book is
about *informal* type theory.

Mike

[Bill Richter]

Vladimir & Dan, thanks for helping me install Coq 8.3 plus Foundations. I did try on my 32-bit machine to make Coq 8.3 with the Foundation patches, and got the same error. But I bet Dan's patches work.

Thanks to Andrej and Mike and everyone who responded. I think I'm not being clear. The issue for me isn't whether UF/Coq is a great thing, something that will improve classical pure math. I assume that's true, but I'm trying to sell UF/Coq to HOL programmers, and I'm worried about something more practical.

Let's forget fancy category theory etc. for a bit and say we e.g. want to formalize the period doubling route to chaos, which is not well explained in Devaney's book. Sternberg has some on-line notes which greatly expand Devaney's proofs. But since no clear explanation is published, why don't we formalize it? I think it shouldn't involve any category theory. So what is the best proof assistant to use? HOL has problems just composing function defined on sets, so perhaps Coq with its dependent types would be superior to HOL Light. But John Harrison says, citing Bob Solovay, that Coq's dependent types are too hard to understand. So maybe it's my mission to understand Coq's dependent type, which you say aren't hard, and explain them to the HOL world. That's fine, if that's my mission.

But maybe I'm getting it wrong. Maybe UF/Coq is superior to plain Coq even in trying to formalize the period doubling route to chaos. Does that sound true? If so, then my mission is to understand the value of UF/Coq even for advanced calculus and point set topology. That sounds like a challenging and interesting mission.

--
Best,
Bill

[Bas Spitters]

Dear Bill,

I believe I have answered to what I believe was Solovay's question, if not, please provide us with a more precise statement.

We meet the HOL community regularly, for instance at ITP, CPP, ... Here my was attempt at explaining my excitement for UF (to the Coq community admittedly).
   http://www.cs.ru.nl/~spitters/Coq13.pdf

others will have made similar attempts. I don't believe in selling UF, but I do believe in trying to explain it.

Best,

Bas

[Vladimir Voevodsky]

On Jan 15, 2014, at 8:49 AM, Bill Richter wrote:

> Vladimir & Dan, thanks for helping me install Coq 8.3 plus Foundations. I did try on my 32-bit machine to make Coq 8.3 with the Foundation patches, and got the same error. But I bet Dan's patches work.

You are not being clear. On which machines have you succeeded in installing patched Coq + Foundations and on which you have not?

V.

[Vladimir Voevodsky]

On Jan 15, 2014, at 8:49 AM, Bill Richter wrote:

But maybe I'm getting it wrong.  Maybe UF/Coq is superior to plain Coq even in trying to formalize the period doubling route to chaos.  Does that sound true? 

Yes. Except there is no "UF/Coq".  There is Coq and there is a way to encode mathematical concepts in Coq which is compatible with UF. 

V.

[Bill Richter]

You are not being clear. On which machines have you succeeded in
installing patched Coq + Foundations and on which you have not?

Sorry, Vladimir. I have never succeeded in in building coq 8.3 on any machine, with or without your Foundations patches. I have not succeded in installing Dan's 8.3 coq-builder-master patches. I did succeed in installing your Foundations patches on my home 32-bit machine, and I'll now install them on the NWU 64-bit machine. I'm glad I'm doing this, because I want to tell you what patches I'm installing. First:

(poisson)Desktop> tar xvfz ../Downloads/coq-8.3pl2.tar.gz

Then in a different directory I
unzip Foundations-master.zip
I read your file
Foundations-master/Coq_patches/README
and (I think) found all the relevant patch commands starting with vladimir$. I copied these patches to the coq-8.3pl2 directory

(poisson)Coq_patches> cp *patch* ~/Desktop/coq-8.3pl2/

I then moved to coq-8.3pl2 and ran these commands:

patch -p1 < inductive-indice-levels-matter-8.3.patch
patch -p3 < patch.type-in-type
patch -p0 < fix-hanging-at-end-of-proof.patch
patch -p0 < grayson-fix-infinite-loop.patch
patch -p0 < grayson-improved-abstraction-version2-8.3pl2.patch
patch -p0 < grayson-closedir-after-opendir.patch

I think all the patches installed correctly, and the output is included below.

But I could not build coq 8.3 with the Foundation patches.

I get the same error:

./configure --prefix /rhome/2/richter/Coq83 -natdynlink no
make world
[..]

OCAMLC library/heads.mli
OCAMLOPT library/heads.ml
OCAMLOPT -a -o library/library.cmxa
OCAMLC pretyping/vnorm.mli
OCAMLOPT pretyping/vnorm.ml
OCAMLC pretyping/retyping.mli
OCAMLOPT pretyping/retyping.ml
OCAMLC pretyping/cbv.mli
OCAMLOPT pretyping/cbv.ml
OCAMLC pretyping/pretype_errors.mli
OCAMLOPT pretyping/pretype_errors.ml
File "pretyping/pretype_errors.ml", line 49, characters 4-109:
Error: Unbound constructor Stdpp.Exc_located
make[1]: *** [pretyping/pretype_errors.cmx] Error 2
make[1]: Leaving directory `/tmp_mnt/rhome/2/richter/Desktop/coq-8.3pl2'

--
Best,
Bill

(poisson)coq-8.3pl2> patch -p1 < inductive-indice-levels-matter-8.3.patch
Hmm... Looks like a unified diff to me...
The text leading up to this was:
--------------------------
|diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
|index df3670d..3e33ffb 100644
|--- a/kernel/indtypes.ml
|+++ b/kernel/indtypes.ml
--------------------------
Patching file kernel/indtypes.ml using Plan A...
Hunk #1 succeeded at 161.
Hunk #2 succeeded at 187.
Hunk #3 succeeded at 224.
Hunk #4 succeeded at 265.
Hmm... The next patch looks like a unified diff to me...
The text leading up to this was:
--------------------------
|diff --git a/kernel/inductive.ml b/kernel/inductive.ml
|index 24b0751..a81531e 100644
|--- a/kernel/inductive.ml
|+++ b/kernel/inductive.ml
--------------------------
Patching file kernel/inductive.ml using Plan A...
Hunk #1 succeeded at 202.
Hmm... The next patch looks like a unified diff to me...
The text leading up to this was:
--------------------------
|diff --git a/kernel/inductive.mli b/kernel/inductive.mli
|index a0fba8e..188a1cb 100644
|--- a/kernel/inductive.mli
|+++ b/kernel/inductive.mli
--------------------------
Patching file kernel/inductive.mli using Plan A...
Hunk #1 succeeded at 88.
done
(poisson)coq-8.3pl2>
(poisson)coq-8.3pl2> patch -p3 < patch.type-in-type
Hmm... Looks like a unified diff to me...
The text leading up to this was:
--------------------------
|diff --git a/branches/v8.3/kernel/reduction.ml b/branches/v8.3/kernel/reduction.ml
|index aa50f78..77e6072 100644
|--- a/branches/v8.3/kernel/reduction.ml
|+++ b/branches/v8.3/kernel/reduction.ml
--------------------------
Patching file kernel/reduction.ml using Plan A...
Hunk #1 succeeded at 183.
done
(poisson)coq-8.3pl2>
(poisson)coq-8.3pl2> patch -p0 < fix-hanging-at-end-of-proof.patch
Hmm... Looks like a unified diff to me...
The text leading up to this was:
--------------------------
|diff -ub coq-8.3pl2-clean/kernel/closure.ml coq-8.3pl2-no-universe-constraints--index-levels-matter/kernel/closure.ml
|--- kernel/closure.ml 2010-07-28 07:22:04.000000000 -0500
|+++ kernel/closure.ml 2011-10-03 14:48:17.000000000 -0500
--------------------------
Patching file kernel/closure.ml using Plan A...
Hunk #1 succeeded at 17.
done
(poisson)coq-8.3pl2>
(poisson)coq-8.3pl2> patch -p0 < grayson-fix-infinite-loop.patch
Hmm... Looks like a unified diff to me...
The text leading up to this was:
--------------------------
|This "fixes" a seemingly infinite loop by abandoning the routine after ten repetitions.
|A better fix would involve understanding what the code was supposed to do.
|
| Dan Grayson
|
|diff -ubr ../coq-8.3pl2-clean/tactics/tactics.ml ./tactics/tactics.ml
|--- ../coq-8.3pl2-clean/tactics/tactics.ml 2011-04-08 11:59:26.000000000 -0500
|+++ ./tactics/tactics.ml 2011-10-07 09:55:24.000000000 -0500
--------------------------
Patching file ./tactics/tactics.ml using Plan A...
Hunk #1 succeeded at 522.
done
(poisson)coq-8.3pl2>
(poisson)coq-8.3pl2> patch -p0 < grayson-improved-abstraction-version2-8.3pl2.patch
Hmm... Looks like a unified diff to me...
The text leading up to this was:
--------------------------
|diff -ur ../coq-8.3pl2-patched/configure ./configure
|--- ../coq-8.3pl2-patched/configure 2011-04-19 02:19:00.000000000 -0500
|+++ ./configure 2011-09-12 18:25:27.000000000 -0500
--------------------------
Patching file ./configure using Plan A...
Hunk #1 succeeded at 6.
Hunk #2 succeeded at 323.
Hmm... The next patch looks like a unified diff to me...
The text leading up to this was:
--------------------------
|diff -ur ../coq-8.3pl2-patched/pretyping/evd.ml ./pretyping/evd.ml
|--- ../coq-8.3pl2-patched/pretyping/evd.ml 2011-03-10 09:50:24.000000000 -0600
|+++ ./pretyping/evd.ml 2011-09-11 06:30:25.000000000 -0500
--------------------------
Patching file ./pretyping/evd.ml using Plan A...
Hunk #1 succeeded at 675.
Hmm... The next patch looks like a unified diff to me...
The text leading up to this was:
--------------------------
|diff -ur ../coq-8.3pl2-patched/pretyping/evd.mli ./pretyping/evd.mli
|--- ../coq-8.3pl2-patched/pretyping/evd.mli 2011-03-10 09:50:24.000000000 -0600
|+++ ./pretyping/evd.mli 2011-09-11 06:30:39.000000000 -0500
--------------------------
Patching file ./pretyping/evd.mli using Plan A...
Hunk #1 succeeded at 224.
Hmm... The next patch looks like a unified diff to me...
The text leading up to this was:
--------------------------
|diff -ur ../coq-8.3pl2-patched/pretyping/pretype_errors.ml ./pretyping/pretype_errors.ml
|--- ../coq-8.3pl2-patched/pretyping/pretype_errors.ml 2010-07-24 10:57:30.000000000 -0500
|+++ ./pretyping/pretype_errors.ml 2011-09-13 16:23:06.000000000 -0500
--------------------------
Patching file ./pretyping/pretype_errors.ml using Plan A...
Hunk #1 succeeded at 34.
Hunk #2 succeeded at 179.
Hmm... The next patch looks like a unified diff to me...
The text leading up to this was:
--------------------------
|diff -ur ../coq-8.3pl2-patched/pretyping/pretype_errors.mli ./pretyping/pretype_errors.mli
|--- ../coq-8.3pl2-patched/pretyping/pretype_errors.mli 2010-07-24 10:57:30.000000000 -0500
|+++ ./pretyping/pretype_errors.mli 2011-09-13 16:22:42.000000000 -0500
--------------------------
Patching file ./pretyping/pretype_errors.mli using Plan A...
Hunk #1 succeeded at 35.
Hunk #2 succeeded at 108.
Hmm... The next patch looks like a unified diff to me...
The text leading up to this was:
--------------------------
|diff -ur ../coq-8.3pl2-patched/pretyping/unification.ml ./pretyping/unification.ml
|--- ../coq-8.3pl2-patched/pretyping/unification.ml 2010-07-26 17:12:43.000000000 -0500
|+++ ./pretyping/unification.ml 2011-09-13 17:03:34.000000000 -0500
--------------------------
Patching file ./pretyping/unification.ml using Plan A...
Hunk #1 succeeded at 28.
Hunk #2 succeeded at 1033.
Hmm... The next patch looks like a unified diff to me...
The text leading up to this was:
--------------------------
|diff -ur ../coq-8.3pl2-patched/pretyping/unification.mli ./pretyping/unification.mli
|--- ../coq-8.3pl2-patched/pretyping/unification.mli 2010-07-24 10:57:30.000000000 -0500
|+++ ./pretyping/unification.mli 2011-09-12 12:27:16.000000000 -0500
--------------------------
Patching file ./pretyping/unification.mli using Plan A...
Hunk #1 succeeded at 52.
Hmm... The next patch looks like a unified diff to me...
The text leading up to this was:
--------------------------
|diff -ur ../coq-8.3pl2-patched/proofs/logic.ml ./proofs/logic.ml
|--- ../coq-8.3pl2-patched/proofs/logic.ml 2010-07-26 17:12:43.000000000 -0500
|+++ ./proofs/logic.ml 2011-09-12 11:47:14.000000000 -0500
--------------------------
Patching file ./proofs/logic.ml using Plan A...
Hunk #1 succeeded at 58.
Hmm... The next patch looks like a unified diff to me...
The text leading up to this was:
--------------------------
|diff -ur ../coq-8.3pl2-patched/tactics/tactics.ml ./tactics/tactics.ml
|--- ../coq-8.3pl2-patched/tactics/tactics.ml 2011-10-11 07:28:57.000000000 -0500
|+++ ./tactics/tactics.ml 2011-10-10 16:38:28.000000000 -0500
--------------------------
Patching file ./tactics/tactics.ml using Plan A...
Hunk #1 succeeded at 134.
Hunk #2 succeeded at 1914.
Hmm... The next patch looks like a unified diff to me...
The text leading up to this was:
--------------------------
|diff -ur ../coq-8.3pl2-patched/test-suite/success/unification.v ./test-suite/success/unification.v
|--- ../coq-8.3pl2-patched/test-suite/success/unification.v 2010-04-07 17:01:23.000000000 -0500
|+++ ./test-suite/success/unification.v 2011-09-12 17:55:41.000000000 -0500
--------------------------
Patching file ./test-suite/success/unification.v using Plan A...
Hunk #1 succeeded at 136.
Hmm... The next patch looks like a unified diff to me...
The text leading up to this was:
--------------------------
|diff -ur ../coq-8.3pl2-patched/test-suite/success/unification2.v ./test-suite/success/unification2.v
|--- ../coq-8.3pl2-patched/test-suite/success/unification2.v 2011-10-11 07:31:05.000000000 -0500
|+++ ./test-suite/success/unification2.v 2011-09-12 18:11:59.000000000 -0500
--------------------------
Patching file ./test-suite/success/unification2.v using Plan A...
Hunk #1 succeeded at 1.
Hmm... The next patch looks like a unified diff to me...
The text leading up to this was:
--------------------------
|diff -ur ../coq-8.3pl2-patched/toplevel/himsg.ml ./toplevel/himsg.ml
|--- ../coq-8.3pl2-patched/toplevel/himsg.ml 2010-09-24 17:23:07.000000000 -0500
|+++ ./toplevel/himsg.ml 2011-09-13 17:07:40.000000000 -0500
--------------------------
Patching file ./toplevel/himsg.ml using Plan A...
Hunk #1 succeeded at 439.
Hunk #2 succeeded at 512.
Hunk #3 succeeded at 862.
done
(poisson)coq-8.3pl2>
(poisson)coq-8.3pl2> patch -p0 < grayson-closedir-after-opendir.patch
Hmm... Looks like a unified diff to me...
The text leading up to this was:
--------------------------
|This patch will leave many few file descriptors unclosed.
|
| Dan Grayson
|
|diff -ur ../coq-8.3pl2-clean/lib/system.ml ./lib/system.ml
|--- ../coq-8.3pl2-clean/lib/system.ml 2010-12-24 03:55:54.000000000 -0600
|+++ ./lib/system.ml 2011-10-14 12:49:30.000000000 -0500
--------------------------
Patching file ./lib/system.ml using Plan A...
Hunk #1 succeeded at 103.
done

[Bill Richter]

> [Is] UF/Coq is superior to plain Coq even in trying to formalize
> the period doubling route to chaos?

Yes. Except there is no "UF/Coq".

That's fantastic, Vladimir, that's what I wanted to hear. BTW the period doubling route to chaos could I think be formalized in HOL Light, as John Harrison has already written so much Multivariate code. But I'd like to say that the formalization will look nicer doing it your way.

There is Coq and there is a way to encode mathematical concepts in
Coq which is compatible with UF.

Hmm, that's what I meant by "UF/Coq". What should I say instead? Coq using UF is superior to vanilla Coq in formalizing the period doubling route to chaos?


Bas, I saw your slide show before, and I didn't get anything out of it. I seem to lack many skills folks here have. I think I can be a valuable UF contributor, being a good mathematician abnormally interested in mathematical rigor, and having worked on HOL Light code for 2 years now. But I don't know anything about toposes or ITT, and I'm impressed that folks here do. I'll learn it eventually.

--
Best,
Bill

[Bill Richter]

You are not being clear. On which machines have you succeeded in
installing patched Coq + Foundations and on which you have not?

[Bill Richter]

Andrej, your blog post was very helpful
http://math.andrej.com/2014/01/13/univalent-foundations-subsume-classical-mathematics/
I think you're saying that UF handles classical math because LEM/AC are only apply to (-1)-types and 0-types, as LEM/AC are really only questions about logic and sets. And I think you explained that n-types for n > 0 buys you Postnikov towers of degree (height?) n, so UF should be good for homotopy theory. OK, that's great.

But your post didn't explain why UF is a good thing for formalizing calculus type results like the period doubling route to chaos. I would naively have thought that the way to formalize calculus was with sets, and that's (-1)-type logic applied to 0-types. However, Vladimir posted that UF would help for calculus. And I'm guessing that means that either that higher dimensional groupoids must help either with the logic or with set-type constructions like topological spaces. I haven't gotten far enough into the HoTT book to tell.

I feel like we're talking a bit past you.

I think so.

For instance, have you read that answer of Mike Shulman's to the
question "why worry about axiom of choice"? It precisely addresses
your questions of why a classical mathematician should care about
choice. But you never commented on it, so I do not know what else
we can offer as an answer.

There's no point in you convincing me that UF is good for pure math, and that it's good to think constructively, and it's good to give constructive proofs even in a subject full of non-constructive result. I'm sure that's all true, even if I don't understand it yet. What I want you to help me understand, by May, is how to explain UF to HOL programmers. So I'd like to know why UF would improve the proofs of in the 8484KB directory Multivariate of HOL Light which you can get download
svn checkout http://hol-light.googlecode.com/svn/trunk/ hol_light
I've rewritten (in directory RichterHilbertAxiomGeometry) maybe 1/10 of the file 19,000 line file Multivariate/topology.ml, and I don't see how you could improve on my coding. Now I haven't done any functions yet, and it's a problem in HOL to say there's a unique function between two sets (as opposed to types) having a certain property. So I can see how Coq DT would help with coding up function uniqueness stuff, but so far, I don't have any inkling about why UF will help. I can figure this out without anyone's help, of course, by reading the HoTT book. But I'd like to know now, if there's a simple explanation. I know it's true, at least, because Vladimir said it was.

--
Best,
Bill