HoTT applied to something other than topology

[Andrew Dabrowski]

Could someone please point me to a good treatment of a subject besides topology using HoTT? 

Or alternately, could someone describe how the addition of homotopy to types makes the language so much more expressive that practical proof assistants are now thought to be within range?

I've just started chapter 6 of the HoTT Book and I'm thinking maybe higher inductive types are supposed to be the killer app.  But (1) it's not clear that the general notion of HIT really requires homotopy rather than some other more generic addition to type theory and (2) as usual the first half dozen examples in the book are drawn from topology where it's hard to judge how much of the power is general and how much dependent on the synergy of using using homotopy to study homotopy.

[Alexander Altman]

Oddly enough, the last four chapters of the HoTT Book are all about applications, and three out of the four have nothing to do with topology (or, rather, only as much to do with topology as everything in mathematics does).

[Michael Shulman]

On Sun, Oct 22, 2017 at 1:28 PM, Andrew Dabrowski <unhan...@gmail.com> wrote:
> Or alternately, could someone describe how the addition of homotopy to types
> makes the language so much more expressive that practical proof assistants
> are now thought to be within range?

I don't know where you heard this, but IMHO it is a serious
exaggeration. HoTT is an *incremental* improvement to type theory; it
remedies certain infelicities with previously-existing type theories
(in addition to making possible entirely new kinds of mathematics),
but in terms of the practical utility of proof assistants to the
everyday mathematician it is only one small step along a very long
road.

Many other steps along that road have already been taken, as witnessed
by the recent verification of several big-name theorems like the
four-color theorem, the odd-order theorem, and the Kepler conjecture.
But my own opinion is that many more such steps remain to be taken,
most of which are essentially software engineering problems rather
than mathematical ones.

You might be interested in these blog posts of mine:
https://golem.ph.utexas.edu/category/2015/05/the_revolution_will_not_be_for.html
https://golem.ph.utexas.edu/category/2015/06/whats_so_hott_about_formalizat.html

[Andrew Dabrowski]

Thanks, those articles are good antidotes to what I'd read elsewhere, e.g. that Voevodsky had forever changed the meaning of "=".

About that.  It seems that in HoTT the notion of homotopy equivalence has become the notion of "=".  I can see how that that makes HoTT a good system for doing homotopy theory, but is that really an idea that all mathematicians could get on board with?  I'm anxious to start on the last chapters of the HoTT Book to see how it plays out for other fields, but at the moment I'm skeptical that HoTT is going to prove a boon to algebra and logic.

Could you try to describe for a non-expert why homotopy theory adds to type theory something of more general interest?  Or do you think that is also an exaggeration?  Is it possible that each field of math could require its own comparable breakthrough to get from type theory the benefits that topology gets from HoTT?

[Gershom B]

On Mon, Oct 23, 2017 at 12:10 PM, Andrew Dabrowski
<unhan...@gmail.com> wrote:
> Thanks, those articles are good antidotes to what I'd read elsewhere, e.g.
> that Voevodsky had forever changed the meaning of "=".

I think both can be true. Univalent equality is a more general notion
than standard (propositional) equality, which can truncate back down.
Even if we're only interested in working with propositional equality
in a given setting, understanding the richer structure behind it is of
some use, and the introduction of the univalence axiom clarified a
great deal that was known, but not systematized the same way about the
structure of intensional type theories in general, including those
permitting axioms which contradict univalence.

But that doesn't mean that to do topology one _must_ work using the
homotopical interpretation of equality as the way to model homotopy
spaces. And if you do not, then it is indeed just an incremental
improvement, albeit one that helps in the general project in a useful
way. And so from the standpoint of other branches of mathematics, it
should help in just about the same (incremental) way.

> I'm anxious to start on the last
> chapters of the HoTT Book to see how it plays out for other fields, but at
> the moment I'm skeptical that HoTT is going to prove a boon to algebra and
> logic.

Logic is one of the places that constructive type theories have
already had a huge impact, well before HoTT, due to the deep
correspondence between type theory and logic that dates to the
metamathematics of the mid-20th century, and more directly of course
to Howard, and then Martin-Lof. I'm curious about algebra myself -- I
don't know enough about the state of the art to have any good
understanding of where its current pain points lie. My understanding
is that algebraists have been quite open to using computer assistance
in long and technical calculations. The gap there is between those
computer algorithms and any formal verification of them, and I suppose
people would be interested in closing that, though I don't know how
many. So I would be interested, if anyone can speak to it, of the
impact of the formalization of Feit-Thompson in broader mathematical
circles -- or if there was not much of one.

> Could you try to describe for a non-expert why homotopy theory adds to type
> theory something of more general interest? Or do you think that is also an
> exaggeration? Is it possible that each field of math could require its own
> comparable breakthrough to get from type theory the benefits that topology
> gets from HoTT?

There is a general sort of sentiment that there is more homotopical
structure around in more things than people have seen in the past (see
this interview with Manin:
https://golem.ph.utexas.edu/category/2009/11/interview_with_manin.html).
So one speculation might be that as more mathematics moves towards
wanting to work with higher n-structures, then the need for tools
(both formal and informal) that speak higher things as their native
tongue will increase. But this is a very long-term speculation, of
course.

Cheers,
Gershom

[Andrew Dabrowski]

Thanks for directing me to that excellent interview with Manin. 

Manin:

I am pretty strongly convinced that there is an
ongoing reversal in the collective consciousness of
mathematicians: the right hemispherical and ho-
motopical picture of the world becomes the basic
intuition, and if you want to get a discrete set, then
you pass to the set of connected components of a
space defined only up to homotopy.
That is, the Cantor points become continuous
components, or attractors, and so on—almost from
the start. Cantor’s problems of the infinite recede
to the background: from the very start, our images
are so infinite that if you want to make something
finite out of them, you must divide them by an-
other infinity.

Makes me almost regret I never studied topology. 

[Michael Shulman]

On Mon, Oct 23, 2017 at 9:10 AM, Andrew Dabrowski <unhan...@gmail.com> wrote:
> About that. It seems that in HoTT the notion of homotopy equivalence has
> become the notion of "=". I can see how that that makes HoTT a good system
> for doing homotopy theory, but is that really an idea that all
> mathematicians could get on board with?

As Gershom pointed out, homotopy theory (or, equivalently, higher
category theory) is starting to infect more and more of mathematics.
However, even in areas to which it has not yet metastasized, there is
no "getting on board" necessary, since one can simply ignore all the
unneeded higher homotopy types and work only with the sets.

(There are a few *possible* exceptions to this, such as ZF set theory,
but describing the relation between HoTT and ZF would be an entire
other thread.)

> Could you try to describe for a non-expert why homotopy theory adds to type
> theory something of more general interest? Or do you think that is also an
> exaggeration?

For a mathematician whose subject area uses nothing homotopical or
category-theoretic, I would say that the main thing that HoTT adds to
type theory is that it fixes certain problems with type theory that
you probably never would have believed existed if you hadn't used it
before. In vanilla Coq, for instance, (1) two functions can take the
same values on all inputs without being equal as functions, (2) two
subsets of a set can contain the same elements without being equal as
subsets, and (3) there is no good way to define the quotient of a set
by an equivalence relation. To the ordinary mathematician these are
bizarre restrictions that make type theory almost unusable as a
foundation for mathematics. Type theorists have developed various
workarounds, such as working with "setoids", but HoTT actually *fixes*
these problems.

A less important, but nontrivial, benefit of HoTT even for the
non-homotopically-inclined mathematician is the notion of higher
inductive type. The general type-theoretic notion of "inductive type"
deserves to be much better known in mathematics. Many mathematical
objects are naturally defined as inductive types -- or at least they
would be, if mathematicians knew what general inductive types were and
didn't feel obligated to butcher all inductive proofs to force them to
induct over natural numbers (or more generally ordinal numbers) rather
than arbitrary inductive types. (-: Higher inductive types make
inductive types even more powerful by essentially allowing the
quotient by an equivalence relation to happen as part of the inductive
definition.

> Is it possible that each field of math could require its own
> comparable breakthrough to get from type theory the benefits that topology
> gets from HoTT?

I think *require* is too strong of a word. But I do think that at
least some other fields of math can or could be usefully treated
"synthetically", in an analogous way to how HoTT treats homotopy
theory "synthetically". For some fields such a theory exists already,
such as synthetic differential geometry (SDG), synthetic topology, or
synthetic domain theory; for others it remains to be developed.

I do also believe HoTT is somewhat special in this regard, though,
because homotopy theory and higher category theory are really about
the most fundamental structure of mathematics, specifically what it
means for two things to be "equal". It generally seems to be the case
that the enhancements of HoTT are useful (albeit in a more limited
way, as described above) when doing all kinds of mathematics, not just
synthetic homotopy theory; whereas the axioms of most other synthetic
theories are restricted in usefulness to that subject area.

> Makes me almost regret I never studied topology.

It's never too late! HoTT is actually not a bad way to learn homotopy
theory (which should be distinguished from "topology", as the latter
studies spaces up to homeomorphism rather than just homotopy
equivalence).

[Urs Schreiber]

These are great replies by Mike Shulman.

Since these kinds of questions will keep being asked, it would be
really useful to organize the replies (these and more) into an FAQ.
Maybe this rudiment FAQ here would be worth expanding:

https://ncatlab.org/nlab/show/homotopy+type+theory+FAQ

Best wishes,
urs

> --
> You received this message because you are subscribed to the Google Groups
> "HoTT Cafe" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to hott-cafe+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>

[Matt Oliveri]

On Tuesday, October 24, 2017 at 12:30:50 AM UTC-4, Michael Shulman wrote:

On Mon, Oct 23, 2017 at 9:10 AM, Andrew Dabrowski <unhan...@gmail.com> wrote:
> About that.  It seems that in HoTT the notion of homotopy equivalence has
> become the notion of "=".  I can see how that that makes HoTT a good system
> for doing homotopy theory, but is that really an idea that all
> mathematicians could get on board with?

As Gershom pointed out, homotopy theory (or, equivalently, higher
category theory) is starting to infect more and more of mathematics.
However, even in areas to which it has not yet metastasized, there is
no "getting on board" necessary, since one can simply ignore all the
unneeded higher homotopy types and work only with the sets.

(There are a few *possible* exceptions to this, such as ZF set theory,
but describing the relation between HoTT and ZF would be an entire
other thread.)

We should have that entire other thread. In ZF, the collection of all small sets is a large set. In HoTT, it's not a set at all, it's a 1-type. This makes HoTT more general, but harder to use. If, for most mathematicians, the extra generality is unhelpful, then HoTT may be perceived as imposing undue difficulties, and be rejected. So I would think it's not so easy to get on board with the HoTT approach.

If HoTTheorists want to actually work to "sell" their approach to the rest of the math community, they should be explaining how to work around this difficulty, starting, like, years ago. And/or they need to show how univalence is strictly more useful than a (large) set of all (small) sets. The facts that all (small) *Zermelo-style* sets *do* form a (large) set, and that univalence makes isomorphic structured sets formally interchangeable are great selling points. They show that, while different, the HoTT perspective 1) isn't broken, and 2) can be useful.

> Could you try to describe for a non-expert why homotopy theory adds to type
> theory something of more general interest?  Or do you think that is also an
> exaggeration?

For a mathematician whose subject area uses nothing homotopical or
category-theoretic, I would say that the main thing that HoTT adds to
type theory is that it fixes certain problems with type theory that
you probably never would have believed existed if you hadn't used it
before.  In vanilla Coq, for instance, (1) two functions can take the
same values on all inputs without being equal as functions, (2) two
subsets of a set can contain the same elements without being equal as
subsets, and (3) there is no good way to define the quotient of a set
by an equivalence relation.  To the ordinary mathematician these are
bizarre restrictions that make type theory almost unusable as a
foundation for mathematics.  Type theorists have developed various
workarounds, such as working with "setoids", but HoTT actually *fixes*
these problems.

I completely disagree with this. Anyone who formalizes mathematics in a system without extensionality and quotients will feel the pain. It's not like they won't know what they're missing. That seems almost implausible. Moreover, HoTT is excessive as a way to provide set-level extensionality principles. Type theorists have been assuming extensionality principles for decades. HoTT is not the first, simplest, or most convenient way to get set-level extensionality.

A less important, but nontrivial, benefit of HoTT even for the
non-homotopically-inclined mathematician is the notion of higher
inductive type.  The general type-theoretic notion of "inductive type"
deserves to be much better known in mathematics.  Many mathematical
objects are naturally defined as inductive types -- or at least they
would be, if mathematicians knew what general inductive types were and
didn't feel obligated to butcher all inductive proofs to force them to
induct over natural numbers (or more generally ordinal numbers) rather
than arbitrary inductive types.  (-: Higher inductive types make
inductive types even more powerful by essentially allowing the
quotient by an equivalence relation to happen as part of the inductive
definition.

I completely agree with this!

> Is it possible that each field of math could require its own
> comparable breakthrough to get from type theory the benefits that topology
> gets from HoTT?

[...]

I do also believe HoTT is somewhat special in this regard, though,
because homotopy theory and higher category theory are really about
the most fundamental structure of mathematics, specifically what it

means for two things to be "equal"...

I basically agree with this, except I would say homotopy is about "interchangeability" in general, not "equality" in general. The surprise is that the axiomatization of "equality" we all learned is actually an axiomatization of interchangeability, but this only becomes apparent when proofs are allowed to be nontrivial mathematical objects.

[Andrew Dabrowski]

Thanks for fleshing that out so well.  Some more dumb questions:

It might be too late for me to learn homotopy theory - my mind is very discrete.  I was thrown recently by the possibility that a function on a singleton domain could fail to be continuous.  I'm not convinced the homotopical notion of continuity is really necessary in type theory.

The fixing of problems in type theory does seem important and I want to think about that more.  But there are other ways of handling extensionality (e.g. Axcel's bisimulations) without homotopy theory, no?

Is homotopy really required for HITs?  I'm probably missing something important: is there more to HITs than structural recursion on well-founded objects?

[Michael Shulman]

On Tue, Oct 24, 2017 at 11:49 AM, Matt Oliveri <atm...@gmail.com> wrote:
> We should have that entire other thread. In ZF, the collection of all small
> sets is a large set. In HoTT, it's not a set at all, it's a 1-type. This
> makes HoTT more general, but harder to use.

No mathematicians that I know of actually use this fact about ZF-sets,
except for ZF-theorists (and as you pointed out, the collection of
ZF-sets does form a set). So in practice, it isn't actually any
harder to use. This is not something particular to HoTT either; it's
also true about other "structural" foundations like ETCS, and has been
explained many times.

> Anyone who formalizes mathematics in a system without extensionality
> and quotients will feel the pain.

That's what I said.

> It's not like they won't know what they're missing.

I didn't say they wouldn't.

> Moreover, HoTT is excessive as a way to provide set-level extensionality
> principles. Type theorists have been assuming extensionality principles for
> decades. HoTT is not the first, simplest, or most convenient way to get
> set-level extensionality.

It's true that HoTT with univalence as an axiom is no better as a way
to obtain function extensionality and propositional extensionality
than by assuming them as separate axioms. But cubical type theory
gives a *computational* way to get both of these principles; this is
approached by other type theories like OTT but not, as far as I can
tell, as conveniently. In particular, as far as I understand it,
OTT's "propositions" are a separate universe rather than defined as
h-props, which is an approach that generally breaks the function
comprehension principle.

Moreover, I do believe that the rules for propositional truncation and
quotients derived from the HIT perspective are the simplest, most
convenient, and most correct ones, and these rules were not widely
accepted in type theory prior to HoTT.

[Michael Shulman]

On Tue, Oct 24, 2017 at 11:58 AM, Andrew Dabrowski
<unhan...@gmail.com> wrote:
> I'm not convinced the
> homotopical notion of continuity is really necessary in type theory.

It's misleading to think of homotopy theory as being about
"continuity". It's actually about sameness (which most of us call
simply "equality", although apparently some people prefer to split
hairs), and sameness is basic to any mathematical foundation.

> Is homotopy really required for HITs? I'm probably missing something
> important: is there more to HITs than structural recursion on well-founded
> objects?

Structural recursion on well-founded objects is *ordinary* inductive
types. Higher inductive types allow inductive quotienting as well as
generation, and the resulting object doesn't necessarily admit any
well-founded relation.

HITs make sense without homotopy theory, but they were invented by
homotopical intuition. Moreover, to prove basic things about HITs one
generally requires at least a limited form of univalence to make
"large elims" on HITs possible.

[Andrew Dabrowski]

On Tuesday, October 24, 2017 at 3:31:15 PM UTC-4, Michael Shulman wrote:

HITs make sense without homotopy theory,

Then shouldn't it be possible to make a type theory with HITs without using homotopy?

I have to read up on HITs, I don't understand why adding equivalence classes to the construction makes recursion qualitatively more difficult.  Surely they've been doing that kind of thing in model theory for a long time?

but they were invented by
homotopical intuition.  Moreover, to prove basic things about HITs one
generally requires at least a limited form of univalence to make
"large elims" on HITs possible.

Univalence has been described as type extensionality.  In that sense homotopy wouldn't seem necessary for univalence either.  I mentioned that Aczel developed a theory of nonwell-founded sets 30 years ago that might provide a model for extensionality in type theory.

I can see how HoTT seems fantastic to homotopy theorists.  But I still do not see why it shouldn't be possible to formulate a type theory with all the best bits of HoTT but without the homotopy semantics that may alienate mathematicians in other fields. 

 

[Matt Oliveri]

On Tuesday, October 24, 2017 at 3:27:44 PM UTC-4, Michael Shulman wrote:

On Tue, Oct 24, 2017 at 11:49 AM, Matt Oliveri <atm...@gmail.com> wrote:
> Anyone who formalizes mathematics in a system without extensionality
> and quotients will feel the pain.

That's what I said.

> It's not like they won't know what they're missing.

I didn't say they wouldn't.

You wrote:
> I would say that the main thing that HoTT adds to

type theory is that it fixes certain problems with type theory *that

you probably never would have believed existed if you hadn't used it

before*.  In vanilla Coq, for instance, (1) two functions can take the

same values on all inputs without being equal as functions, (2) two
subsets of a set can contain the same elements without being equal as
subsets, and (3) there is no good way to define the quotient of a set
by an equivalence relation.

(Emphasis added)

I think I misinterpreted this. I thought you meant "if you hadn't used HoTT before". In other words, you could use regular MLTT without seeing a problem. But now that I reread it, I suppose you meant "if you hadn't used plain MLTT before". In other words, without seeing it first hand, you wouldn't believe such a painful system was used. :)

[Matt Oliveri]

On Tuesday, October 24, 2017 at 3:27:44 PM UTC-4, Michael Shulman wrote:

On Tue, Oct 24, 2017 at 11:49 AM, Matt Oliveri <atm...@gmail.com> wrote:
> We should have that entire other thread. In ZF, the collection of all small
> sets is a large set. In HoTT, it's not a set at all, it's a 1-type. This
> makes HoTT more general, but harder to use.

No mathematicians that I know of actually use this fact about ZF-sets,
except for ZF-theorists (and as you pointed out, the collection of
ZF-sets does form a set).  So in practice, it isn't actually any
harder to use.  This is not something particular to HoTT either; it's
also true about other "structural" foundations like ETCS, and has been
explained many times.

I'm afraid that when it comes to popularity of approaches to mathematics, it doesn't matter whether regular mathematicians *actually* need small sets to form a set. What matters is whether mathematicians *think* it's important for small sets to form a set. If I had a dollar for each time a programmer chooses a bad programming language because they didn't know better...

I thought in ETCS, collections of sets don't exist. So yeah, small sets don't form a set. They don't form anything.

Anyway, I have an example of how it's useful if small sets form a set: there is a canonical choice of set-level universe to use in a model of ETCS + a universe.

[Michael Shulman]

You can certainly add HITs to type theory but not force yourself into
homotopy models. But you can't do that with univalence; univalence is
what forces types with higher homotopy to exist. I do encourage you
to stop thinking of "homotopy" as meaning something topological that
you find alienating, and start thinking of it instead as just the
natural thing that happens when you start thinking seriously about
representing things like equality and isomorphism, as they are used
*all over* mathematics, faithfully inside a foundational system. I
wrote a bunch about this at https://arxiv.org/abs/1601.05035 .

[Matt Oliveri]

On Tuesday, October 24, 2017 at 3:27:44 PM UTC-4, Michael Shulman wrote:

On Tue, Oct 24, 2017 at 11:49 AM, Matt Oliveri <atm...@gmail.com> wrote:
> Moreover, HoTT is excessive as a way to provide set-level extensionality
> principles. Type theorists have been assuming extensionality principles for
> decades. HoTT is not the first, simplest, or most convenient way to get
> set-level extensionality.

It's true that HoTT with univalence as an axiom is no better as a way
to obtain function extensionality and propositional extensionality
than by assuming them as separate axioms.  But cubical type theory
gives a *computational* way to get both of these principles; this is
approached by other type theories like OTT but not, as far as I can
tell, as conveniently.  In particular, as far as I understand it,
OTT's "propositions" are a separate universe rather than defined as
h-props, which is an approach that generally breaks the function
comprehension principle.

Wait, you're saying OTT's approach breaks the function comprehension principle? And does "function comprehension principle" refer to a unique choice operator?

Moreover, I do believe that the rules for propositional truncation and
quotients derived from the HIT perspective are the simplest, most
convenient, and most correct ones, and these rules were not widely
accepted in type theory prior to HoTT.

I agree with this. But mind the difference between h-props and proof-irrelevant props. HoTT doesn't provide the latter, except with double-negation. (This is probably fixable.) CTT and OTT both provide a working notion of intuitionistic, proof-irrelevant proposition. Via quotients, they also provide an h-prop-like notion, which unfortunately does not have propositional extensionality.

[Michael Shulman]

Yes, function comprehension is basically equivalent to unique choice

I'm not enough of an expert on OTT to pronounce on it definitively.
But the only reference I've seen for propositional extensionality in
OTT involves a special "universe of propositions" that satisfies
extensionality, rather than the HoTT way of *defining* propositions as
(-1)-types, and most type theories I've encountered that have such a
"universe of propositions" (e.g. Coq's Prop, logic-enriched type
theory, the internal logic of a quasitopos) fail to have function
comprehension / unique choice relative to it, whereas with
propositions defined as (-1)-types (and HoTT-style propositional
truncation) function comprehension is provable.

I don't know of any reason why a *mathematician* (intuitionistic or
not) would want any kind of proposition that is any more
proof-irrelevant than an h-prop. (I understand that programmers like
to be able to tag certain things as "erasable at run-time", although
I'm not sure that such tags need to be the same as "propositions".)

[Matt Oliveri]

On Tuesday, October 24, 2017 at 3:31:15 PM UTC-4, Michael Shulman wrote:

On Tue, Oct 24, 2017 at 11:58 AM, Andrew Dabrowski
<unhan...@gmail.com> wrote:
> I'm not convinced the
> homotopical notion of continuity is really necessary in type theory.

It's misleading to think of homotopy theory as being about
"continuity".  It's actually about sameness (which most of us call
simply "equality", although apparently some people prefer to split
hairs), and sameness is basic to any mathematical foundation.

In case you mean me, by "sameness" and "equality", I mean the relation axiomatized in HoTT as judgmental equality. By "interchangeability", I mean the identity type. I remember that you prefer a different perspective. I don't like calling the identity types "equality", because then some terms are more equal than others. That seems destined to cause confusion.
 

Moreover, to prove basic things about HITs one
generally requires at least a limited form of univalence to make
"large elims" on HITs possible.

In a theory with UIP, do HITs require anything beyond function extensionality?

[Michael Shulman]

On Tue, Oct 24, 2017 at 2:36 PM, Matt Oliveri <atm...@gmail.com> wrote:
>> Moreover, to prove basic things about HITs one
>> generally requires at least a limited form of univalence to make
>> "large elims" on HITs possible.
>
> In a theory with UIP, do HITs require anything beyond function
> extensionality?

Yes, for some results you need at least propositional extensionality.
See for instance Lemma 10.1.4, Definition 10.5.4, and Theorems 11.3.16
and 11.6.7 in the HoTT book. These are all "encode-decode proofs"
that live entirely in the world of h-sets, but for defining the codes
family they require large elims into the universe of propositions,
hence propositional extensionality.

[Matt Oliveri]

For a mathematician, I don't know of any reason either. With extrinsic typing, proof-irrelevant propositions automatically arise as reflected judgments. It can be convenient to use them, when they're sufficient. I don't claim that they're mathematically important. (For erasure, as long as it's set up so that something constructed by unique choice on an erased h-prop is also erased, it sounds good to me.)

[Matt Oliveri]

You can have type extensionality principles in type theory based on membership. So they'd be similar to set extensionality from ZF or Aczel's nonwellfounded variant. However, most forms of type theory can't even *express* this sort of principle, because reasoning about membership in types is not allowed. From what I understand, reasoning about membership is not considered meaningful from a structuralist perspective, because it doesn't respect isomorphism. Univalence is a type extensionality principle that's (very) compatible with structuralism.

Nuprl is able to express membership-based type extensionality, but the Nuprl designers decided not to assume it.

[Andrew Dabrowski]

Thanks, I've downloaded your paper, I'll look at it later today.

But surely the notion of continuity in HoTT is much stricter than in other fields.  For example, in real analysis a function on a singleton domain could never fail to be continuous.  But in HoTT maps must be continuous also w.r.t. the internal structure of elements in the domain.  That degree of strictness not something I'd seen before.

Also, there are some fields of mathematics that are hardly concerned with continuity at all (e.g. logic, pure algebra).

[Michael Shulman]

If you're referring to maps out of types like the circle, which must
also act on the nontrivial paths, then the answer is that you should
not think of S^1 as a "singleton". The only true singleton is the
unit type, and it should still be true that "every map out of the unit
type is continuous" in whatever sense that makes sense (although
offhand I can't think of any such sense, since there is no notion of
"discontinuous map" in HoTT).

HoTT also doesn't force you to use homotopy theory; the subuniverse of
sets behaves mostly like it does in ordinary mathematics. The
homotopy theory is there only if you want it, and certainly for some
fields you don't.

[Andrew Dabrowski]

I was thinking of that example in Lemma 3.8.5 in which a singleton type X was constructed but the type

\Pi_{x:X}(x_0=x)

is uninhabited, because no such map would be continuous.  The intuition behind that is pure homotopy theory.

[Michael Shulman]

That X is not a singleton either, for the same reasons as S^1.

On Thu, Oct 26, 2017 at 11:50 AM, Andrew Dabrowski

[Andrew Dabrowski]

Oh, when you said that X does satisfy

\Pi_{x:X} ||x_0=x||

I took that to mean that X is a singleton, but I see now I was wrong.  In HoTT, = does not mean identical.  That of course in itself is extremely confusing for nonhomotopists.

[Andrej Bauer]

> (although offhand I can't think of any such sense, since there is no notion of
> "discontinuous map" in HoTT).

Discontiuous maps from classical mathematics can be represented
constructively as partial maps with ¬¬-dense domains. For example, the
classical sign map sgn : R → {-1,0,1}, defined classically as

sgn(x) = -1 if x < 0
sgn(0) = 0
sng(x) = 1 if x > 0

can be thought of constructively as a *partial* map defined on the subset

D = {x ∈ R | x < 0 ∨ x = 0 ∨ x > 0}

The set D is ¬¬-dense in the sense that R \ D = ∅.

Can we translate these ideas to HoTT? It looks like truncation is
doing some of the work that ¬¬-density is doing constructively.

With kind regards,

Andrej

[Michael Shulman]

I say that = does mean identical. There is no stronger notion of
"sameness" inside the theory than = that could be meant by
"identical". Terms that are = are not necessarily *syntactically*
identical, but that's an external notion, and also the case in all
other mathematical theories: 1+1 is not syntactically identical to 2.
The novelty is rather that two things can "be identical" in more than
one way. An inhabitant of x=y can be called an "identification" of x
with y; then two things are identical if there is an identification
between them. It's instead the truncated equality ||x=y|| that
doesn't mean "identical" but rather something weaker; the difference
being invisible to classical mathematics that works only with sets.

Which is not to say that HoTT isn't confusing for newcomers! It
certainly confused me a lot at first. But the same is true of many
other fields of mathematics.

[Michael Shulman]

*Topologically* discontinuous maps can also be represented in spatial
type theory using the flat and sharp modalities, and under appropriate
axioms this coincides with the double-negation notion. But this sort
of "continuity" is orthogonal to the *homotopical* sort of continuity
that's represented by preservation of identifications, and I think it
was the latter that Andrew was referring to.

[Andrew Dabrowski]

I hope you won't be too dismayed to learn that now I'm even more confused.

On Thursday, October 26, 2017 at 5:44:22 PM UTC-4, Michael Shulman wrote:

I say that = does mean identical.  There is no stronger notion of
"sameness" inside the theory than = that could be meant by
"identical".  Terms that are = are not necessarily *syntactically*
identical, but that's an external notion, and also the case in all
other mathematical theories: 1+1 is not syntactically identical to 2.
The novelty is rather that two things can "be identical" in more than
one way.  An inhabitant of x=y can be called an "identification" of x
with y; then two things are identical if there is an identification
between them.  It's instead the truncated equality ||x=y|| that
doesn't mean "identical" but rather something weaker;

I thought ||x=y|| is a proposition that is true just when x=y is inhabited. 

In the latter case, by what you said above, isn't x the same as y?

 

the difference
being invisible to classical mathematics that works only with sets.

So in order to use HoTT mathematicians will have to become intimate with distinctions

that were formally invisible to them.  That is alarming.  I'm used to that kind of thing when studying a new field,

but I thought the idea was that HoTT would eventually allow mathematicians in all fields to formalize their work idiomatically,

without having to force it into the mold of homotopy theory.

On the other hand mathematicians were forced to formalize their fields in the language of set theory,

so maybe now it is just homotopy's turn on top.  That may be what Manin was getting at.

Could you shed some light on this formerly invisible difference, i.e. that between x=y and ||x=y||? 

How should one think of it intuitively?

Or concretely, what is another element of X from 3.8.5 distinct from x_0=(2,|refl|)?

[Andrej Bauer]

On Fri, Oct 27, 2017 at 12:07 AM, Andrew Dabrowski
<unhan...@gmail.com> wrote:
> So in order to use HoTT mathematicians will have to become intimate with
> distinctions that were formally invisible to them. That is alarming.

Yes, it is quite alarming how a formalism can prevent mathematicians
from comprehending new mathematical ideas.

But for those who think that the new ideas aren't worth learning
about, for whatever reason, HoTT can accommodate an asylum, namely
0-Types, a.k.a. sets.

With kind regards,

Andrej

[Michael Shulman]

On Thu, Oct 26, 2017 at 3:07 PM, Andrew Dabrowski <unhan...@gmail.com> wrote:
> I thought ||x=y|| is a proposition that is true just when x=y is inhabited.
> In the latter case, by what you said above, isn't x the same as y?

> ...

> Could you shed some light on this formerly invisible difference, i.e. that
> between x=y and ||x=y||?
> How should one think of it intuitively?

||x=y|| means, informally, that there is at least one identification
between x and y, but we don't have a way to find one. So in a certain
sense "x is the same as y", but we're limited in our ability to use
that fact because we can't actually find a specific identification
between them. We can only use that fact if what we're trying to do or
prove doesn't depend on which identification between them gets used.
Which is the case in the world of "h-sets", just not in the world of
"higher types".

> Or concretely, what is another element of X from 3.8.5 distinct from
> x_0=(2,|refl|)?

There is no other element that's *distinct* from x_0 in the sense of
being *not* equal to it. Indeed, since ||x=y|| for any two elements
of X, they are "equal" in the above sense that there is an
identfication. It's just that we have no
general/canonical/continuous/algorithmic/natural method to *find* an
identification given any x and y. That is, if I give you a set with
two elements like { blue, green }, in order to identify it with 2 = {
0, 1 } you need to choose whether to match blue=0,green=1 or
blue=1,green=0, and any such choice is arbitrary.

>> the difference
>> being invisible to classical mathematics that works only with sets.
>
> So in order to use HoTT mathematicians will have to become intimate with
> distinctions that were formally invisible to them.

That's true in order to make use of the new "higher types" that HoTT
adds to mathematics. (Although many mathematicians, going far beyond
homotopy theorists, are already familiar with the distinction between
equality and isomorphism, and so it shouldn't see that unfamiliar to
them.) However, as Andrej said, none of that is necessary to use HoTT
as a language to speak about the ordinary mathematics that you're
already used to, which takes place in the world of "sets" (or
"h-sets") inside HoTT. That's what I meant to say.

[Andrew Dabrowski]

OK, that's fine, but it's nothing new to classical mathematics.  In the latter we just say that such a function exists, but it can't be homotopically continuous.  I don't see how escalating this to a near paradox in HoTT in helpful.

The fact is in any model of HoTT the type X will have a single inhabitant.  If one is unable to say that in HoTT, perhaps the problem is with HoTT rather than the notion of "singleton"?

>> the difference
>> being invisible to classical mathematics that works only with sets.
>
> So in order to use HoTT mathematicians will have to become intimate with
> distinctions that were formally invisible to them.

That's true in order to make use of the new "higher types" that HoTT
adds to mathematics.  (Although many mathematicians, going far beyond
homotopy theorists, are already familiar with the distinction between
equality and isomorphism, and so it shouldn't see that unfamiliar to
them.)  

Surely you mean all mathematicians are familiar with the distinction between isomorphism and equality?  That is hardly a distinction "invisible in classical mathematics". 

 

However, as Andrej said, none of that is necessary to use HoTT
as a language to speak about the ordinary mathematics that you're
already used to, which takes place in the world of "sets" (or
"h-sets") inside HoTT.  That's what I meant to say.

Maybe my idea is that there should be a way to h-sets without going through homotopy theory.  Then add homotopy to h-sets to get full HoTT.  That approach might be more appealing to nontopologists.

Is such a strict notion of continuity as that in HoTT really necessary for HITs?  Mightn't it be positively advantageous to be able to talk about noncontinuous functions in type theory? 

I can't help but suspect that since homotopy theorists have no use for noncontinuous functions they think no other mathematicians should need them either.  I'm more and more getting the feeling that HoTT is Disneyland for homotopy theorists, but the rest of us will have to construct our own theme parks.

[Daniel R. Grayson]

How would you present a rigorous construction of higher inductive types

to a mathematician, Mike, without indexing the steps in the construction

by ordinals or natural numbers?

[Matt Oliveri]

Andrew, let me try an alternative explanation of the situation in Lemma 3.8.5 (and similar situations), based on different terminology.

HoTT's '=' is *not* equality. It's equivalence. The equality you're used to cannot be reasoned about with the version of HoTT in the book.

The type X := Sig (A:U) || 2 = A || from the lemma is the type of (small) types A such that there exists an equivalence from 2 to A. Intuitively, this the type of sets with two elements. Equivalences between elements of these types are a special case of equivalences between sets (bijections), which are a special case of equivalences between types.
The element x_0 : X := (2, |refl_2|) is the canonical 2-element set, which certainly has two elements.
The type (x_0 = x_0) is the type of equivalences of that set with itself. There are two of those. One is the identity, one swaps the elements.
If X were a set, its elements could only be equivalent in at most one way. x_0 is equivalent to x_0 in two ways, so X is certainly not a set. In particular, it's not a singleton, since a singleton type would be a set.

*If*, you could define the type X' := Sig (A:U) (2 == A), of types *equal* to the canonical 2-element set, it'd obviously be a singleton. But you can't. The closest thing is X'' := Sig (A:U) (2 = A), the type of types paired with an equivalence to 2. Up to equality, this is not a singleton either. But up to equivalence, it is. HoTT always works up to equivalence. (Except for at the judgment level, which you don't explicitly use.)

[Matt Oliveri]

Since an h-set is intuitively any homotopy type that's (homotopy) equivalent to a set, it seems far-fetched to have h-sets without the homotopy stuff. Here "homotopy" doesn't necessarily mean "classical homotopy" (in topological spaces). From what I understand, it's any situation where you always work up to equivalence, roughly.

HoTT has (something equivalent to) any noncontinuous function you like. The idea that all HoTT functions are "continuous" is borrowing intuitions from classical homotopy theory, and is not technically correct in general. Even when you do interpret HoTT functions as continuous functions between (certain) topological spaces, that doesn't mean all functions between *internal* topological spaces are (internally) continuous. (I don't think.) You seem to be confusing internal and external properties.

On Saturday, October 28, 2017 at 4:56:34 PM UTC-4, Andrew Dabrowski wrote:

[Michael Shulman]

On Sat, Oct 28, 2017 at 1:56 PM, Andrew Dabrowski <unhan...@gmail.com> wrote:
> OK, that's fine, but it's nothing new to classical mathematics. In the
> latter we just say that such a function exists, but it can't be
> homotopically continuous. I don't see how escalating this to a near paradox

> in HoTT is helpful.

If you don't mind this distinction in classical mathematics, there's
no reason to consider it "paradoxical" that HoTT has a slightly
different way of expressing it. Just think of Pi(x:A) B(x) as meaning
"there is a continuous function" and Pi(x:A) ||B(x)|| as meaning
"there exists a discontinuous function". The only difference is that
in set-theoretic mathematics the default notion of function is
discontinuous so that we have to manually define and prove when a
function is continuous, whereas in HoTT the default notion of function
is continuous and we have to add a qualifier ||-|| to express
discontinuous ones.

This is useful because, among other reasons, when working in practice
with sets that have nontrivial homotopical structure (or equivalently,
nontrivial categorical/groupoidal structure), continuity/functoriality
is the norm rather than the exception. Thus it saves work to use a
foundational theory that behaves similarly.

> The fact is in any model of HoTT the type X will have a single inhabitant.

Whether or not this is true depends on what one means by "single
inhabitant". A model of HoTT is a certain kind of higher category;
there's no *a priori* meaning to saying that an object of such a
category "has a single inhabitant" or doesn't.

There is a sense in which your "fact" is true, but this is exactly the
sense that we can also prove internally that X "has one element": its
0-truncation is terminal. In all other senses that I can think of,
your "fact" is false: not only is the object X not equivalent to the
terminal object, but there even exist models in which it has more than
one distinct global element (i.e. morphism 1 -> X from the terminal
object).

> Surely you mean all mathematicians are familiar with the distinction between
> isomorphism and equality? That is hardly a distinction "invisible in
> classical mathematics".

I didn't say that the distinction between isomorphism and equality was
invisible in classical mathematics; I was using it as an *analogy*
that might be more familiar to some people than homotopy theory would
be. I've repeatedly suggested in this thread that it's better to
think of HoTT as being about generalized notions of "sameness", such
as isomorphism and equivalence in category theory; but you persisted
in using terminology like "continuous", so I assumed that it was more
familiar to you than the category-theoretic ideas despite your avowed
dislike of topology. If you are happier with category theory than
with homotopy theory, then you can instead think of Pi(x:A) B(x) as
meaning "there is a functor" and Pi(x:A) ||B(x)|| as meaning "there
exists a non-functorial assignment on objects".

> Maybe my idea is that there should be a way to h-sets without going through
> homotopy theory. Then add homotopy to h-sets to get full HoTT. That
> approach might be more appealing to nontopologists.

Yes, in Book HoTT you can start with MLTT (chapter 1) and add
propositional truncation, set-quotients (or more general set-HITs),
function extensionality, and propositional univalence to such get a
"world of h-sets", then only later add more general HITs and full
univalence. If and when there is a second edition of the HoTT Book,
I'm planning to advocate for an approach that's more like that. (The
first edition was written in only a few months and a lot of the
material in it was less than a year old; it's surprising that it reads
as coherently as it does.)

Mike

[Michael Shulman]

On Sat, Oct 28, 2017 at 1:59 PM, Daniel R. Grayson
<danielrich...@gmail.com> wrote:
> How would you present a rigorous construction of higher inductive types
> to a mathematician, Mike, without indexing the steps in the construction
> by ordinals or natural numbers?

I wouldn't. Why do you ask?

Inside of HoTT, HITs don't need to be "constructed"; they are
postulated. It's only when building a *model* of HoTT that they have
to be constructed. If the model is built inside ZFC, then HITs are
constructed iteratively along the ordinals. In theory, it should also
be possible to build a model of HoTT inside a metatheoretic HoTT and
use HITs in the metatheory to build HITs in the object-theory, but I
don't think that has been made precise.

> On Monday, October 23, 2017 at 11:30:50 PM UTC-5, Michael Shulman wrote:
>>
>>
>> A less important, but nontrivial, benefit of HoTT even for the
>> non-homotopically-inclined mathematician is the notion of higher
>> inductive type. The general type-theoretic notion of "inductive type"
>> deserves to be much better known in mathematics. Many mathematical
>> objects are naturally defined as inductive types -- or at least they
>> would be, if mathematicians knew what general inductive types were and
>> didn't feel obligated to butcher all inductive proofs to force them to
>> induct over natural numbers (or more generally ordinal numbers) rather
>> than arbitrary inductive types. (-: Higher inductive types make
>> inductive types even more powerful by essentially allowing the
>> quotient by an equivalence relation to happen as part of the inductive
>> definition.
>>

[Daniel R. Grayson]

I asked, because showing mathematicians how to construct higher inductive types

rigorously would ensure that "mathematicians knew what general inductive

types were and didn't feel obligated to butcher all inductive proofs."  As a small 

part of the problem of showing mathematicians why HoTT is sound, it might

be a good contribution.  Written in an informal style with no syntax, an expository 

paper covering the construction might prove attractive and useful.

[Michael Shulman]

A rigorous construction of HITs is in https://arxiv.org/abs/1705.07088
. As for an informal style with no syntax, are you thinking of
something like http://home.sandiego.edu/~shulman/papers/indcell.pdf ?

On Sun, Oct 29, 2017 at 7:06 AM, Daniel R. Grayson

[Daniel R. Grayson]

Right, I was aware of your paper.

Those slides from 2012 are exactly the kind of thing I had in mind, thank you.  Imagine enlarging

that into a paper.  HoTT would be mentioned only in the introduction, rigorous proofs would

be provided, perhaps an intermediate section on inductive definitions of sets by constructors

of elements and constructors of relations, could be included, and more examples could be

added.  The goal would be to have something citable when mathematicians want to use

an inductive definition in their own papers.

> email to hott-cafe+unsubscribe@googlegroups.com.

[Andrew Dabrowski]

Sorry for exasperating everyone. 

I was intrigued when I read that HoTT was a language both formal and
sufficiently high-level to permit mathematicians to do real work in it.
But I have never studied type theory (or homotopy theory needless to say)
so I've taken on a probably impossible task to try try to get myself up to speed in
HoTT in a couple of weeks.  Since this is the only place I can find people who
actually understand HoTT I've been asking all sorts of stupid questions, but I should
probably go back and start studying type theory from scratch.

Nevertheless :) I have a few follow up questions and comments (below).

On Saturday, October 28, 2017 at 6:19:24 PM UTC-4, Michael Shulman wrote:

On Sat, Oct 28, 2017 at 1:56 PM, Andrew Dabrowski <unhan...@gmail.com> wrote:


> The fact is in any model of HoTT the type X will have a single inhabitant.

Whether or not this is true depends on what one means by "single
inhabitant".  A model of HoTT is a certain kind of higher category;

Isn't the intention that HoTT be modeled on a computer?  Isn't it reasonable to

ask whether any two objects x,y:X on the computer satisfy x=y?

 

there's no *a priori* meaning to saying that an object of such a
category "has a single inhabitant" or doesn't.

There is a sense in which your "fact" is true, but this is exactly the
sense that we can also prove internally that X "has one element": its
0-truncation is terminal.  In all other senses that I can think of,
your "fact" is false: not only is the object X not equivalent to the
terminal object, but there even exist models in which it has more than
one distinct global element (i.e. morphism 1 -> X from the terminal
object).

You've lost me.  Are you saying 1:X?

And didn't you say earlier "There is no other element that's *distinct* from x_0 in the sense of
being *not* equal to it."?

 

At the very least I think this shows that the eample X constructed in Lemma 3.8.5 has great pedagogic potential

and deserves a fuller examination the HoTT Book.

> Maybe my idea is that there should be a way to h-sets without going through
> homotopy theory.  Then add homotopy to h-sets to get full HoTT.  That
> approach might be more appealing to nontopologists.

Yes, in Book HoTT you can start with MLTT (chapter 1) and add
propositional truncation, set-quotients (or more general set-HITs),

Why do you need to add truncation to MLTT?  Is there a notion of infinity-groupoids in MLTT?

Couldn't you start with OTT and add the H?

 

[Cory Knapp]

 

Isn't the intention that HoTT be modeled on a computer?  Isn't it reasonable to

ask whether any two objects x,y:X on the computer satisfy x=y?

One intention, not *the* intention. But I don't see how this is relevant to the point: "Having an object" is something that needs to be interpreted for objects that aren't sets.

 

 

there's no *a priori* meaning to saying that an object of such a
category "has a single inhabitant" or doesn't.

There is a sense in which your "fact" is true, but this is exactly the
sense that we can also prove internally that X "has one element": its
0-truncation is terminal.  In all other senses that I can think of,
your "fact" is false: not only is the object X not equivalent to the
terminal object, but there even exist models in which it has more than
one distinct global element (i.e. morphism 1 -> X from the terminal
object).

You've lost me.  Are you saying 1:X?

A "global element" of X in a category is a map from the terminal object to X; this is the closest thing to a notion of "element" in a categorical setting

 

And didn't you say earlier "There is no other element that's *distinct* from x_0 in the sense of
being *not* equal to it."?

There is no other element which we can prove to be distinct from x_0 in the language; a particular model may have others.

 

 

At the very least I think this shows that the eample X constructed in Lemma 3.8.5 has great pedagogic potential

and deserves a fuller examination the HoTT Book.

> Maybe my idea is that there should be a way to h-sets without going through
> homotopy theory.  Then add homotopy to h-sets to get full HoTT.  That
> approach might be more appealing to nontopologists.

Yes, in Book HoTT you can start with MLTT (chapter 1) and add
propositional truncation, set-quotients (or more general set-HITs),

Why do you need to add truncation to MLTT?  Is there a notion of infinity-groupoids in MLTT?

Whether we can see it or not, the types of MLTT are infinity-groupoids. The infinity-groupoids we're interested in might all be "1-truncated" (sets in hott). However, without truncations, the only interpretation of logic is the Curry-Howard interpretation, which is not particularly well-behaved (e.g., the "image" of a function with the CH interpretation is equivalent to the domain). The extensive use of setoids in type-theoretic formalizations is partly to correct for this. Truncations give us an interpretation of logic that behaves well.

 

Couldn't you start with OTT and add the H?

I don't know enough about OTT to say much, but my (probably incorrect) understanding is that HoTT+truncations+set-HITs gives a more uniform presentation.

 

--
You received this message because you are subscribed to the Google Groups "HoTT Cafe" group.

To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+unsubscribe@googlegroups.com.

[Gershom B]

Observational Type Theory and HoTT are extremely different in their
treatment of identity -- OTT almost definitionally has "no homotopy."
One way, maybe, to think of it is as a subtheory of extensional type
theory where equality is representable by a certain poset structure.
For those interested, Conor McBride, one of the people who worked on
OTT, wrote up a blogpost a few years ago where he tried to summarize
some of the key ideas in light of subsequent developments:
https://pigworker.wordpress.com/2015/01/08/observational-type-theory-delivery/

--Gershom

>> email to hott-cafe+...@googlegroups.com.

>> For more options, visit https://groups.google.com/d/optout.
>
>

> --
> You received this message because you are subscribed to the Google Groups
> "HoTT Cafe" group.
> To unsubscribe from this group and stop receiving emails from it, send an

> email to hott-cafe+...@googlegroups.com.

[Michael Shulman]

On Wed, Nov 1, 2017 at 7:19 PM, Andrew Dabrowski <unhan...@gmail.com> wrote:
> Isn't the intention that HoTT be modeled on a computer? Isn't it reasonable
> to ask whether any two objects x,y:X on the computer satisfy x=y?

I suspect that what you mean by "modeled on a computer" is
"*implemented* on a computer". That is, the sort of thing we do in
Coq, Agda, and Lean, where the computer constructs, elaborates,
typechecks, and evaluates terms for us. In other words, this is using
the computer to manipulate the "tautological" syntactic model of the
type theory.

The syntactic model does probably have the property that any two
*global elements* of this type X (i.e. closed terms, defined in the
empty context) will be equal. (I say "probably" because the only
proof of this that I can think of would involve a canonicity theorem
for terms of type X, which I'm not sure has been proven yet, even in
cubical type theory.) In this way it is similar to the model in
classical oo-groupoids.

There is also a different possible sense of "modeled on a computer"
where one uses a given notion of computation (separate from the syntax
itself) to *build* a model, generally called a "realizability" model.
(Perhaps "computational type theory" blurs the line between these two
senses.) I don't know whether there are realizability models in which
X has multiple distinct global elements.

The point, though, is that there are also "non-computational" models,
and in some of these X does certainly have multiple distinct global
elements. So your original statement "in *any* model of HoTT the type
X will have a single inhabitant" is not true, except in the internal
sense of "X is 0-connected". But more importantly, even internally in
the theory there are other senses of "having only a single element"
that are false about the type X. Homotopy type theory is a theory of
oo-groupoid-like objects, and it's just a fact that for an
oo-groupoid, being 0-connected is different from being contractible.
Since these properties are indistinguishable for sets, no matter how
we set up the notation and terminology, some retraining of the
intuition is necessary.