Re: [HoTT] Re: Precategories, Categories and Univalent categories

[Bas Spitters <b.a.w.spitters@gmail.com>]

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ó
<escardo.martin@gmail.com> 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.

-- 
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.