[-- Attachment #1.1: Type: text/plain, Size: 1366 bytes --] I would like to advertise this paper, which investigates injective types and algebraically injective types, and their relationship (https://arxiv.org/abs/1903.01211). In this paper, it is important to take universe levels seriously (for the reasons explained there). In the HoTT book, and in Coq, the universes are taken to be cumulative on the nose, and we pretend, notationally, that there is only one universe (this is called typical ambiguity). Based on the experience of this paper, I have the feeling that the loss of cumulativity, as in Agda, but also as in the infty-topos model of univalent type theory by Mike (https://arxiv.org/abs/1904.07004) is a good thing. In particular, I am not sure how typical ambiguity with cumulativity would be able to handle what is said in the above injectives paper. When I say "would be able to handle" I don't mean just "accepting the constructions", but also present them to the (mathematical) user in such a way that is both understandable and usable as a blackbox (by quoting published resuls). 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+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 1654 bytes --] <div dir="ltr">I would like to advertise this paper, which investigates injective types and algebraically injective types, and their relationship (https://arxiv.org/abs/1903.01211).<div><br></div><div>In this paper, it is important to take universe levels seriously (for the reasons explained there). In the HoTT book, and in Coq, the universes are taken to be cumulative on the nose, and we pretend, notationally, that there is only one universe (this is called typical ambiguity). Based on the experience of this paper, I have the feeling that the loss of cumulativity, as in Agda, but also as in the infty-topos model of univalent type theory by Mike (https://arxiv.org/abs/1904.07004) is a good thing. In particular, I am not sure how typical ambiguity with cumulativity would be able to handle what is said in the above injectives paper.</div><div><br></div><div>When I say "would be able to handle" I don't mean just "accepting the constructions", but also present them to the (mathematical) user in such a way that is both understandable and usable as a blackbox (by quoting published resuls).</div><div><br></div><div>Martin</div><div><br></div></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> For more options, visit <a href="https://groups.google.com/d/optout">https://groups.google.com/d/optout</a>.<br />

Interesting point! I definitely agree that we don't want to be *forced* to be typically ambiguous; there are times when we need to explicitly distinguish universes. This was already the case in a few places in the book, e.g. Lemmas 10.3.21 and 10.3.22. And Coq's universe polymorphism now also *allows* the user to explicitly specify universe levels when desired. (On the other hand, it's also nice to not be forced to label all universes explicitly all the time. But on the third hard, at least in Coq as it is now, the interaction of user-specified universes with automatically-deduced ones seems to be fairly fragile.) However, it's not clear to me why cumulativity would be a problem. In fact you wrote in the paper that "We don't assume that the universes are cumulative... but we also don't assume that they are not". Which makes it sound as though cumulativity, though not necessary, wouldn't be a problem if it did hold -- would it? On Tue, Apr 30, 2019 at 4:05 PM <escardo.martin@gmail.com> wrote: > > I would like to advertise this paper, which investigates injective types and algebraically injective types, and their relationship (https://arxiv.org/abs/1903.01211). > > In this paper, it is important to take universe levels seriously (for the reasons explained there). In the HoTT book, and in Coq, the universes are taken to be cumulative on the nose, and we pretend, notationally, that there is only one universe (this is called typical ambiguity). Based on the experience of this paper, I have the feeling that the loss of cumulativity, as in Agda, but also as in the infty-topos model of univalent type theory by Mike (https://arxiv.org/abs/1904.07004) is a good thing. In particular, I am not sure how typical ambiguity with cumulativity would be able to handle what is said in the above injectives paper. > > When I say "would be able to handle" I don't mean just "accepting the constructions", but also present them to the (mathematical) user in such a way that is both understandable and usable as a blackbox (by quoting published resuls). > > 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+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- 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+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 3200 bytes --] On 01/05/2019 03:50, Michael Shulman wrote:> Interesting point! I definitely agree that we don't want to be > *forced* to be typically ambiguous; there are times when we need to > explicitly distinguish universes. This was already the case in a few > places in the book, e.g. Lemmas 10.3.21 and 10.3.22. And Coq's > universe polymorphism now also *allows* the user to explicitly specify > universe levels when desired. (On the other hand, it's also nice to > not be forced to label all universes explicitly all the time. But on > the third hard, at least in Coq as it is now, the interaction of > user-specified universes with automatically-deduced ones seems to be > fairly fragile.) Right. > However, it's not clear to me why cumulativity would be a problem. In Agda each type gets a unique universe (or at most one universe) and often (but not always) the system is able to infer them if we write question marks "?" for them (but not always). Cumulativity is not "on the nose" in the sense that from X : U_l you would get X : U_m for m ≥ l. Instead, if you need to have (a copy of) X in U_m, you need to use an explicit embedding U_l → U_m. (I only ever used this embedding to show that U_l is a retract of U_m if we assume propositional resizing.) In practice, however, I never needed to use this embedding, as the closure properties for universes work with more than one universe at a time. For instance, if X:U_l and A : X → U_m, then Π X A : U_{max l m}. With this kind of closure property, I haven't encountered the practical need for cumulativity. It is nice, in practice, that universes are uniquely determined. Insted of thousands of level constraints, we have a unique, small, (polymorphic) level assignment. > In fact you wrote in the paper that "We don't assume that the > universes are cumulative... but we also don't assume that they are > not". Which makes it sound as though cumulativity, though not > necessary, wouldn't be a problem if it did hold -- would it? In theory it wouldn't be a problem if it holds. However, if Agda did have cumulativity, it would lose the unique-level assignment property that I use to infer the levels of the results from my given levels of the data. However, in the absence of a concrete proof assistant with the option to enable and disable cumulativity, it is impossible to perform experiments to confirm or reject this conjectural impression. I consider the universe-level system of Agda to be excellent in practice, and easy to use. Moreover, as I said, if I publish a mathematical theorem developed in Agda, I think it is fair to the reader to let them know what the universe level assignments are rather than just say that they exist. In some cases, as injectivity, the universe levels are crucial, and if we ignore them we get false claims. Best, 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+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 4066 bytes --] <div dir="ltr"><div>On 01/05/2019 03:50, Michael Shulman wrote:> Interesting point! I definitely agree that we don't want to be</div><div>> *forced* to be typically ambiguous; there are times when we need to</div><div>> explicitly distinguish universes. This was already the case in a few</div><div>> places in the book, e.g. Lemmas 10.3.21 and 10.3.22. And Coq's</div><div>> universe polymorphism now also *allows* the user to explicitly specify</div><div>> universe levels when desired. (On the other hand, it's also nice to</div><div>> not be forced to label all universes explicitly all the time. But on</div><div>> the third hard, at least in Coq as it is now, the interaction of</div><div>> user-specified universes with automatically-deduced ones seems to be</div><div>> fairly fragile.)</div><div>Right.</div><div><br></div><div>> However, it's not clear to me why cumulativity would be a problem.</div><div>In Agda each type gets a unique universe (or at most one universe) and</div><div>often (but not always) the system is able to infer them if we write</div><div>question marks "?" for them (but not always).</div><div><br></div><div>Cumulativity is not "on the nose" in the sense that from X : U_l you</div><div>would get X : U_m for m ≥ l. Instead, if you need to have (a copy of)</div><div>X in U_m, you need to use an explicit embedding U_l → U_m. (I only</div><div>ever used this embedding to show that U_l is a retract of U_m if we</div><div>assume propositional resizing.)</div><div><br></div><div>In practice, however, I never needed to use this embedding, as the</div><div>closure properties for universes work with more than one universe at a</div><div>time. For instance,</div><div><br></div><div> if X:U_l and A : X → U_m, then Π X A : U_{max l m}.</div><div><br></div><div>With this kind of closure property, I haven't encountered the</div><div>practical need for cumulativity.</div><div><br></div><div>It is nice, in practice, that universes are uniquely</div><div>determined. Insted of thousands of level constraints, we have a</div><div>unique, small, (polymorphic) level assignment.</div><div><br></div><div>> In fact you wrote in the paper that "We don't assume that the</div><div>> universes are cumulative... but we also don't assume that they are</div><div>> not". Which makes it sound as though cumulativity, though not</div><div>> necessary, wouldn't be a problem if it did hold -- would it?</div><div>In theory it wouldn't be a problem if it holds. However, if Agda did</div><div>have cumulativity, it would lose the unique-level assignment property</div><div>that I use to infer the levels of the results from my given levels of</div><div>the data. However, in the absence of a concrete proof assistant with</div><div>the option to enable and disable cumulativity, it is impossible to</div><div>perform experiments to confirm or reject this conjectural impression.</div><div><br></div><div>I consider the universe-level system of Agda to be excellent in</div><div>practice, and easy to use. Moreover, as I said, if I publish a</div><div>mathematical theorem developed in Agda, I think it is fair to the</div><div>reader to let them know what the universe level assignments are rather</div><div>than just say that they exist. In some cases, as injectivity, the</div><div>universe levels are crucial, and if we ignore them we get false</div><div>claims.</div><div><br></div><div>Best,</div><div>Martin</div><div><br></div></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> For more options, visit <a href="https://groups.google.com/d/optout">https://groups.google.com/d/optout</a>.<br />

On Tue, Apr 30, 2019 at 11:25 PM <escardo.martin@gmail.com> wrote: > It is nice, in practice, that universes are uniquely > determined. Insted of thousands of level constraints, we have a > unique, small, (polymorphic) level assignment. > ... > I think it is fair to the > reader to let them know what the universe level assignments are rather > than just say that they exist. In some cases, as injectivity, the > universe levels are crucial, and if we ignore them we get false > claims. Yes, this is a good point in favor of Agda-style non-cumulative Russell universes over Coq-style cumulative Russell universes. But isn't there a middle ground with Tarski universes? Suppose we have explicit lifting operators Lift : U_i -> U_{i+1}, so that as in Agda we have unique small polymorphic level assignments. But then suppose we have *definitional* equalities El(Lift(A)) == El(A). Then on the (rare) occasions when we do have to explicitly lift types from one universe to another, we would get stronger cumulativity behavior. (And I could imagine a proof assistant that implements this and sugars away the El to look like Russell universes to the user.) -- 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+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 2704 bytes --] On Wednesday, 1 May 2019 17:55:50 UTC+1, Michael Shulman wrote > > > Yes, this is a good point in favor of Agda-style non-cumulative > Russell universes over Coq-style cumulative Russell universes. > > But isn't there a middle ground with Tarski universes? It would be nice to have such a middle ground, particularly because formulating universe assumptions in each single definition and theorem is unfamiliar in mathematical practice, and so "typical ambiguity" (pretending there is only one universe) is potentially a good idea for many (or even most) examples. But not in the paper I advertised in this thread. Here I post an example when Giraud did precisely that, namely to assume two arbitrary universes U and V, explaining why this is needed in that level of generality after the formulation of a theorem and its proof, given to me by Thierry Coquand: https://www.cs.bham.ac.uk/~mhe/giraud-universes.pdf (photo of one page of a book). The book is “Cohmologie non abelienne” (1971, https://www.springer.com/gp/book/9783540053071). Suppose we > have explicit lifting operators Lift : U_i -> U_{i+1}, so that as in > Agda we have unique small polymorphic level assignments. But then > suppose we have *definitional* equalities El(Lift(A)) == El(A). Then > on the (rare) occasions when we do have to explicitly lift types from > one universe to another, I can confirm from a 26k line Agda development (with comments and repeated blank lines removed in this counting of the number of lines) that not once did I need to embed a universe into a larger universe, except when I wanted to state the theorem that any universe is a retract of any larger universe if one assumes the propositional resizing axiom (any proposition in a universe U has an equivalent copy in any universe V). So I would say that such situations are *extremely rare* in practice. > we would get stronger cumulativity behavior. > (And I could imagine a proof assistant that implements this and sugars > away the El to look like Russell universes to the user.) At the moment we can choose cumulativity (Coq) or non-cumulativity (Agda), and there is no system that combines the virtues of Coq and Agda regarding universe handling. (And I fear that such a system would potentially multiply the vices of both. :-) ) M. -- 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+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 3538 bytes --] <div dir="ltr"><br><br>On Wednesday, 1 May 2019 17:55:50 UTC+1, Michael Shulman wrote<blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><br>Yes, this is a good point in favor of Agda-style non-cumulative <br>Russell universes over Coq-style cumulative Russell universes. <br> <br>But isn't there a middle ground with Tarski universes? </blockquote><div><br></div><div>It would be nice to have such a middle ground, particularly because formulating universe assumptions in each single definition and theorem is unfamiliar in mathematical practice, and so "typical ambiguity" (pretending there is only one universe) is potentially a good idea for many (or even most) examples. But not in the paper I advertised in this thread.</div><div><br></div><div>Here I post an example when Giraud did precisely that, namely to assume two arbitrary universes U and V, explaining why this is needed in that level of generality after the formulation of a theorem and its proof, given to me by Thierry Coquand:</div><div><br></div><div> https://www.cs.bham.ac.uk/~mhe/giraud-universes.pdf (photo of one page of a book).<br></div><div> </div><div>The <span style="font-size: 10pt;">book is “Cohmologie non abelienne” (1971, </span><span style="font-size: 13.3333px;">https://www.springer.com/gp/book/9783540053071).</span></div><div><br></div><blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">Suppose we <br>have explicit lifting operators Lift : U_i -> U_{i+1}, so that as in <br>Agda we have unique small polymorphic level assignments. But then <br>suppose we have *definitional* equalities El(Lift(A)) == El(A). Then <br>on the (rare) occasions when we do have to explicitly lift types from <br>one universe to another, </blockquote><div><br></div><div>I can confirm from a 26k line Agda development (with comments and repeated blank lines removed in this counting of the number of lines) that not once did I need to embed a universe into a larger universe, except when I wanted to state the theorem that any universe is a retract of any larger universe if one assumes the propositional resizing axiom (any proposition in a universe U has an equivalent copy in any universe V). So I would say that such situations are *extremely rare* in practice.</div><div> <br></div><blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">we would get stronger cumulativity behavior. <br>(And I could imagine a proof assistant that implements this and sugars <br>away the El to look like Russell universes to the user.)</blockquote><div> <br></div><div>At the moment we can choose cumulativity (Coq) or non-cumulativity (Agda), and there is no system that combines the virtues of Coq and Agda regarding universe handling. (And I fear that such a system would potentially multiply the vices of both. :-) )</div><div><br></div><div>M.</div><div><br></div></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> For more options, visit <a href="https://groups.google.com/d/optout">https://groups.google.com/d/optout</a>.<br />

I am more optimistic: I think there's a good chance we could do better than both Coq and Agda. Of course sometimes when we try new things they flop; but we can't make progress without trying new things. For one thing, I don't think we should conflate typical ambiguity with cumulativity. It just so happens that Coq has both and Agda has neither, but in principle I see no reason they have to go together. I see typical ambiguity as basically syntactic sugar or abuse of notation, analogous to the use of implicit arguments: the reader or proof assistant is tasked (if they feel like it) to go through and insert level parameters as needed, accumulating constraints on these parameters according to how the instance are used and thereby "elaborating" a typically ambiguous development to a fully precise one with (polymorphic) universe levels. Usually this will be possible, but occasionally if the writer was careless there may be a universe inconsistency. It seems to me that this could be done in both a cumulative and a non-cumulative system. True, in a non-cumulative system we get different constraints, e.g. if we ever write "A=B" then it must be that A and B live in the same universe, whereas in a cumulative system we could be looser about such constraints. But your evidence (and that of other universe-polymorphic users of Agda) suggests that such constraints arising from non-cumulativity are not in practice a problem. In fact, the unique assignment of levels in a non-cumulative system suggests that the universe inference algorithm in a hypothetical typically-ambiguous non-cumulative proof assistant would probably be *simpler*, and less error-prone, than that of Coq. So I don't see any argument here against typical ambiguity, as long as there is the *option* to be unambiguous when necessary (which again, even Coq now supports). In particular, note that when a development is formalized in a typically ambiguous proof assistant, it's not necessary for the universe levels to be written in the source code, or even thought about by the author, in order for the interested reader -- or even the author themselves! -- to learn about what the universe constraints are. They only have to compile the code, in particular running it through the universe checker/elaborator, and then inspect the resulting universe levels/constraints. I've done this in present-day Coq myself, although the proliferation of universe parameters makes the output hard to undertsand; I expect it would only be easier in a hypothetical typically-ambiguous non-cumulative proof assistant. So it seems to me that it should be possible to be "fair to the reader", as you say, and still retain (some of) the advantages of typical ambiguity. I also think there's a good chance we can retain some cumulativity without losing the benefits of non-cumulativity, by using a Tarski-style lifting coercion as I sketched in my last email. (Isn't this in the literature somewhere? I didn't think I'd made it up.) I agree that it's rare to need this, but neither is it unheard-of; so if we can make it more convenient to use with no drawback, why not? (Of course, cumulativity is also trickier to model semantically, but probably possible.) On Thu, May 2, 2019 at 1:46 PM <escardo.martin@gmail.com> wrote: > > > > On Wednesday, 1 May 2019 17:55:50 UTC+1, Michael Shulman wrote >> >> >> Yes, this is a good point in favor of Agda-style non-cumulative >> Russell universes over Coq-style cumulative Russell universes. >> >> But isn't there a middle ground with Tarski universes? > > > It would be nice to have such a middle ground, particularly because formulating universe assumptions in each single definition and theorem is unfamiliar in mathematical practice, and so "typical ambiguity" (pretending there is only one universe) is potentially a good idea for many (or even most) examples. But not in the paper I advertised in this thread. > > Here I post an example when Giraud did precisely that, namely to assume two arbitrary universes U and V, explaining why this is needed in that level of generality after the formulation of a theorem and its proof, given to me by Thierry Coquand: > > https://www.cs.bham.ac.uk/~mhe/giraud-universes.pdf (photo of one page of a book). > > The book is “Cohmologie non abelienne” (1971, https://www.springer.com/gp/book/9783540053071). > >> Suppose we >> have explicit lifting operators Lift : U_i -> U_{i+1}, so that as in >> Agda we have unique small polymorphic level assignments. But then >> suppose we have *definitional* equalities El(Lift(A)) == El(A). Then >> on the (rare) occasions when we do have to explicitly lift types from >> one universe to another, > > > I can confirm from a 26k line Agda development (with comments and repeated blank lines removed in this counting of the number of lines) that not once did I need to embed a universe into a larger universe, except when I wanted to state the theorem that any universe is a retract of any larger universe if one assumes the propositional resizing axiom (any proposition in a universe U has an equivalent copy in any universe V). So I would say that such situations are *extremely rare* in practice. > >> >> we would get stronger cumulativity behavior. >> (And I could imagine a proof assistant that implements this and sugars >> away the El to look like Russell universes to the user.) > > > At the moment we can choose cumulativity (Coq) or non-cumulativity (Agda), and there is no system that combines the virtues of Coq and Agda regarding universe handling. (And I fear that such a system would potentially multiply the vices of both. :-) ) > > M. > > -- > 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+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- 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+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

I think the paper "A calculus of constructions with explicit subtyping" by Ali Assaf that can be found at https://hal.inria.fr/hal-01097401 is a relevant reference for coercive lifts between Tarski style universes. K. On 03/05/2019 13:45, Michael Shulman wrote: > I am more optimistic: I think there's a good chance we could do better > than both Coq and Agda. Of course sometimes when we try new things > they flop; but we can't make progress without trying new things. > > For one thing, I don't think we should conflate typical ambiguity with > cumulativity. It just so happens that Coq has both and Agda has > neither, but in principle I see no reason they have to go together. I > see typical ambiguity as basically syntactic sugar or abuse of > notation, analogous to the use of implicit arguments: the reader or > proof assistant is tasked (if they feel like it) to go through and > insert level parameters as needed, accumulating constraints on these > parameters according to how the instance are used and thereby > "elaborating" a typically ambiguous development to a fully precise one > with (polymorphic) universe levels. Usually this will be possible, > but occasionally if the writer was careless there may be a universe > inconsistency. > > It seems to me that this could be done in both a cumulative and a > non-cumulative system. True, in a non-cumulative system we get > different constraints, e.g. if we ever write "A=B" then it must be > that A and B live in the same universe, whereas in a cumulative system > we could be looser about such constraints. But your evidence (and > that of other universe-polymorphic users of Agda) suggests that such > constraints arising from non-cumulativity are not in practice a > problem. In fact, the unique assignment of levels in a non-cumulative > system suggests that the universe inference algorithm in a > hypothetical typically-ambiguous non-cumulative proof assistant would > probably be *simpler*, and less error-prone, than that of Coq. So I > don't see any argument here against typical ambiguity, as long as > there is the *option* to be unambiguous when necessary (which again, > even Coq now supports). > > In particular, note that when a development is formalized in a > typically ambiguous proof assistant, it's not necessary for the > universe levels to be written in the source code, or even thought > about by the author, in order for the interested reader -- or even the > author themselves! -- to learn about what the universe constraints > are. They only have to compile the code, in particular running it > through the universe checker/elaborator, and then inspect the > resulting universe levels/constraints. I've done this in present-day > Coq myself, although the proliferation of universe parameters makes > the output hard to undertsand; I expect it would only be easier in a > hypothetical typically-ambiguous non-cumulative proof assistant. So > it seems to me that it should be possible to be "fair to the reader", > as you say, and still retain (some of) the advantages of typical > ambiguity. > > I also think there's a good chance we can retain some cumulativity > without losing the benefits of non-cumulativity, by using a > Tarski-style lifting coercion as I sketched in my last email. (Isn't > this in the literature somewhere? I didn't think I'd made it up.) I > agree that it's rare to need this, but neither is it unheard-of; so if > we can make it more convenient to use with no drawback, why not? (Of > course, cumulativity is also trickier to model semantically, but > probably possible.) > > > > > > On Thu, May 2, 2019 at 1:46 PM <escardo.martin@gmail.com> wrote: >> >> >> On Wednesday, 1 May 2019 17:55:50 UTC+1, Michael Shulman wrote >>> >>> Yes, this is a good point in favor of Agda-style non-cumulative >>> Russell universes over Coq-style cumulative Russell universes. >>> >>> But isn't there a middle ground with Tarski universes? >> >> It would be nice to have such a middle ground, particularly because formulating universe assumptions in each single definition and theorem is unfamiliar in mathematical practice, and so "typical ambiguity" (pretending there is only one universe) is potentially a good idea for many (or even most) examples. But not in the paper I advertised in this thread. >> >> Here I post an example when Giraud did precisely that, namely to assume two arbitrary universes U and V, explaining why this is needed in that level of generality after the formulation of a theorem and its proof, given to me by Thierry Coquand: >> >> https://www.cs.bham.ac.uk/~mhe/giraud-universes.pdf (photo of one page of a book). >> >> The book is “Cohmologie non abelienne” (1971, https://www.springer.com/gp/book/9783540053071). >> >>> Suppose we >>> have explicit lifting operators Lift : U_i -> U_{i+1}, so that as in >>> Agda we have unique small polymorphic level assignments. But then >>> suppose we have *definitional* equalities El(Lift(A)) == El(A). Then >>> on the (rare) occasions when we do have to explicitly lift types from >>> one universe to another, >> >> I can confirm from a 26k line Agda development (with comments and repeated blank lines removed in this counting of the number of lines) that not once did I need to embed a universe into a larger universe, except when I wanted to state the theorem that any universe is a retract of any larger universe if one assumes the propositional resizing axiom (any proposition in a universe U has an equivalent copy in any universe V). So I would say that such situations are *extremely rare* in practice. >> >>> we would get stronger cumulativity behavior. >>> (And I could imagine a proof assistant that implements this and sugars >>> away the El to look like Russell universes to the user.) >> >> At the moment we can choose cumulativity (Coq) or non-cumulativity (Agda), and there is no system that combines the virtues of Coq and Agda regarding universe handling. (And I fear that such a system would potentially multiply the vices of both. :-) ) >> >> M. >> >> -- >> 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+unsubscribe@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. -- 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+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1: Type: text/plain, Size: 7311 bytes --] Indeed! There is also http://www.math.ias.edu/Voevodsky/files/files-annotated/Dropbox/Unfinished_papers/Type_systems/UPTS_current/Universe_polymorphic_type_sytem.pdf Thierry On 3 May 2019, at 15:25, Kenji Maillard <chocobodralliam@gmail.com<mailto:chocobodralliam@gmail.com>> wrote: I think the paper "A calculus of constructions with explicit subtyping" by Ali Assaf that can be found at https://hal.inria.fr/hal-01097401 is a relevant reference for coercive lifts between Tarski style universes. K. On 03/05/2019 13:45, Michael Shulman wrote: I am more optimistic: I think there's a good chance we could do better than both Coq and Agda. Of course sometimes when we try new things they flop; but we can't make progress without trying new things. For one thing, I don't think we should conflate typical ambiguity with cumulativity. It just so happens that Coq has both and Agda has neither, but in principle I see no reason they have to go together. I see typical ambiguity as basically syntactic sugar or abuse of notation, analogous to the use of implicit arguments: the reader or proof assistant is tasked (if they feel like it) to go through and insert level parameters as needed, accumulating constraints on these parameters according to how the instance are used and thereby "elaborating" a typically ambiguous development to a fully precise one with (polymorphic) universe levels. Usually this will be possible, but occasionally if the writer was careless there may be a universe inconsistency. It seems to me that this could be done in both a cumulative and a non-cumulative system. True, in a non-cumulative system we get different constraints, e.g. if we ever write "A=B" then it must be that A and B live in the same universe, whereas in a cumulative system we could be looser about such constraints. But your evidence (and that of other universe-polymorphic users of Agda) suggests that such constraints arising from non-cumulativity are not in practice a problem. In fact, the unique assignment of levels in a non-cumulative system suggests that the universe inference algorithm in a hypothetical typically-ambiguous non-cumulative proof assistant would probably be *simpler*, and less error-prone, than that of Coq. So I don't see any argument here against typical ambiguity, as long as there is the *option* to be unambiguous when necessary (which again, even Coq now supports). In particular, note that when a development is formalized in a typically ambiguous proof assistant, it's not necessary for the universe levels to be written in the source code, or even thought about by the author, in order for the interested reader -- or even the author themselves! -- to learn about what the universe constraints are. They only have to compile the code, in particular running it through the universe checker/elaborator, and then inspect the resulting universe levels/constraints. I've done this in present-day Coq myself, although the proliferation of universe parameters makes the output hard to undertsand; I expect it would only be easier in a hypothetical typically-ambiguous non-cumulative proof assistant. So it seems to me that it should be possible to be "fair to the reader", as you say, and still retain (some of) the advantages of typical ambiguity. I also think there's a good chance we can retain some cumulativity without losing the benefits of non-cumulativity, by using a Tarski-style lifting coercion as I sketched in my last email. (Isn't this in the literature somewhere? I didn't think I'd made it up.) I agree that it's rare to need this, but neither is it unheard-of; so if we can make it more convenient to use with no drawback, why not? (Of course, cumulativity is also trickier to model semantically, but probably possible.) On Thu, May 2, 2019 at 1:46 PM <escardo.martin@gmail.com<mailto:escardo.martin@gmail.com>> wrote: On Wednesday, 1 May 2019 17:55:50 UTC+1, Michael Shulman wrote Yes, this is a good point in favor of Agda-style non-cumulative Russell universes over Coq-style cumulative Russell universes. But isn't there a middle ground with Tarski universes? It would be nice to have such a middle ground, particularly because formulating universe assumptions in each single definition and theorem is unfamiliar in mathematical practice, and so "typical ambiguity" (pretending there is only one universe) is potentially a good idea for many (or even most) examples. But not in the paper I advertised in this thread. Here I post an example when Giraud did precisely that, namely to assume two arbitrary universes U and V, explaining why this is needed in that level of generality after the formulation of a theorem and its proof, given to me by Thierry Coquand: https://www.cs.bham.ac.uk/~mhe/giraud-universes.pdf (photo of one page of a book). The book is “Cohmologie non abelienne” (1971, https://www.springer.com/gp/book/9783540053071). Suppose we have explicit lifting operators Lift : U_i -> U_{i+1}, so that as in Agda we have unique small polymorphic level assignments. But then suppose we have *definitional* equalities El(Lift(A)) == El(A). Then on the (rare) occasions when we do have to explicitly lift types from one universe to another, I can confirm from a 26k line Agda development (with comments and repeated blank lines removed in this counting of the number of lines) that not once did I need to embed a universe into a larger universe, except when I wanted to state the theorem that any universe is a retract of any larger universe if one assumes the propositional resizing axiom (any proposition in a universe U has an equivalent copy in any universe V). So I would say that such situations are *extremely rare* in practice. we would get stronger cumulativity behavior. (And I could imagine a proof assistant that implements this and sugars away the El to look like Russell universes to the user.) At the moment we can choose cumulativity (Coq) or non-cumulativity (Agda), and there is no system that combines the virtues of Coq and Agda regarding universe handling. (And I fear that such a system would potentially multiply the vices of both. :-) ) M. -- 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+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. For more options, visit https://groups.google.com/d/optout. -- 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+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. For more options, visit https://groups.google.com/d/optout. -- 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+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 10524 bytes --] <html> <head> <meta http-equiv="Content-Type" content="text/html; charset=utf-8"> </head> <body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""> Indeed! <div class=""> There is also </div> <div class=""><br class=""> </div> <div class=""><a href="http://www.math.ias.edu/Voevodsky/files/files-annotated/Dropbox/Unfinished_papers/Type_systems/UPTS_current/Universe_polymorphic_type_sytem.pdf" class="">http://www.math.ias.edu/Voevodsky/files/files-annotated/Dropbox/Unfinished_papers/Type_systems/UPTS_current/Universe_polymorphic_type_sytem.pdf</a></div> <div class=""><br class=""> </div> <div class=""> Thierry<br class=""> <div><br class=""> <blockquote type="cite" class=""> <div class="">On 3 May 2019, at 15:25, Kenji Maillard <<a href="mailto:chocobodralliam@gmail.com" class="">chocobodralliam@gmail.com</a>> wrote:</div> <br class="Apple-interchange-newline"> <div class=""> <div class="">I think the paper "A calculus of constructions with explicit subtyping"<br class=""> by Ali Assaf that can be found at <a href="https://hal.inria.fr/hal-01097401" class=""> https://hal.inria.fr/hal-01097401</a> is<br class=""> a relevant reference for coercive lifts between Tarski style universes.<br class=""> <br class=""> K.<br class=""> <br class=""> On 03/05/2019 13:45, Michael Shulman wrote:<br class=""> <blockquote type="cite" class="">I am more optimistic: I think there's a good chance we could do better<br class=""> than both Coq and Agda. Of course sometimes when we try new things<br class=""> they flop; but we can't make progress without trying new things.<br class=""> <br class=""> For one thing, I don't think we should conflate typical ambiguity with<br class=""> cumulativity. It just so happens that Coq has both and Agda has<br class=""> neither, but in principle I see no reason they have to go together. I<br class=""> see typical ambiguity as basically syntactic sugar or abuse of<br class=""> notation, analogous to the use of implicit arguments: the reader or<br class=""> proof assistant is tasked (if they feel like it) to go through and<br class=""> insert level parameters as needed, accumulating constraints on these<br class=""> parameters according to how the instance are used and thereby<br class=""> "elaborating" a typically ambiguous development to a fully precise one<br class=""> with (polymorphic) universe levels. Usually this will be possible,<br class=""> but occasionally if the writer was careless there may be a universe<br class=""> inconsistency.<br class=""> <br class=""> It seems to me that this could be done in both a cumulative and a<br class=""> non-cumulative system. True, in a non-cumulative system we get<br class=""> different constraints, e.g. if we ever write "A=B" then it must be<br class=""> that A and B live in the same universe, whereas in a cumulative system<br class=""> we could be looser about such constraints. But your evidence (and<br class=""> that of other universe-polymorphic users of Agda) suggests that such<br class=""> constraints arising from non-cumulativity are not in practice a<br class=""> problem. In fact, the unique assignment of levels in a non-cumulative<br class=""> system suggests that the universe inference algorithm in a<br class=""> hypothetical typically-ambiguous non-cumulative proof assistant would<br class=""> probably be *simpler*, and less error-prone, than that of Coq. So I<br class=""> don't see any argument here against typical ambiguity, as long as<br class=""> there is the *option* to be unambiguous when necessary (which again,<br class=""> even Coq now supports).<br class=""> <br class=""> In particular, note that when a development is formalized in a<br class=""> typically ambiguous proof assistant, it's not necessary for the<br class=""> universe levels to be written in the source code, or even thought<br class=""> about by the author, in order for the interested reader -- or even the<br class=""> author themselves! -- to learn about what the universe constraints<br class=""> are. They only have to compile the code, in particular running it<br class=""> through the universe checker/elaborator, and then inspect the<br class=""> resulting universe levels/constraints. I've done this in present-day<br class=""> Coq myself, although the proliferation of universe parameters makes<br class=""> the output hard to undertsand; I expect it would only be easier in a<br class=""> hypothetical typically-ambiguous non-cumulative proof assistant. So<br class=""> it seems to me that it should be possible to be "fair to the reader",<br class=""> as you say, and still retain (some of) the advantages of typical<br class=""> ambiguity.<br class=""> <br class=""> I also think there's a good chance we can retain some cumulativity<br class=""> without losing the benefits of non-cumulativity, by using a<br class=""> Tarski-style lifting coercion as I sketched in my last email. (Isn't<br class=""> this in the literature somewhere? I didn't think I'd made it up.) I<br class=""> agree that it's rare to need this, but neither is it unheard-of; so if<br class=""> we can make it more convenient to use with no drawback, why not? (Of<br class=""> course, cumulativity is also trickier to model semantically, but<br class=""> probably possible.)<br class=""> <br class=""> <br class=""> <br class=""> <br class=""> <br class=""> On Thu, May 2, 2019 at 1:46 PM <<a href="mailto:escardo.martin@gmail.com" class="">escardo.martin@gmail.com</a>> wrote:<br class=""> <blockquote type="cite" class=""><br class=""> <br class=""> On Wednesday, 1 May 2019 17:55:50 UTC+1, Michael Shulman wrote<br class=""> <blockquote type="cite" class=""><br class=""> Yes, this is a good point in favor of Agda-style non-cumulative<br class=""> Russell universes over Coq-style cumulative Russell universes.<br class=""> <br class=""> But isn't there a middle ground with Tarski universes?<br class=""> </blockquote> <br class=""> It would be nice to have such a middle ground, particularly because formulating universe assumptions in each single definition and theorem is unfamiliar in mathematical practice, and so "typical ambiguity" (pretending there is only one universe) is potentially a good idea for many (or even most) examples. But not in the paper I advertised in this thread.<br class=""> <br class=""> Here I post an example when Giraud did precisely that, namely to assume two arbitrary universes U and V, explaining why this is needed in that level of generality after the formulation of a theorem and its proof, given to me by Thierry Coquand:<br class=""> <br class=""> <a href="https://www.cs.bham.ac.uk/~mhe/giraud-universes.pdf" class="">https://www.cs.bham.ac.uk/~mhe/giraud-universes.pdf</a> (photo of one page of a book).<br class=""> <br class=""> The book is “Cohmologie non abelienne” (1971, <a href="https://www.springer.com/gp/book/9783540053071" class=""> https://www.springer.com/gp/book/9783540053071</a>).<br class=""> <br class=""> <blockquote type="cite" class="">Suppose we<br class=""> have explicit lifting operators Lift : U_i -> U_{i+1}, so that as in<br class=""> Agda we have unique small polymorphic level assignments. But then<br class=""> suppose we have *definitional* equalities El(Lift(A)) == El(A). Then<br class=""> on the (rare) occasions when we do have to explicitly lift types from<br class=""> one universe to another,<br class=""> </blockquote> <br class=""> I can confirm from a 26k line Agda development (with comments and repeated blank lines removed in this counting of the number of lines) that not once did I need to embed a universe into a larger universe, except when I wanted to state the theorem that any universe is a retract of any larger universe if one assumes the propositional resizing axiom (any proposition in a universe U has an equivalent copy in any universe V). So I would say that such situations are *extremely rare* in practice.<br class=""> <br class=""> <blockquote type="cite" class="">we would get stronger cumulativity behavior.<br class=""> (And I could imagine a proof assistant that implements this and sugars<br class=""> away the El to look like Russell universes to the user.)<br class=""> </blockquote> <br class=""> At the moment we can choose cumulativity (Coq) or non-cumulativity (Agda), and there is no system that combines the virtues of Coq and Agda regarding universe handling. (And I fear that such a system would potentially multiply the vices of both. :-) )<br class=""> <br class=""> M.<br class=""> <br class=""> --<br class=""> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br class=""> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com" class="">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br class=""> For more options, visit <a href="https://groups.google.com/d/optout" class="">https://groups.google.com/d/optout</a>.<br class=""> </blockquote> </blockquote> <br class=""> -- <br class=""> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br class=""> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com" class="">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br class=""> For more options, visit <a href="https://groups.google.com/d/optout" class="">https://groups.google.com/d/optout</a>.<br class=""> </div> </div> </blockquote> </div> <br class=""> </div> </body> </html> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> For more options, visit <a href="https://groups.google.com/d/optout">https://groups.google.com/d/optout</a>.<br />

On 02/05/2019 22.46, escardo.martin@gmail.com wrote: > I can confirm from a 26k line Agda development (with comments and > repeated blank lines removed in this counting of the number of lines) > that not once did I need to embed a universe into a larger universe, > except when I wanted to state the theorem that any universe is a > retract of any larger universe if one assumes the propositional > resizing axiom (any proposition in a universe U has an equivalent copy > in any universe V). So I would say that such situations are *extremely > rare* in practice. I once wrote some code where I made use of univalence at three different levels. Does anyone know if one can prove that univalence at one level implies univalence at lower levels, without making use of cumulativity? -- /NAD -- 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+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/5fa99a80-56ed-abc5-d64f-876c192bca6a%40cse.gu.se. For more options, visit https://groups.google.com/d/optout.

Even with cumulativity, that sounds suspicious, because cumulativity of U in a bigger universe V does not obviously give you a map (A B : U) -> Id V A B -> Id U A B. The J-rule does not allow you to build this map. On 7/05/19 14:42, Nils Anders Danielsson wrote: > On 02/05/2019 22.46, escardo.martin@gmail.com wrote: >> I can confirm from a 26k line Agda development (with comments and >> repeated blank lines removed in this counting of the number of lines) >> that not once did I need to embed a universe into a larger universe, >> except when I wanted to state the theorem that any universe is a >> retract of any larger universe if one assumes the propositional >> resizing axiom (any proposition in a universe U has an equivalent copy >> in any universe V). So I would say that such situations are *extremely >> rare* in practice. > > I once wrote some code where I made use of univalence at three different > levels. Does anyone know if one can prove that univalence at one level > implies univalence at lower levels, without making use of cumulativity? > -- 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+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/49d95599-153c-d641-4ae9-a3f7c02b1cc3%40gmail.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 3219 bytes --] On 07/05/2019 14:51, Andreas Nuyts wrote: > Even with cumulativity, that sounds suspicious, because cumulativity of > U in a bigger universe V does not obviously give you a map > > (A B : U) -> Id V A B -> Id U A B. > > The J-rule does not allow you to build this map. Indeed. In the non-cumulative system, with V bigger than U, you have a map f : U → V with f A ≃ A. For example, if C is any contractible type in V, you can take f A := A × C. If both U and V are univalent, then any map f : U → V with f A ≃ A is an embedding for all A : U, meaning that the canonical map Id U A B → Id V (f A) (f B) is equivalence (or equivalently that the fibers of f are propositions). I checked this in Agda. The reformulation of your statement above with an explicit inclusion f : U → V, namely (A B : U) -> Id V (f A) (f B) -> Id U A B, which amounts to the left-cancellability of f, is a consequence of f being an embedding, and in general strictly weaker than f being an embedding. But I don't see how to prove even the left-cancellability of f without assuming univalence in the smaller universe U. Assuming that V is univalent, Id V (f A) (f B) gives f A ≃ f B, and then composing with the equivalences A ≃ f A and f B ≃ B we get A ≃ B. If U were univalent we would get Id U A B and hence f would be left-cancellable. But, as I said, the univalence of U and V gives more, namely that f is an embedding. And if V is univalent and f is an embedding, then U is univalent, for A ≃ B is equivalent to f A ≃ f B and hence to Id V (f A) (f B), and hence to Id U A B, using the embedding property in the last step. So if V is univalent, then the smaller universe U is univalent iff every map f : U → V with f A ≃ A for all A : U is an embedding (iff some given such map is an embedding). Martin > > On 7/05/19 14:42, Nils Anders Danielsson wrote: >> On 02/05/2019 22.46, escardo.martin@gmail.com wrote: >>> I can confirm from a 26k line Agda development (with comments and >>> repeated blank lines removed in this counting of the number of lines) >>> that not once did I need to embed a universe into a larger universe, >>> except when I wanted to state the theorem that any universe is a >>> retract of any larger universe if one assumes the propositional >>> resizing axiom (any proposition in a universe U has an equivalent copy >>> in any universe V). So I would say that such situations are *extremely >>> rare* in practice. >> >> I once wrote some code where I made use of univalence at three different >> levels. Does anyone know if one can prove that univalence at one level >> implies univalence at lower levels, without making use of cumulativity? -- 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+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/6bae18da-1ecc-4633-a565-9df222140d87%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 4371 bytes --] <div dir="ltr"><div>On 07/05/2019 14:51, Andreas Nuyts wrote:</div><div>> Even with cumulativity, that sounds suspicious, because cumulativity of </div><div>> U in a bigger universe V does not obviously give you a map</div><div>> </div><div>> (A B : U) -> Id V A B -> Id U A B.</div><div>> </div><div>> The J-rule does not allow you to build this map.</div><div><br></div><div>Indeed.</div><div><br></div><div>In the non-cumulative system, with V bigger than U, you have a map</div><div>f : U → V with f A ≃ A. For example, if C is any contractible type in</div><div>V, you can take f A := A × C.</div><div><br></div><div>If both U and V are univalent, then any map f : U → V with f A ≃ A is</div><div>an embedding for all A : U, meaning that the canonical map</div><div><br></div><div> Id U A B → Id V (f A) (f B)</div><div> </div><div>is equivalence (or equivalently that the fibers of f are propositions).</div><div>I checked this in Agda.</div><div><br></div><div>The reformulation of your statement above with an explicit inclusion</div><div>f : U → V, namely</div><div><br></div><div> (A B : U) -> Id V (f A) (f B) -> Id U A B,</div><div><br></div><div>which amounts to the left-cancellability of f, is a consequence of f</div><div>being an embedding, and in general strictly weaker than f being an</div><div>embedding.</div><div><br></div><div>But I don't see how to prove even the left-cancellability of f without</div><div>assuming univalence in the smaller universe U.</div><div><br></div><div>Assuming that V is univalent, Id V (f A) (f B) gives f A ≃ f B, and</div><div>then composing with the equivalences A ≃ f A and f B ≃ B we get A ≃ B.</div><div>If U were univalent we would get Id U A B and hence f would be</div><div>left-cancellable. But, as I said, the univalence of U and V gives</div><div>more, namely that f is an embedding.</div><div><br></div><div>And if V is univalent and f is an embedding, then U is univalent, for</div><div>A ≃ B is equivalent to f A ≃ f B and hence to Id V (f A) (f B), and</div><div>hence to Id U A B, using the embedding property in the last step.</div><div><br></div><div>So if V is univalent, then the smaller universe U is univalent iff</div><div>every map f : U → V with f A ≃ A for all A : U is an embedding (iff</div><div>some given such map is an embedding).</div><div><br></div><div>Martin</div><div><br></div><div>> </div><div>> On 7/05/19 14:42, Nils Anders Danielsson wrote:</div><div>>> On 02/05/2019 22.46, escardo.martin@gmail.com wrote:</div><div>>>> I can confirm from a 26k line Agda development (with comments and</div><div>>>> repeated blank lines removed in this counting of the number of lines)</div><div>>>> that not once did I need to embed a universe into a larger universe,</div><div>>>> except when I wanted to state the theorem that any universe is a</div><div>>>> retract of any larger universe if one assumes the propositional</div><div>>>> resizing axiom (any proposition in a universe U has an equivalent copy</div><div>>>> in any universe V). So I would say that such situations are *extremely</div><div>>>> rare* in practice.</div><div>>></div><div>>> I once wrote some code where I made use of univalence at three different</div><div>>> levels. Does anyone know if one can prove that univalence at one level</div><div>>> implies univalence at lower levels, without making use of cumulativity?</div><div><br></div></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/6bae18da-1ecc-4633-a565-9df222140d87%40googlegroups.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/6bae18da-1ecc-4633-a565-9df222140d87%40googlegroups.com</a>.<br /> For more options, visit <a href="https://groups.google.com/d/optout">https://groups.google.com/d/optout</a>.<br />