[FOM] Eradicating Evil?

Tue Oct 28 20:40:12 EDT 2014

On Oct 27, 2014, at 6:01 AM, Harvey Friedman <hmflogic at gmail.com> wrote:

> My back channels tell me that there is a crusade to "eradicate evil"
> spearheaded by the HoTT community.

Steve Awodey wrote:

"This is absolute rubbish and a good example of what is wrong with FOM.
It is impossible to have a civil discussion here about anything *new*
in foundations
without being accused of being a “crazy”, “radical”, “zealot”, etc.

Why does everything on this list have to be a fight?
I’m tired of the gauntlets, challenges, accusations, personal attacks, etc.,
especially the ones beginning “without knowing anything about X, here
is what I think about X …”.

Those who are honestly interested in learning about Homotopy Type Theory
— and I recommend it to readers of this list as a new area of
foundational research
with many interesting connections to mathematics, logic, and computer science —
should have no trouble finding resources online, particularly the already cited:

www.homotopytypetheory.org

and the book available there.
The current discussion, by contract, has no informational value, and
shows no signs of heading in that direction.

After many years on this list, I have finally had enough.
When you have finally succeeded in driving out everyone with a
different point of view,
then you will be free to vilify them without rebuttal.

Good bye, and good luck with this forum,"

I am interested in the claim in the press and from radicals that "this
is a revolution in the foundations of mathematics". So I am assuming
that this is supposed to be general purpose. I am interested in
hearing, in generally understandable terms, just what general purpose
is being revolutionized, just what the reasons why this promises to
overthrow the Standard Umbrella, and so forth. I can already relate to
at least some of the complaints about the Standard Umbrella that are
generally understandable. I have already been spurred to rethink my
previous work on "flat mental pictures" in

https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
84. Flat Mental Pictures, September 5, 2014, 5 pages. Extended abstract.

in terms of what I now call "flat foundations". I already posted some
initial stuff about it on the FOM, but now am planning to soon post a
series on it on my numbered postings. I think that it is SOMEWHAT
responsive to the "speak no evil" imperative, but I would not expect
it to be FULLY responsive. For that, I need some interaction with
people like Steve Awodey - in GENERALLY UNDERSTANDABLE terms. If Steve
genuinely believes that HoTT is really general purpose, then Steve
ought to engage in a dialog in order to make my "flat foundations" yet
MORE RESPONSIVE. If Steve won't interact this way, perhaps somebody
else will?

SPEAK NO EVIL

The term "speak no evil" appears in the index of the HoTT book, but
apparently not in the text.

It seems to have been introduced by John Baez.

Here are some links:

https://golem.ph.utexas.edu/category/2013/03/category_theory_in_homotopy_ty.html

Thus, since in a saturated category, equality of objects is identified
with isomorphism, it follows that any construction we can perform must
also respect isomorphism of objects. So working with a saturated
category provides an ironclad guarantee of “non-evilness”: if you can
state your definition or prove your theorem for saturated categories
in HoTT, then it is automatically isomorphism-invariant.

The thing which I like so much about this approach is that it allows
multiple kinds of category theory to coexist. People who prefer to
“speak no evil” can work with saturated categories, and almost all of
classical category theory will work just as it does classically (or
even better), since it is well-known to satisfy the principle of
equivalence.

http://permalink.gmane.org/gmane.science.mathematics.categories/5858

If you take a strictly speak-no-evil approach to category theory
(perhaps even going so far as to found your mathematics on FOLDS),
then it is impossible to state that two categories are isomorphic,
because you must speak of equality of objects (or functors) to do this.
In this approach, Cat and Cat/Set are bicategories but not categories.

But it IS still possible to state that two concrete categories are isomorphic;
the bicategory Conc is (up to equivalence) a locally posetal bicategory
(so if you ignore the non-invertible transformations, it's a category).
So it is possible (and necessary) to say, even when you speak no evil,
that all of Marco's examples are concrete isomorphisms.

So I agree that it is important that these are not mere equivalences,
but I claim (playing the role of an equality-is-evil partisan)
that what is important is not so much that they are isomorphisms
as that they are concrete.

http://ncatlab.org/michaelshulman/show/internal+logic+of+a+2-category

In particular, note that equality, as a proposition, is only defined
between elements of a 0-type. Thus, our language doesn’t even have the
terminology to speak about equality between objects of a 1-type
(category), only equality between elements of a 0-type (such as arrows
in a category). This is also known as the “Speak No Evil” approach to
category theory.

But if thought corrupts language, language can also corrupt thought. –
George Orwell

http://ncatlab.org/nlab/show/SEAR

Implicit in the existence of three types of things is that nothing is
both a set and an element, etc., so in particular a statement such as
x=A is not well-formed if x is an element and A a set. Furthermore,
SEAR does not include an equality relation between sets: even if A and
B are both sets we do not consider A=B to be well-formed. (Thus SEAR
adheres to the philosophy of “speak no evil.”)

Exercise: why is adherence to “speak no evil” necessary for Axiom 5 to
be reasonable as stated?

http://ncatlab.org/nlab/show/principle+of+equivalence

Terminology

Michael Makkai proposed the Principle of Isomorphism, “all
grammatically correct properties of objects of a fixed category are to
be invariant under isomorphism”, in his paper “Towards a categorical
foundation of mathematics”, in Johann A. Makowsky, Elena V. Ravve,
eds., Logic Colloquium ‘95: Proceedings of the Annual European Summer
Meeting of the Association of Symbolic Logic, held in Haifa, Israel,
August 9-18, 1995 (Berlin: Springer-Verlag, 1998), 153-190.

Peter Aczel mentioned a similar concept, the Structure Identity
Principle, “isomorphic structures have the same structural properties”
in Oberwolfach report 52/2011. This seems a priori a little weaker
tome, but if we demand that objects should be seen as only having
structural properties (as opposed to the category of ZF-sets), then we
look like we get back the Principle of Isomorphism.

A very precise way of stating this idea is encapsulated in Vladimir
Voevodsky’s univalence axiom, which is a fundamental part of homotopy
type theory as a foundation for mathematics. By identifying
equivalences/isomorphisms with inhabitants of an identity type, it
ensures that all properties and structure which can be expressed
within the formal type theory are invariant under such.

Floating around the web (and maybe the nLab) is the idea of
half-jokingly referring to a breaking of equivalence invariance as
“evil”. This is probably meant as a pedagogical way of amplifying that
it is to be avoided.
Defining higher categorial structures using such ‘evil’ equalities
tends to lead to strict concepts; avoiding them and imposing coherence
relations leads to weak concepts.

https://golem.ph.utexas.edu/category/2009/09/towards_a_computeraided_system.html

Of course, set-theoretic foundations are perhaps not philosophically
in line with category theory, which may be more along the lines of
what McLarty is getting at. For instance, there is the problem of
evil: as long as your categories have sets of objects, you’ll be able
to talk about equality of those objects. But I don’t see any way to
solve that unless your foundational axioms are really about the
2-category of categories; even the 1-category of categories isn’t good
enough.

(Strictly speaking, I have just said something “evil”, but I am not
going to worry about this on first pass.)

AND many more in this link.

Here are some other links, without excerpts.

http://ncatlab.org/nlab/show/principle+of+equivalence

http://comments.gmane.org/gmane.science.mathematics.categories/5459

http://comments.gmane.org/gmane.science.mathematics.categories/5462

The terminology "speak no evil" has caused some controversy e.g. among fans of
fibrations. See e.g.

http://ncatlab.org/nlab/show/Grothendieck+fibration

Harvey Friedman