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

[Erik Palmgren <palmgren@math.su.se>]

Den 2018-11-07 kl. 13:21, skrev Martín Hötzel Escardó:
> 
> 
> 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.

Bishop seem rather antitheological about mathematics in his Manifesto. 
Anyway.

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

 From http://staff.math.su.se/palmgren/7.pdf:

"In conclusion, the notion of univalent category is too restrictive to 
cover many familiar examples. H-category is generalization of 
precategory and is a convenient version of E- category with equality on 
objects. The notion of E-category is still more general as shown here."

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