I wrote the "category theory in HoTT" articles on the wiki. They are nothing more than what is already in the book. Part of the reason for this question is to make sure there is some agreement on what I am writing. On Wednesday, 7 November 2018 13:03:03 UTC, Bas Spitters wrote: > > We also have a wiki of course: > https://ncatlab.org/homotopytypetheory/show/HomePage > On Wed, Nov 7, 2018 at 1:21 PM Martín Hötzel Escardó > > wrote: > > > > > > > > On Wednesday, 7 November 2018 12:03:31 UTC, palmgren wrote: > >> > >> Setoid hell? This sounds like a sermon ... :-) > > > > > > This theological aspect seems to be an attribute of constructive > mathematics. We also have the Limited Principle of Omniscience. Both the > Setoid Hell was created and LPO was named by Bishop. Perhaps this is > justified by his very own name. > > > > But seriously, I would like to have the terminology for the various > types of categories settled and agreed among ourselves. I agree with the > mathematical argument given by Ulrik. I sympathize with Peter's argument, > which tries to avoid confusion, but I think in the long term it may cause > even more confusion. Maybe Ulrik's remarks should be added to the HoTT Book > and blogged at https://homotopytypetheory.org/blog/ > > > > 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.