definition of paths over may need a universe

[DanGrayson]

Here is my definition of paths over a path:

And here is path induction:

So we need a suitable universe to contain everything. But this is long before the section on universes. And in the section on universes we don't even say that every family Y(x) of types has all its members contained in some universe.

Or we need to revert to the asymmetric definition involving transport.

Or we need a new form of path induction devoted to defining new types. This seems to be the cleanest way to proceed.

[UlrikBuchholtz]

Yes, before we have universes we need all inductive types, including path types, to support large elimination.

The question is how best to deal with this pedagogically. Maybe the best option is just to face it head on, and mention it as an additional rule for each inductive type. For natural numbers, for example, we can mention the family of higher type functionals, F 0 = N, F (Succ n) = F n → N.

But then, after we introduce universes, large elimination comes for free, so this should be noted.

And in the section on universes we don't even say that every family Y(x) of types has all its members contained in some universe.

We do, at the beginning of Sec. 2.12 on universes, where we say that we “make precise” the notion of a family of types by taking it to be a function to a universe.

[DanGrayson]

The previous notion of a family of types was already precise, and what this section does is to change the definition of the notion:

I like the idea of adding additional inductive rules -- they're easy to motivate.

[DanGrayson]

Re:

But then, after we introduce universes, large elimination comes for free, so this should be noted.

Not totally for free -- one must still prove that each family of types has every member in some universe. And that's a meta-mathematical statement, so we should avoid delving into it.

[DanGrayson]

Hmm, would we need a totally new identity type whose elements identify 2 types?

(So we could use it here:

)

[UlrikBuchholtz]

Hmm, would we need a totally new identity type whose elements identify 2 types?

Yes, we would. And, on p. 25 (in Sec. 2.12), we would then need to add: (6') If X,X' : U, then (X = X') : U and (X = X') ≡ (X =_U X') : U', when U : U'. Or only: (X = X') : U', as the former option makes the identity types in U U-small on the nose, and not only essentially U-small, which is what we get from univalence.

And we'd probably need definitional equalities relating large eliminations to U-small eliminations as well. (Maybe in App. B we could/should say something about universes à la Tarski/Russell, cumulativity, etc.)

My worry is that these issues will be a distraction in Ch. 2. There are also some issues that may still be subject to ongoing research. For example, I don't know/remember if there's been progress on conservativity of Russell-style over Tarksi-style since Zhaohui Luo's Notes on Universes.

[DanGrayson]

I don't see how to provide a semantic interpretation for X=X' in topology -- you need a universe U to speak of U-small fibrations over [0,1] connecting X to X'. I think we'd better stay away from all that. We could move the section on universes so it comes before this section. Or we could instead take one of the two asymmetric definitions for paths over involving transport.

[UlrikBuchholtz]

Yes, maybe it's better pedagogically to just switch to the transport definition.

BTW, in Sec. 2.12 on universes, shouldn't we rephrase item (5) on p. 25 to include all inductive types? (And any higher inductive types we may later introduce.)

(Re semantics, I don't see the problem: If nothing else, we could define X=X' to be the type of equivalences X≃X', which itself is a subtype of X→X'.)

[DanGrayson]

re 2.12: we haven't introduced a general scheme for making new inductive definitions, so what do we mean by "all inductive types"?

re semantics: take that approach and you probably can't validate the existence of a map between X=X' and X =_U X', in either direction.

[DanGrayson]

I'll switch to the transport definition.

[UlrikBuchholtz]

Great!

re semantics: take that approach and you probably can't validate the existence of a map between X=X' and X =_U X', in either direction.

Isn't that exactly univalence?

[DanGrayson]

Oh, right -- there should be a map X =_U X' ---> X = X', and it should be an equivalence. Now I'm suspicious of transport by elements of X = X'.

[UlrikBuchholtz]

re 2.12: we haven't introduced a general scheme for making new inductive definitions, so what do we mean by "all inductive types"?

At the very least, we could say “all the particular ones introduced hitherto (e.g., in Sec. 2.11), as well as any others that will be introduced later on.”

BTW, I just noticed: We use large eliminations twice on p. 23: Once for the family P over Bool and again in Ex. 2.11.3 for the family T (again over Bool).

[UlrikBuchholtz]

We say now, on p. 23, “Thirdly, there will be a type called Bool, defined by induction and provided with two elements, yes and no.”

Bool isn't defined by induction – rather, it's an inductive type!

[DanGrayson]

Instead of introducing that terminology, it might be good just to display all the rules for each of the types in that section.

[UlrikBuchholtz]

Instead of introducing that terminology, it might be good just to display all the rules for each of the types in that section.

You mean “large elimination”? Yes, that terminology can be relegated to the margin. I don't think we need to give the exact rule for each inductive type; it should suffice to spell it out in Sec. 2.3 (on natural numbers), make a note about it in Sec. 2.4 (on identity types), and then another note in Sec. 2.11, perhaps in the introductory paragraph. But what did you have in mind?

[DanGrayson]

No, I was thinking of "inductive type", which might be hard to define. Well, maybe not -- we could just say that inductive types are the ones we present, which are characterized by the rules for using them, one of which is for producing elements by induction.

As for "large elimination", we probably should not mention it, nor use it.

I was thinking that for empty, unit, and bool, we should spell out, for each of them, all the rules. Otherwise we're asking students to guess.

[UlrikBuchholtz]

Well we use the term “inductive type” many times, even in the title of Sec. 2.11.

If we want to do without large eliminations, then we do need to move the universe section to prior to Sec. 2.11, or move the bits about proving yes ≠ no and 0 ≠ 1 etc. to the universe section.

[DanGrayson]

On second thought, it might be sort of cool to have large elimination rules for each of our inductive types. Well, maybe not for the circle.

[UlrikBuchholtz]

Why not? A key point in Ch. 3 is to consider type families over the circle as types with a self-equivalence.

[DanGrayson]

The question for me is whether anyone is including large elimination for the circle in a sound semantic model based on topology.

[UlrikBuchholtz]

I'm no expert on semantics, but don't we usually work in a meta-theory where any type/set belongs to some (Grothendieck) universe. If A → S¹ is a fibration, then A (and S¹) belong to some universe U, and the fibration itself then lives in the semantics of U-small type families over S¹.

If there is anything to worry about, it's probably cumulativity of universes: As I mentioned above, that's more likely to cause trouble either semantically and/or for canonicity.

[DanGrayson]

If you model X =_U X' with U-small fibrations over [0,1], then the thing depends on U, so you can't expect to get a well defined object for X = X' by choosing a universe at random.

[UlrikBuchholtz]

I think that illustrates rather why one should be dubious about cumulativity in general.

I was suggesting above to model X = X' as X ≃ X' which is patently universe-invariant. The question then re-appeared in the guise of large elimination for HITs. I just had a look at Lumsdaine–Shulman, and they only do large eliminations, so that's in a sense easier than ensuring the universes are closed under HITs.

[UlrikBuchholtz]

Sorry, that's not right: They say you need universes to get large eliminations. But I still think they're easier to get than cumulative universes, though as I said, I'm no expert on semantics.

[DanGrayson]

I was worried above about modeling transport along an identity of type X = X', but transport is only for identities between two elements of a type. Let's just stay away from identities between two types, unless we are already thinking of them as elements of a single universe. I can rephrase 2.6.2 to produce an equivalence between the two possible definitions of paths-over.

As for cumulative universes, Vladimir preferred the Tarski style.

[marcbezem]

There are 57 lines on with the macro \pathover occurs, 36 of which are in intro-uf.tex. There may also be some pictures involved. As an alternative, we could move the definition till after universes are introduced. Let's discuss this on one of our Thursday meetings.

[bidundas]

As you know, I’m totally fine with scrapping pathovers.

Where, if anywhere, have we written X=X’ when X and X’ are not in some (probably unspecified) universe U with a different interpretation than X=_UX’ ?

Bjorn

On 23 Aug 2021, at 08:54, Marc Bezem @.***> wrote:

There are 57 lines on with the macro \pathover occurs, 36 of which are in intro-uf.tex. There may also be some pictures involved. As an alternative, we could move the definition till after universes are introduced. Let's discuss this on one of our Thursday meetings.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android.

[DanGrayson]

I used X = X' here:

[DanGrayson]

... but it's not essential -- the identity can be converted to an equivalence.

[DanGrayson]

As you know, I’m totally fine with scrapping pathovers.

I really like the way they make this result look, though:

[DanGrayson]

I tried to formulate an additional induction principle for paths so I could refer to it in definition 2.6.1, but it seems hard! The problem is that if you follow E3 of 2.4 as a template, you end up just mentioning a type X, an element a, and a type T. From this you get a family of types S(a',p) parametrized by an element a' and a path p of type a=a'. There's nothing about y' : Y(a') and nothing about specializing a' to a so y' and y have the same type.

The same omission occurs in E3 -- the possibility of further elements in the context is ignored.

[marcbezem]

I'm trying to understand this better. It seems that the optimal context is (spacing intentional) A,Y,a,y, a',p, y', and that the problem is y' to the right of a',p. A context on the left occurs already in 2.2 when addition is defined. (@DanGrayson: do you remember we had a discussion about this with n:N in the context for +, in Oslo?). The biggest problem is the absence of a universe. With a universe we can take Y(a') -> U to abstract from y'. The HoTT book has universes early on, and states that "A is a type" always meant "A:U" for some U.

PS: context A,Y as above already uses universes.

[UlrikBuchholtz]

How about the following:

(E4) Suppose we are given: a type X and an element a : X;
a family of types P(b,e) as in (E3);
as well as a type family Tₐ(p) parametrized by p : P(a,refl).
Then we get a family of types T(b,e,p) parametrized by b : X, e : a = b, and p : P(b,e).
Moreover, T(a,refl,p) ≡ Tₐ(p) for all p:P(a,refl)

In Def. 2.6.1 we then take P(b,e) :≡ Y(b) and Tₐ(y') :≡ (y = y) for y' : Y(a).

[marcbezem]

This seems to work. However:

• It is very complicated to have already in 2.3;
• I can't overlook the consequences for the meta-properties of this in combination with all other things we have;
• Would we have large elimination for all inductive types? Higher up in the thread @UlrikBuchholtz remarked that large elimination would come for free when we have universes. I didn't understand that remark.

[bidundas]

Here I agree with Marc. Would a middle ground be to keep transport as the official device, but somehow allow pathovers as a notational convenience?

Bjorn

On 27 Aug 2021, at 09:18, Marc Bezem @.***> wrote:

This seems to work. However:

• It is very complicated to have already in 2.3; • I can't overlook the consequences for the meta-properties of this in combination with all other things we have; • Would we have large elimination for all inductive types? Higher up in the thread @UlrikBuchholtz remarked that large elimination would come for free when we have universes. I didn't understand that remark. — You are receiving this because you commented. Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android.

[UlrikBuchholtz]

It is very complicated to have already in 2.3;

I agree it's a mouthful.

Would we have large elimination for all inductive types?

Yes, then I would say we'd have this for all (highter) inductive types.

I can't overlook the consequences for the meta-properties of this in combination with all other things we have;

Higher up in the thread @UlrikBuchholtz remarked that large elimination would come for free when we have universes. I didn't understand that remark.

My thinking was that we could translate the formal system underlying the above (judgments for being a type family and cumulative universes) into a system like that of the HoTT book where the judgment “Γ ⊢ P : A → Type” is translated as “Γ ⊢ P : A → Uᵢ for some i”. Then all our large eliminations reduce to small eliminations relative to some universe.

Here I agree with Marc. Would a middle ground be to keep transport as the official device, but somehow allow pathovers as a notational convenience?

Another option is to heave close to the HoTT book and do universes earlier: Maybe split in two parts: An early part that says every type belongs to a universe, and a later part with more details.

[UlrikBuchholtz]

Recall that we still need large elimination in some form to prove true ≠ false and 0 ≠ 1.

[marcbezem]

That would also be solved by "... do universes earlier: Maybe split in two parts ..." I'm in favor of that.

[bidundas]

With the caption “Early universes” ;-)

Bjorn

On 27 Aug 2021, at 11:04, Marc Bezem @.***> wrote:

That would also be solved by "... do universes earlier: Maybe split in two parts ..." I'm in favor of that.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android.

[marcbezem]

Or: "In the beginning there were universes". They are the first types one defines in the empty context, before everything else.

[DanGrayson]

How about the following:

(E4) Suppose we are given: a type X and an element a : X;
a family of types P(b,e) as in (E3);
as well as a type family Tₐ(p) parametrized by p : P(a,refl).
Then we get a family of types T(b,e,p) parametrized by b : X, e : a = b, and p : P(b,e).
Moreover, T(a,refl,p) ≡ Tₐ(p) for all p:P(a,refl)

In Def. 2.6.1 we then take P(b,e) :≡ Y(b) and Tₐ(y') :≡ (y = y) for y' : Y(a).

That covers just one special case, so it doesn't seem general enough. Somehow (E3) "works" without even mentioning the possibility of further items in the context. Of course, some students might notice that problem with (E3).

[UlrikBuchholtz]

That covers just one special case, so it doesn't seem general enough. Somehow (E3) "works" without even mentioning the possibility of further items in the context. Of course, some students might notice that problem with (E3).

For (E3), you can use Π-types to get the general case “with variable to the right in the context”. Likewise, you can use Σ-types of everything to the right to see that my proposed (E4) is sufficiently general.

But it doesn't matter, since we decided to do “Early universes”/“In the beginning was the universe hierarchy, and the universe hierarchy was with the types, and the types were classified by universes.”

[DanGrayson]

But it doesn't matter, since we decided to do “Early universes”/“In the beginning was the universe hierarchy, and the universe hierarchy was with the types, and the types were classified by universes.”

Oh, okay. I guess we'd better put it after 2.2 (Types, etc.) and before 2.3 (natural numbers). Then we'll be prepared to say that induction on a natural number can also be used to make families of types.

I'd be happy to take care of it.

[bidundas]

“In the beginning was the universe hierarchy, and the universe hierarchy was with the types, and the types were classified by universes.”

I think the gospel according to Marc/Daniel/Ulrik/Pierre/Bjorn will be looked on kindly by Pope Francis, but I’m concerned about having a horde of evangelical fundamentalists at our door if we publish it in this form.

Bjorn

[DanGrayson]

Okay, I've made the relevant changes (except for the ones related to making type families over bool). But now I'm sad:

Do we have to address what happens to the path-over type if a different universe is chosen?

[UlrikBuchholtz]

That seems like the same sort of issue that causes problems with canonicity when we have cumulativity. I don't know how that's taken care of in Thierry's paper, but we could ask him.

BTW, I changed the word “artifice” to “instrument” in the beginning of (the new) Sec. 2.3 to describe universes, as I don't want to give the impression that universes are inherently deceptive (although many surrounding issues certainly can be tricky!).

[UlrikBuchholtz]

What do you think of Thierry's suggestion to take dependent paths as a primitive? We can of course prove that it is equivalent to both the indexed inductive family and the two transport equalities.

[bidundas]

I was fine with sticking with transport (and as to the argument about asymmetry, the fact that the induction singles out one of the endpoints makes all definitions asymmetric), so I take this as a theological discussion from which I am exempted.

Bjorn

On Sep 13, 2021, at 13:19, Ulrik Buchholtz @.***> wrote:

What do you think of Thierry's suggestion to take dependent paths as a primitive? We can of course prove that it is equivalent to both the indexed inductive family and the two transport equalities.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android.

[bidundas]

PS. I can’t come Thursday.

Bjorn

On Sep 13, 2021, at 14:02, Bjorn Ian Dundas @.***> wrote:

I was fine with sticking with transport (and as to the argument about asymmetry, the fact that the induction singles out one of the endpoints makes all definitions asymmetric), so I take this as a theological discussion from which I am exempted.

Bjorn

On Sep 13, 2021, at 13:19, Ulrik Buchholtz @.***> wrote:

What do you think of Thierry's suggestion to take dependent paths as a primitive? We can of course prove that it is equivalent to both the indexed inductive family and the two transport equalities.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android.

[marcbezem]

Dependent paths as a primitive in 2.3 is quite difficult for the reader. Isn't it better to pay some attention to the asymmetry later in the book (heading: "Asymmetry")? Ulrik mentions the equivalence of the two transport equalities. Bjørn is right that based path induction is already asymmetric, we could show that choosing "the other" base point is equivalent (or have an exercise to that effect).