On Sun, Feb 17, 2019 at 1:25 AM Michael Shulman wrote: > The supposed arbitrariness of some types having strict eta and others > not has been mentioned at least twice. However, I don't find it > arbitrary at all [...] In particular, the difference in whether > Sigma-types have strict eta > or not simply lies in whether we are talking about positive > Sigma-types or negative Sigma-types Since I've mentioned eta for Sigma in this context: thanks for this explanation, Mike! -- Nicolai > -- 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.