Remark 4.2.21, universes

[marcbezem]

Remark 4.2.21 about size issues has some problems since it assumes much more about the universe structure than currently stated in Section 2.3, such as:

• the universe in which a composite type lives (notably the sum type in lines 3,4 of Remark 4.2.21);
• the ascending chain of universes which is misstated as "Our convention from Section 2.3."

At least the first problem cannot be solved in Section 2.3. Although I agree with a light approach to universes, I think something more has to be said about them in Remark 4.2.21 in order to make this remark understandable. The remark can also be simplified by taking as example the trivial group, with small classifying type (True,triv) and large one (Set_(True),True).

I assigned this issue to myself, but would appreciate your input on beforehand.

[bidundas]

Ouch, this was of course written long before 2.3 existed. Here’s my opinion. If we need to say much about the underlying universe before an informal remark as 4.2.21 is made, I suggest it is not done in chapter 4. For everything after chapter 2 we’ll need to have the basic structure in place (without mention or distraction). As we present new structure in chapter 2 we should be clear whether these things to will be assumed to exist without mentioned later - perhaps with a summing up at the end of chapter 2: this is mandatory and this is optional.

Bjorn

On Jun 19, 2024, at 10:00, Marc Bezem @.***> wrote:

Remark 4.2.21 about size issues has some problems since it assumes much more about the universe structure than currently stated in Section 2.3, such as: • the universe in which a composed type lives (notably the sum type in lines 3,4 of Remark 4.2.21); • the ascending chain of universes which is misstated as "Our convention from Section 2.3." At least the first problem cannot be solved in Section 2.3. Although I agree with a light approach to universes, I think something more has to be said about them in Remark 4.2.21 in order to make this remark understandable. The remark can also be simplified by taken as example the trivial group, with small classifying type (True,triv) and large one (Set_(True),True). I assigned this issue to myself, but would appreciate your input on beforehand. — Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you are subscribed to this thread.Message ID: @.***>

[External email] Make sure you recognize the sender's email address before you click links, open attachments, or get involved in financial transactions. Contact IT-support BRITA if you have any questions.

[marcbezem]

No doubt 2.3 has changed over time, and it has been moved to this early place when Dan found out that our definition of paths over actually requires universes. The ascending chain of universes could be added to 2.3. But sum types come later. In 2.3 the reader has been introduced to function types in 2.2, but not sum types yet. We could add in 2.3 in some light form: if X:U and Y:U' then X->Y lives in a universe that includes both U and U', and something similar holds for the type formers that will show up in the sequel. Then there is a basis to say in 4.2.21 that, e.g., Set_0 : U_1, where Set_0 is the sum type over U_0. I wouldn't need much more to explain small and large versions of the trivial group. If 4.2.21 is still too much of a distraction, it could perhaps become a footnote?

[marcbezem]

I have added a new footnote 8 (currently on page 99) that can be discussed as alternative to Remark 4.2.21 with its footnotes 9 and 10 (which are integrated in my new footnote).

[marcbezem]

After some discussions we landed on footnote 8, with some minor changes. I also changed the definition of the trivial group to Aut_Prop(True) (was with Set for Prop), taking care of all consequences. I'm closing this issue now.