Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] Precategories, Categories and Univalent categories
@ 2018-11-07 10:03 Ali Caglayan
  2018-11-07 10:31 ` [HoTT] " Paolo Capriotti
                   ` (2 more replies)
  0 siblings, 3 replies; 46+ messages in thread
From: Ali Caglayan @ 2018-11-07 10:03 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- Attachment #1.1: Type: text/plain, Size: 1098 bytes --]

I want to get a general idea of peoples opinions when it comes to naming 
categories internal to HoTT.

On the one hand I have seen, in the HoTT book for example, precategory and 
category being used where the latter has the map idtoiso being an 
equivalence.

On the other hand I have seen people call these categories and univalent 
categories which is also fine.

Now because we have Rezk completion every precategory is yearning to become 
a category, so some might argue that a distinction isn't necessery. I would 
argue that the HoTT book convention is infact more misleading as 
"precategory" there is really just the usual notion of category. And a 
univalent category is some nice structure we can add to it because we are 
working in HoTT.

What are your thoughts and opinions on this?

-- 
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: 1393 bytes --]

^ permalink raw reply	[flat|nested] 46+ messages in thread

end of thread, other threads:[~2018-11-09 15:07 UTC | newest]

Thread overview: 46+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-11-07 10:03 [HoTT] Precategories, Categories and Univalent categories Ali Caglayan
2018-11-07 10:31 ` [HoTT] " Paolo Capriotti
2018-11-07 10:35 ` Ulrik Buchholtz
2018-11-07 10:37   ` Ulrik Buchholtz
2018-11-07 11:09   ` Peter LeFanu Lumsdaine
2018-11-07 11:43     ` Ulrik Buchholtz
2018-11-07 11:50       ` Erik Palmgren
2018-11-07 11:51       ` Ulrik Buchholtz
2018-11-07 12:03         ` Erik Palmgren
2018-11-07 12:21           ` Martín Hötzel Escardó
2018-11-07 13:00             ` Erik Palmgren
2018-11-07 13:02             ` Bas Spitters
2018-11-07 13:47               ` Ali Caglayan
2018-11-07 13:53               ` Thomas Streicher
2018-11-07 14:05                 ` Thorsten Altenkirch
2018-11-07 13:58       ` Thorsten Altenkirch
2018-11-07 14:14         ` Ulrik Buchholtz
2018-11-07 14:27           ` Peter LeFanu Lumsdaine
     [not found]             ` <CAOvivQyG1q9=3YoS8hX3bRQK0yi+mpBnJu+rqb3oon0uPLpZ4A@mail.gmail.com>
2018-11-07 20:01               ` Michael Shulman
2018-11-08 21:37               ` Martín Hötzel Escardó
2018-11-08 21:43                 ` Michael Shulman
2018-11-09  4:43                   ` Andrew Polonsky
2018-11-09 10:18                     ` Ulrik Buchholtz
2018-11-09 10:57                       ` Paolo Capriotti
2018-11-07 14:31           ` Thorsten Altenkirch
2018-11-07 14:05       ` Peter LeFanu Lumsdaine
2018-11-07 14:28         ` Ulrik Buchholtz
2018-11-07 15:35           ` Thomas Streicher
2018-11-07 16:54             ` Thorsten Altenkirch
2018-11-07 16:56               ` Thorsten Altenkirch
2018-11-07 17:31                 ` Eric Finster
2018-11-08 11:58               ` Thomas Streicher
2018-11-08 12:23                 ` [HoTT] " Emily Riehl
2018-11-08 12:28                   ` Emily Riehl
2018-11-08 14:01                     ` Thomas Streicher
2018-11-08 16:10                   ` Thomas Streicher
2018-11-08 14:38                 ` [HoTT] " Michael Shulman
2018-11-08 21:08                   ` Thomas Streicher
2018-11-08 21:30                     ` Michael Shulman
2018-11-09 11:56                       ` Thomas Streicher
2018-11-09 13:46                         ` Michael Shulman
2018-11-09 15:06                           ` Thomas Streicher
2018-11-08 16:01                 ` Thorsten Altenkirch
2018-11-08 19:39                   ` Thorsten Altenkirch
2018-11-07 20:00         ` Michael Shulman
2018-11-08 21:35 ` Martín Hötzel Escardó

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).