Discussion of Homotopy Type Theory and Univalent Foundations
help / 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.

[-- Attachment #1.2: Type: text/html, Size: 1393 bytes --]

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

* [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-07 10:03 [HoTT] Precategories, Categories and Univalent categories Ali Caglayan
@ 2018-11-07 10:31  " Paolo Capriotti
2018-11-07 10:35  Ulrik Buchholtz
2018-11-08 21:35  Martín Hötzel Escardó
2 siblings, 0 replies; 46+ messages in thread
From: Paolo Capriotti @ 2018-11-07 10:31 UTC (permalink / raw)
To: Homotopy Type Theory

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

On Wed, 7 Nov 2018, at 10:03 AM, Ali Caglayan wrote:
> 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 wouldn't say that. Yes, there is an adjunction between categories and
precategories, but it's not an equivalence even in an ∞-categorical sense.
In fact, following Ayala and Francis, you can think of a precategory as a
category C equipped with the extra structure of a type X, and a surjective
(i.e. -1-connected) morphism X → obj C.

> What are your thoughts and opinions on this?

Whatever notion ends up being called *category*, I would say it ought to at
least be mapped to something that is (Quillen) equivalent to the usual
notion of category through the simplicial set interpretation. That suggests
categories should be univalent by default.

Best,
Paolo

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

[-- Attachment #1.2: Type: text/html, Size: 1430 bytes --]

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

* [HoTT] Re: Precategories, Categories and Univalent categories
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-08 21:35  Martín Hötzel Escardó
2 siblings, 2 replies; 46+ messages in thread
From: Ulrik Buchholtz @ 2018-11-07 10:35 UTC (permalink / raw)
To: Homotopy Type Theory

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

Hi,

First, there are (at least) three mathematically important and useful
types: precategories, strict (or set) categories (precategories with a set
of objects), and (univalent) categories.

I take as one main lesson from HoTT/UF that mathematical objects have
types, and that the identity types should indicate the relevant notion of
identity.

The type of precategories is equivalent to that of type-flagged categories
(categories together with a type O and a function from O to the objects of
the category). (The equivalence is given by pulling back the category
structure to get a precategory structure with O as the type of objects in
one way, and taking the Rezk completion together with the object part of
unit map in the other.)

Two precategories are identified via an equivalence of the O-types and an
equivalence of the categories, together with a witness that the square
commutes.

Two strict categories are identified via an isomorphism, and two
(univalent) categories are identified via an equivalence.

So I disagree that "precategory" is the usual notion of category: it can't
be because the criterion of identity is different. But it's still a useful
concept.

I personally prefer to keep “category” for univalent precategory, as most
often constructions on categories are meant to be well-defined up to
equivalence of categories. In the category theory literature written in a
set-theory metatheory where the distinction is not so clear, you can of
course find plenty of uses of the word “category” where “strict category”
is meant from a HoTT/UF point-of-view. The type of precategories as a
common generalization of strict and univalent categories is, I think, a new
concept to HoTT/UF. (Although infinity-groupoid flagged
(infinity,1)-categories arose independently in homotopy theory; these could
also be called (infinity,1)-precategories.)

Cheers,
Ulrik

On Wednesday, November 7, 2018 at 11:03:17 AM UTC+1, Ali Caglayan wrote:
>
> 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.

[-- Attachment #1.2: Type: text/html, Size: 3733 bytes --]

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

* [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-07 10:35  Ulrik Buchholtz
@ 2018-11-07 10:37    Ulrik Buchholtz
2018-11-07 11:09    Peter LeFanu Lumsdaine
1 sibling, 0 replies; 46+ messages in thread
From: Ulrik Buchholtz @ 2018-11-07 10:37 UTC (permalink / raw)
To: Homotopy Type Theory

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

Mine and Paolo's replies crossed, but of course I missed the condition that
the function be surjective.

On Wednesday, November 7, 2018 at 11:35:11 AM UTC+1, Ulrik Buchholtz wrote:
>
> Hi,
>
> First, there are (at least) three mathematically important and useful
> types: precategories, strict (or set) categories (precategories with a set
> of objects), and (univalent) categories.
>
> I take as one main lesson from HoTT/UF that mathematical objects have
> types, and that the identity types should indicate the relevant notion of
> identity.
>
> The type of precategories is equivalent to that of type-flagged categories
> (categories together with a type O and a function from O to the objects of
> the category). (The equivalence is given by pulling back the category
> structure to get a precategory structure with O as the type of objects in
> one way, and taking the Rezk completion together with the object part of
> unit map in the other.)
>
> Two precategories are identified via an equivalence of the O-types and an
> equivalence of the categories, together with a witness that the square
> commutes.
>
> Two strict categories are identified via an isomorphism, and two
> (univalent) categories are identified via an equivalence.
>
> So I disagree that "precategory" is the usual notion of category: it can't
> be because the criterion of identity is different. But it's still a useful
> concept.
>
> I personally prefer to keep “category” for univalent precategory, as most
> often constructions on categories are meant to be well-defined up to
> equivalence of categories. In the category theory literature written in a
> set-theory metatheory where the distinction is not so clear, you can of
> course find plenty of uses of the word “category” where “strict category”
> is meant from a HoTT/UF point-of-view. The type of precategories as a
> common generalization of strict and univalent categories is, I think, a new
> concept to HoTT/UF. (Although infinity-groupoid flagged
> (infinity,1)-categories arose independently in homotopy theory; these could
> also be called (infinity,1)-precategories.)
>
> Cheers,
> Ulrik
>
> On Wednesday, November 7, 2018 at 11:03:17 AM UTC+1, Ali Caglayan wrote:
>>
>> 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.

[-- Attachment #1.2: Type: text/html, Size: 4068 bytes --]

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
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
From: Peter LeFanu Lumsdaine @ 2018-11-07 11:09 UTC (permalink / raw)
To: Ulrik Buchholtz; +Cc: HomotopyTypeTheory

[-- Attachment #1: Type: text/plain, Size: 1835 bytes --]

Ulrik’s email nicely lays out the three key notions (pre-category, strict
category, univalent category), and the argument for the
Ahrens–Kapulkin–Shulman / HoTT book terminology, with “category” meaning
“univalent category” by default.

For my part I lean the other way: I think it’s too radical to use
“category” for a definition which doesn’t come out equivalent to the
traditional definition under the naïve set interpretation (or under the
addition of UIP to the type theory).  Choosing terminology that actively
clashes with traditional terminology makes it much harder to compare
statements in HoTT with their classical analogues, and see what difference
HoTT really makes to the development of topics.

Based on that criterion, I strongly prefer taking category to mean
“precategory”.  A big payoff from this is that if you formalise something
using “category ” to mean “precategory” in type theory without assuming UA,
then you can read the result either as valid in HoTT, or (under the
set-interpretation) as ordinary arguments in classical category theory,
with all the terms meaning just what they traditionally would.

Univalence of categories is an important and powerful property, but not an
innocuous one; it changes the character of the resulting “category theory”
in interesting ways.  Making the restriction to univalent categories tacit
understanding its effects.

–p.

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

[-- Attachment #2: Type: text/html, Size: 2111 bytes --]

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-07 11:09    Peter LeFanu Lumsdaine
@ 2018-11-07 11:43      Ulrik Buchholtz
2018-11-07 11:50        Erik Palmgren
(3 more replies)
0 siblings, 4 replies; 46+ messages in thread
From: Ulrik Buchholtz @ 2018-11-07 11:43 UTC (permalink / raw)
To: Homotopy Type Theory

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

I'm a bit confused by your message, Peter: HoTT doesn't have a naive set
interpretation and is inconsistent with UIP, so I'm not sure how that
should guide us. (Maybe if we're working in good old (agnostic?) MLTT?)

As I tried to say, I find that precategory is the novel concept, and that
both strict category and univalent category should be familiar to category
theorists. (They have a mental model for when one notion is called for or
the other, but we can make the distinction formal.)

On Wednesday, November 7, 2018 at 12:10:10 PM UTC+1, Peter LeFanu Lumsdaine
wrote:
>
> Ulrik’s email nicely lays out the three key notions (pre-category, strict
> category, univalent category), and the argument for the
> Ahrens–Kapulkin–Shulman / HoTT book terminology, with “category” meaning
> “univalent category” by default.
>
> For my part I lean the other way: I think it’s too radical to use
> “category” for a definition which doesn’t come out equivalent to the
> traditional definition under the naïve set interpretation (or under the
> addition of UIP to the type theory).  Choosing terminology that actively
> clashes with traditional terminology makes it much harder to compare
> statements in HoTT with their classical analogues, and see what difference
> HoTT really makes to the development of topics.
>
> Based on that criterion, I strongly prefer taking category to mean
> “precategory”.  A big payoff from this is that if you formalise something
> using “category ” to mean “precategory” in type theory without assuming UA,
> then you can read the result either as valid in HoTT, or (under the
> set-interpretation) as ordinary arguments in classical category theory,
> with all the terms meaning just what they traditionally would.
>
> Univalence of categories is an important and powerful property, but not an
> innocuous one; it changes the character of the resulting “category theory”
> in interesting ways.  Making the restriction to univalent categories tacit
> understanding its effects.
>
> –p.
>
>

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

[-- Attachment #1.2: Type: text/html, Size: 2912 bytes --]

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-07 11:43      Ulrik Buchholtz
@ 2018-11-07 11:50        Erik Palmgren
2018-11-07 11:51        Ulrik Buchholtz
(2 subsequent siblings)
3 siblings, 0 replies; 46+ messages in thread
From: Erik Palmgren @ 2018-11-07 11:50 UTC (permalink / raw)
To: Ulrik Buchholtz, Homotopy Type Theory

There is a paper to appear in TYPES 2017 postproceeding that discusses
this from the old MLTT perspective

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

Erik

Den 2018-11-07 kl. 12:43, skrev Ulrik Buchholtz:
> I'm a bit confused by your message, Peter: HoTT doesn't have a naive set
> interpretation and is inconsistent with UIP, so I'm not sure how that
> should guide us. (Maybe if we're working in good old (agnostic?) MLTT?)
>
> As I tried to say, I find that precategory is the novel concept, and
> that both strict category and univalent category should be familiar to
> category theorists. (They have a mental model for when one notion is
> called for or the other, but we can make the distinction formal.)
>
> On Wednesday, November 7, 2018 at 12:10:10 PM UTC+1, Peter LeFanu
> Lumsdaine wrote:
>
>     Ulrik’s email nicely lays out the three key notions (pre-category,
>     strict category, univalent category), and the argument for the
>     Ahrens–Kapulkin–Shulman / HoTT book terminology, with “category”
>     meaning “univalent category” by default.
>
>     For my part I lean the other way: I think it’s too radical to use
>     “category” for a definition which doesn’t come out equivalent to the
>     traditional definition under the naïve set interpretation (or under
>     the addition of UIP to the type theory).  Choosing terminology that
>     actively clashes with traditional terminology makes it much harder
>     to compare statements in HoTT with their classical analogues, and
>     see what difference HoTT really makes to the development of topics.
>
>     Based on that criterion, I strongly prefer taking category to mean
>     “precategory”.  A big payoff from this is that if you formalise
>     something using “category ” to mean “precategory” in type theory
>     without assuming UA, then you can read the result either as valid in
>     HoTT, or (under the set-interpretation) as ordinary arguments in
>     classical category theory, with all the terms meaning just what they
>
>     Univalence of categories is an important and powerful property, but
>     not an innocuous one; it changes the character of the resulting
>     “category theory” in interesting ways.  Making the restriction to
>     “insiders”, and obscures understanding its effects.
>
>     –p.
>
> --
> 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
> 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.

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
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 13:58        Thorsten Altenkirch
2018-11-07 14:05        Peter LeFanu Lumsdaine
From: Ulrik Buchholtz @ 2018-11-07 11:51 UTC (permalink / raw)
To: Homotopy Type Theory

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

Let me add one more point: in agnostic type theory, we can't define the
type of (Cauchy) real numbers, so we make do with the setoid of Cauchy
sequences. Likewise, we can't define the type of (univalent) categories, so
we make do with the 2-groupoid of precategories, equivalences and natural
isomorphisms.

In agnostic type theory we are both in setoid and higher groupoid hell. In
set theory/extensional type theory, we can escape the setoid hell, but
still have the higher groupoid hell, and in HoTT we can finally escape this
particular family of infernos :)

On Wednesday, November 7, 2018 at 12:43:32 PM UTC+1, Ulrik Buchholtz wrote:
>
> I'm a bit confused by your message, Peter: HoTT doesn't have a naive set
> interpretation and is inconsistent with UIP, so I'm not sure how that
> should guide us. (Maybe if we're working in good old (agnostic?) MLTT?)
>
> As I tried to say, I find that precategory is the novel concept, and that
> both strict category and univalent category should be familiar to category
> theorists. (They have a mental model for when one notion is called for or
> the other, but we can make the distinction formal.)
>
> On Wednesday, November 7, 2018 at 12:10:10 PM UTC+1, Peter LeFanu
> Lumsdaine wrote:
>>
>> Ulrik’s email nicely lays out the three key notions (pre-category, strict
>> category, univalent category), and the argument for the
>> Ahrens–Kapulkin–Shulman / HoTT book terminology, with “category” meaning
>> “univalent category” by default.
>>
>> For my part I lean the other way: I think it’s too radical to use
>> “category” for a definition which doesn’t come out equivalent to the
>> traditional definition under the naïve set interpretation (or under the
>> addition of UIP to the type theory).  Choosing terminology that actively
>> clashes with traditional terminology makes it much harder to compare
>> statements in HoTT with their classical analogues, and see what difference
>> HoTT really makes to the development of topics.
>>
>> Based on that criterion, I strongly prefer taking category to mean
>> “precategory”.  A big payoff from this is that if you formalise something
>> using “category ” to mean “precategory” in type theory without assuming UA,
>> then you can read the result either as valid in HoTT, or (under the
>> set-interpretation) as ordinary arguments in classical category theory,
>> with all the terms meaning just what they traditionally would.
>>
>> Univalence of categories is an important and powerful property, but not
>> an innocuous one; it changes the character of the resulting “category
>> theory” in interesting ways.  Making the restriction to univalent
>> categories tacit is misleading to readers who aren’t fully “insiders”, and
>> obscures understanding its effects.
>>
>> –p.
>>
>>

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

[-- Attachment #1.2: Type: text/html, Size: 3741 bytes --]

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-07 11:51        Ulrik Buchholtz
@ 2018-11-07 12:03          Erik Palmgren
2018-11-07 12:21            Martín Hötzel Escardó
From: Erik Palmgren @ 2018-11-07 12:03 UTC (permalink / raw)
To: Ulrik Buchholtz, Homotopy Type Theory

Setoid hell? This sounds like a sermon ... :-)  I think the critique
needs to be a little more specific.

Den 2018-11-07 kl. 12:51, skrev Ulrik Buchholtz:
> Let me add one more point: in agnostic type theory, we can't define the
> type of (Cauchy) real numbers, so we make do with the setoid of Cauchy
> sequences. Likewise, we can't define the type of (univalent) categories,
> so we make do with the 2-groupoid of precategories, equivalences and
> natural isomorphisms.
>
> In agnostic type theory we are both in setoid and higher groupoid hell.
> In set theory/extensional type theory, we can escape the setoid hell,
> but still have the higher groupoid hell, and in HoTT we can finally
> escape this particular family of infernos :)
>
> On Wednesday, November 7, 2018 at 12:43:32 PM UTC+1, Ulrik Buchholtz wrote:
>
>     I'm a bit confused by your message, Peter: HoTT doesn't have a naive
>     set interpretation and is inconsistent with UIP, so I'm not sure how
>     that should guide us. (Maybe if we're working in good old
>     (agnostic?) MLTT?)
>
>     As I tried to say, I find that precategory is the novel concept, and
>     that both strict category and univalent category should be familiar
>     to category theorists. (They have a mental model for when one notion
>     is called for or the other, but we can make the distinction formal.)
>
>     On Wednesday, November 7, 2018 at 12:10:10 PM UTC+1, Peter LeFanu
>     Lumsdaine wrote:
>
>         Ulrik’s email nicely lays out the three key notions
>         (pre-category, strict category, univalent category), and the
>         argument for the Ahrens–Kapulkin–Shulman / HoTT book
>         terminology, with “category” meaning “univalent category” by
>         default.
>
>         For my part I lean the other way: I think it’s too radical to
>         use “category” for a definition which doesn’t come out
>         equivalent to the traditional definition under the naïve set
>         interpretation (or under the addition of UIP to the type
>         theory).  Choosing terminology that actively clashes with
>         traditional terminology makes it much harder to compare
>         statements in HoTT with their classical analogues, and see what
>         difference HoTT really makes to the development of topics.
>
>         Based on that criterion, I strongly prefer taking category to
>         mean “precategory”.  A big payoff from this is that if you
>         formalise something using “category ” to mean “precategory” in
>         type theory without assuming UA, then you can read the result
>         either as valid in HoTT, or (under the set-interpretation) as
>         ordinary arguments in classical category theory, with all the
>         terms meaning just what they traditionally would.
>
>         Univalence of categories is an important and powerful property,
>         but not an innocuous one; it changes the character of the
>         resulting “category theory” in interesting ways.  Making the
>         restriction to univalent categories tacit is misleading to
>         readers who aren’t fully “insiders”, and obscures understanding
>         its effects.
>
>         –p.
>
> --
> 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
> 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.

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
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
0 siblings, 2 replies; 46+ messages in thread
From: Martín Hötzel Escardó @ 2018-11-07 12:21 UTC (permalink / raw)
To: Homotopy Type Theory

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

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.

[-- Attachment #1.2: Type: text/html, Size: 1498 bytes --]

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-07 12:21            Martín Hötzel Escardó
@ 2018-11-07 13:00              Erik Palmgren
2018-11-07 13:02              Bas Spitters
1 sibling, 0 replies; 46+ messages in thread
From: Erik Palmgren @ 2018-11-07 13:00 UTC (permalink / raw)
To: Martín Hötzel Escardó, Homotopy Type Theory

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

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
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
1 sibling, 2 replies; 46+ messages in thread
From: Bas Spitters @ 2018-11-07 13:02 UTC (permalink / raw)
To: Martín Hötzel Escardó; +Cc: homotopytypetheory

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.

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-07 13:02              Bas Spitters
@ 2018-11-07 13:47                Ali Caglayan
2018-11-07 13:53                Thomas Streicher
1 sibling, 0 replies; 46+ messages in thread
From: Ali Caglayan @ 2018-11-07 13:47 UTC (permalink / raw)
To: Homotopy Type Theory

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

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

[-- Attachment #1.2: Type: text/html, Size: 3260 bytes --]

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
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
From: Thomas Streicher @ 2018-11-07 13:53 UTC (permalink / raw)
To: Bas Spitters; +Cc: Martín Hötzel Escardó, homotopytypetheory

It would appear to me as natural to call "categories" the most general
notion and "univalent" those ones which validate the univalence axiom.
In any case the word "category" should not imply univalence.

But there is a point that one might call the most general notion
"precategory" and "categories" those precategories whose hom types
validate UIP, i.e. are sets.

But then univalent categories are not categories but just precategories.
Why not call the general notion "\infty-category" as usual?

Thomas

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

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-07 11:43      Ulrik Buchholtz
2018-11-07 11:50        Erik Palmgren
2018-11-07 11:51        Ulrik Buchholtz
@ 2018-11-07 13:58        Thorsten Altenkirch
2018-11-07 14:14          Ulrik Buchholtz
2018-11-07 14:05        Peter LeFanu Lumsdaine
From: Thorsten Altenkirch @ 2018-11-07 13:58 UTC (permalink / raw)
To: Ulrik Buchholtz, Homotopy Type Theory

[-- Attachment #1: Type: text/plain, Size: 4319 bytes --]

I'm a bit confused by your message, Peter: HoTT doesn't have a naive set interpretation and is inconsistent with UIP, so I'm not sure how that should guide us. (Maybe if we're working in good old (agnostic?) MLTT?)

As I tried to say, I find that precategory is the novel concept, and that both strict category and univalent category should be familiar to category theorists. (They have a mental model for when one notion is called for or the other, but we can make the distinction formal.)

This is too clever!

If you just transcribe the traditional definition of a category in type theory you end up with what in the HoTT book is called precategory. This is confusing for the non-expert even though you can justify why it should be so.

Hence I think the terminology category / univalent category is preferable. This also maintains the traditional wisdom that categories (with trivial ie.e propositional homsets) correspond to preorders. We may add that univalent categories correspond to partial orders.

And yes indeed there is something wrong with preorders because they have equality and equivalence and hence it is better to have a preorder. The same holds for categories, you have both equality and isomorphism and hence it is better to have a univalent category.

Thorsten

From: <homotopytypetheory@googlegroups.com> on behalf of Ulrik Buchholtz <ulrikbuchholtz@gmail.com>
Date: Wednesday, 7 November 2018 at 11:44
Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories

On Wednesday, November 7, 2018 at 12:10:10 PM UTC+1, Peter LeFanu Lumsdaine wrote:
Ulrik’s email nicely lays out the three key notions (pre-category, strict category, univalent category), and the argument for the Ahrens–Kapulkin–Shulman / HoTT book terminology, with “category” meaning “univalent category” by default.

For my part I lean the other way: I think it’s too radical to use “category” for a definition which doesn’t come out equivalent to the traditional definition under the naïve set interpretation (or under the addition of UIP to the type theory).  Choosing terminology that actively clashes with traditional terminology makes it much harder to compare statements in HoTT with their classical analogues, and see what difference HoTT really makes to the development of topics.

Based on that criterion, I strongly prefer taking category to mean “precategory”.  A big payoff from this is that if you formalise something using “category ” to mean “precategory” in type theory without assuming UA, then you can read the result either as valid in HoTT, or (under the set-interpretation) as ordinary arguments in classical category theory, with all the terms meaning just what they traditionally would.

Univalence of categories is an important and powerful property, but not an innocuous one; it changes the character of the resulting “category theory” in interesting ways.  Making the restriction to univalent categories tacit is misleading to readers who aren’t fully “insiders”, and obscures understanding its effects.

–p.

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

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
attachment.

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.

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

[-- Attachment #2: Type: text/html, Size: 9430 bytes --]

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-07 11:43      Ulrik Buchholtz
(2 preceding siblings ...)
2018-11-07 13:58        Thorsten Altenkirch
@ 2018-11-07 14:05        Peter LeFanu Lumsdaine
2018-11-07 14:28          Ulrik Buchholtz
2018-11-07 20:00          Michael Shulman
3 siblings, 2 replies; 46+ messages in thread
From: Peter LeFanu Lumsdaine @ 2018-11-07 14:05 UTC (permalink / raw)
To: Ulrik Buchholtz; +Cc: HomotopyTypeTheory

[-- Attachment #1: Type: text/plain, Size: 2178 bytes --]

On Wed, Nov 7, 2018 at 12:43 PM Ulrik Buchholtz <ulrikbuchholtz@gmail.com>
wrote:

> I'm a bit confused by your message, Peter: HoTT doesn't have a naive set
> interpretation and is inconsistent with UIP, so I'm not sure how that
> should guide us. (Maybe if we're working in good old (agnostic?) MLTT?)
>

Yep, I indeed meant “agnostic” MLTT — in particular, without univalence (or
roughly-equivalent things like the glue-types of cubical type theory).
There are lots of motivations for working over that as far as possible:
baking univalence into material where it’s not really required feels like
when classical mathematicians make use of AC for no real advantage.

As I tried to say, I find that precategory is the novel concept, and that
> both strict category and univalent category should be familiar to category
> theorists. (They have a mental model for when one notion is called for or
> the other, but we can make the distinction formal.)
>

I would argue both are familiar to traditional category theorists.  It’s
not unusual to make use of, for instance, the small model for FinSet where
the set of objects is taken as N — call this FinSet_N, say.  Category
theorists would certainly say that there’s a difference in character
between FinSet_N and FinSet itself: FinSet_N is small; and I think they
would also agree that they’re conscious informally of an extra character
FinSet has, which in HoTT can be precisely expressed as its univalence.

But do you really think they don’t consider FinSet_N to be a category??  I
find that very hard to believe: I am pretty sure that most traditional
category theorists would consider FinSet_N a category without any doubt at
all, which really seems to imply that the standard concept of category is
more like “precategory” than “univalent category”.

–p.

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

[-- Attachment #2: Type: text/html, Size: 2942 bytes --]

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-07 13:53                Thomas Streicher
@ 2018-11-07 14:05                  Thorsten Altenkirch
0 siblings, 0 replies; 46+ messages in thread
From: Thorsten Altenkirch @ 2018-11-07 14:05 UTC (permalink / raw)
To: Thomas Streicher, Bas Spitters
Cc: Martín Hötzel Escardó, homotopytypetheory

Something that only satisfies the axioms of a category but whose homs are not sets I would call a "wild category".

So yes a category needs to have homsets otherwise you have to give it a number.  And -1-categories already have a name they are called preorders.

I think the interesting notion for HoTT are categories whose Homs are types and which fullfill all the coherence conditions, i.e. they correspond to (\infty,1)-categories. Nicolai and Paolo gave a definition of univalent (\infty,1)-cats in 2-level HoTT as "complete Segal types". From this one can aslo derive non-univalent (\inft,1)-cats but in this case it is easier to define the univalent version because then you don't have to deal with degeneracies.

Thorsten

It would appear to me as natural to call "categories" the most general
notion and "univalent" those ones which validate the univalence axiom.
In any case the word "category" should not imply univalence.

But there is a point that one might call the most general notion
"precategory" and "categories" those precategories whose hom types
validate UIP, i.e. are sets.

But then univalent categories are not categories but just precategories.
Why not call the general notion "\infty-category" as usual?

Thomas

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

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
attachment.

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.

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

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-07 13:58        Thorsten Altenkirch
@ 2018-11-07 14:14          Ulrik Buchholtz
2018-11-07 14:27            Peter LeFanu Lumsdaine
2018-11-07 14:31            Thorsten Altenkirch
0 siblings, 2 replies; 46+ messages in thread
From: Ulrik Buchholtz @ 2018-11-07 14:14 UTC (permalink / raw)
To: Homotopy Type Theory

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

On Wednesday, November 7, 2018 at 2:58:28 PM UTC+1, Thorsten Altenkirch
wrote:
>
> As I tried to say, I find that precategory is the novel concept, and that
> both strict category and univalent category should be familiar to category
> theorists. (They have a mental model for when one notion is called for or
> the other, but we can make the distinction formal.)
>
>
> This is too clever!
>
>
>
> If you just transcribe the traditional definition of a category in type
> theory you end up with what in the HoTT book is called precategory. This is
> confusing for the non-expert even though you can justify why it should be
> so.
>

No, you get the notion of a strict category, which in some sense is all
that you directly have in set theory. (To get the (2,1)-category of
univalent categories, you take the homotopy (2,1)-category of the folk
model structure on the category(?!) of strict categories.)

As I said before, the notion of strict category is useful, and encompasses
the examples that Erik was missing from univalent categories.

But from a HoTT/UF point of view, the notion of strict category has the
drawback that you cannot get a strict category of sets (or groups or…)
without assuming the axiom (a homotopical taboo) that sets cover.

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

[-- Attachment #1.2: Type: text/html, Size: 2176 bytes --]

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
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 14:31            Thorsten Altenkirch
From: Peter LeFanu Lumsdaine @ 2018-11-07 14:27 UTC (permalink / raw)
To: Ulrik Buchholtz; +Cc: HomotopyTypeTheory

[-- Attachment #1: Type: text/plain, Size: 1770 bytes --]

On Wed, Nov 7, 2018 at 3:14 PM Ulrik Buchholtz <ulrikbuchholtz@gmail.com>
wrote:

> On Wednesday, November 7, 2018 at 2:58:28 PM UTC+1, Thorsten Altenkirch
> wrote:
>>
>> As I tried to say, I find that precategory is the novel concept, and that
>> both strict category and univalent category should be familiar to category
>> theorists. (They have a mental model for when one notion is called for or
>> the other, but we can make the distinction formal.)
>>
>>
>> This is too clever!
>>
>>
>>
>> If you just transcribe the traditional definition of a category in type
>> theory you end up with what in the HoTT book is called precategory. This is
>> confusing for the non-expert even though you can justify why it should be
>> so.
>>
>
> No, you get the notion of a strict category, which in some sense is all
> that you directly have in set theory.
>

No in turn: you can arguably get either strict categories, or
precategories, or what Thorsten dubbed “wild categories” above, since “set”
in set theory is the (naïve) interpretation of both “set” and “type”.
(Just as when you transcribe classical definitions in a constructive
setting, you sometimes want to read “predicate” just as “predicate” and
other times as “decidable predicate” — all predicates are decidable
classically, but that doesn’t mean that their constructive transcription
should include “decidable” by default.)

–p.

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

[-- Attachment #2: Type: text/html, Size: 2667 bytes --]

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
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 20:00          Michael Shulman
From: Ulrik Buchholtz @ 2018-11-07 14:28 UTC (permalink / raw)
To: Homotopy Type Theory

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

On Wednesday, November 7, 2018 at 3:05:44 PM UTC+1, Peter LeFanu Lumsdaine
wrote:
>
> Yep, I indeed meant “agnostic” MLTT — in particular, without univalence
> (or roughly-equivalent things like the glue-types of cubical type theory).
> There are lots of motivations for working over that as far as possible:
> baking univalence into material where it’s not really required feels like
> when classical mathematicians make use of AC for no real advantage.
>

I'm in some respects sympathetic to this. We just have to be aware that
working in agnostic type theory leaves us with a burden of
mentally/manually handling the relevant notions of identity because the
identity types cannot be relied upon.

But do you really think they don’t consider FinSet_N to be a category??  I
>> find that very hard to believe: I am pretty sure that most traditional
>> category theorists would consider FinSet_N a category without any doubt at
>> all, which really seems to imply that the standard concept of category is
>> more like “precategory” than “univalent category”.
>>
>
Well, FinSet_N presents FinSet and we often elide the difference between an
object and a presentation for it, but we do so at our own peril.
Traditionally, all categories are presented by a strict category, but
traditional category theorists context-switch easily between strict and
univalent categories (using heuristics about “evil”–there we go with the
preaching again, sorry!).

I'm beginning to despair for ever using the word “category” again without a
modifier. The notion of “precategory” is pretty weird in the standard
model: Why should the notion of an infinity-groupoid with a family of
hom-sets be the sanctified notion?! Of course it turns out to be a useful
notion, just like group presentations are useful. But group theory is about
groups, not group presentations.

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

[-- Attachment #1.2: Type: text/html, Size: 3210 bytes --]

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-07 14:14          Ulrik Buchholtz
2018-11-07 14:27            Peter LeFanu Lumsdaine
@ 2018-11-07 14:31            Thorsten Altenkirch
1 sibling, 0 replies; 46+ messages in thread
From: Thorsten Altenkirch @ 2018-11-07 14:31 UTC (permalink / raw)
To: Ulrik Buchholtz, Homotopy Type Theory

[-- Attachment #1: Type: text/plain, Size: 2948 bytes --]

Strict cats are no good because the first example of a category, the category of sets isn’t one. And we always say homSETS but not sets of objects (ok this is mainly for size but the two are not unrelated).

Btw, there are strict univalent cats but they are quite rare…

Thorsten

From: <homotopytypetheory@googlegroups.com> on behalf of Ulrik Buchholtz <ulrikbuchholtz@gmail.com>
Date: Wednesday, 7 November 2018 at 14:14
Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories

On Wednesday, November 7, 2018 at 2:58:28 PM UTC+1, Thorsten Altenkirch wrote:
As I tried to say, I find that precategory is the novel concept, and that both strict category and univalent category should be familiar to category theorists. (They have a mental model for when one notion is called for or the other, but we can make the distinction formal.)

This is too clever!

If you just transcribe the traditional definition of a category in type theory you end up with what in the HoTT book is called precategory. This is confusing for the non-expert even though you can justify why it should be so.

No, you get the notion of a strict category, which in some sense is all that you directly have in set theory. (To get the (2,1)-category of univalent categories, you take the homotopy (2,1)-category of the folk model structure on the category(?!) of strict categories.)

As I said before, the notion of strict category is useful, and encompasses the examples that Erik was missing from univalent categories.

But from a HoTT/UF point of view, the notion of strict category has the drawback that you cannot get a strict category of sets (or groups or…) without assuming the axiom (a homotopical taboo) that sets cover.
--
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>.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
attachment.

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.

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

[-- Attachment #2: Type: text/html, Size: 7576 bytes --]

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-07 14:28          Ulrik Buchholtz
@ 2018-11-07 15:35            Thomas Streicher
2018-11-07 16:54              Thorsten Altenkirch
From: Thomas Streicher @ 2018-11-07 15:35 UTC (permalink / raw)
To: Ulrik Buchholtz; +Cc: Homotopy Type Theory

What one calls a category should be a set in the HoTT sense,
i.e. validate UIP, but not a set in the sense of size.

Every deviation from that should be signalled by some adjectives or
prefixes. That reflects the practice in category theory.

Thomas

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

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-07 15:35            Thomas Streicher
@ 2018-11-07 16:54              Thorsten Altenkirch
2018-11-07 16:56                Thorsten Altenkirch
2018-11-08 11:58                Thomas Streicher
0 siblings, 2 replies; 46+ messages in thread
From: Thorsten Altenkirch @ 2018-11-07 16:54 UTC (permalink / raw)
To: Thomas Streicher, Ulrik Buchholtz; +Cc: Homotopy Type Theory

Meinst Du dass die Homs sets sind, oder?

Man braucht ja nicht, dass die Objekte ein Set sind. Insbesondere erlaubt iuns das die Kategorie der Sets zu definieren (also beides klein und HSet).

T.

What one calls a category should be a set in the HoTT sense,
i.e. validate UIP, but not a set in the sense of size.

Every deviation from that should be signalled by some adjectives or
prefixes. That reflects the practice in category theory.

Thomas

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

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
attachment.

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.

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

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
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
From: Thorsten Altenkirch @ 2018-11-07 16:56 UTC (permalink / raw)
To: Thomas Streicher, Ulrik Buchholtz; +Cc: Homotopy Type Theory

Sorry, I meant to reply only to Thomas. That explains the language which is not the internal language of some category...

T

﻿On 07/11/2018, 16:55, "homotopytypetheory@googlegroups.com on behalf of Thorsten Altenkirch" <homotopytypetheory@googlegroups.com on behalf of Thorsten.Altenkirch@nottingham.ac.uk> wrote:

Meinst Du dass die Homs sets sind, oder?

Man braucht ja nicht, dass die Objekte ein Set sind. Insbesondere erlaubt iuns das die Kategorie der Sets zu definieren (also beides klein und HSet).

T.

What one calls a category should be a set in the HoTT sense,
i.e. validate UIP, but not a set in the sense of size.

Every deviation from that should be signalled by some adjectives or
prefixes. That reflects the practice in category theory.

Thomas

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

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
attachment.

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.

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

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
attachment.

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.

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

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-07 16:56                Thorsten Altenkirch
@ 2018-11-07 17:31                  Eric Finster
0 siblings, 0 replies; 46+ messages in thread
From: Eric Finster @ 2018-11-07 17:31 UTC (permalink / raw)
To: Thorsten Altenkirch
Cc: Thomas Streicher, Ulrik Buchholtz, Homotopy Type Theory

[-- Attachment #1: Type: text/plain, Size: 3866 bytes --]

I also agree with Mike and Ulrik.

I feel like the example of categories is the perfect opportunity to explain
to
someone who is interested in HoTT *why* there is a version of the
definition
that we prefer, *why* it is different from the notion they may be familiar
with
and *why*, in my humble opinion, it is an improvement.

On Wed, Nov 7, 2018 at 5:56 PM Thorsten Altenkirch <
Thorsten.Altenkirch@nottingham.ac.uk> wrote:

> Sorry, I meant to reply only to Thomas. That explains the language which
> is not the internal language of some category...
>
> T
>
> ﻿On 07/11/2018, 16:55, "homotopytypetheory@googlegroups.com on behalf of
> Thorsten Altenkirch" <homotopytypetheory@googlegroups.com on behalf of
> Thorsten.Altenkirch@nottingham.ac.uk> wrote:
>
>     Meinst Du dass die Homs sets sind, oder?
>
>     Man braucht ja nicht, dass die Objekte ein Set sind. Insbesondere
> erlaubt iuns das die Kategorie der Sets zu definieren (also beides klein
> und HSet).
>
>     T.
>
>     On 07/11/2018, 15:36, "homotopytypetheory@googlegroups.com on behalf
> of Thomas Streicher" <homotopytypetheory@googlegroups.com on behalf of
>
>         What one calls a category should be a set in the HoTT sense,
>         i.e. validate UIP, but not a set in the sense of size.
>
>         Every deviation from that should be signalled by some adjectives or
>         prefixes. That reflects the practice in category theory.
>
>         Thomas
>
>         --
>         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.
>
>
>
>
>
>     This message and any attachment are intended solely for the addressee
>     and may contain confidential information. If you have received this
>     attachment.
>
>     Any views or opinions expressed by the author of this email do not
>     necessarily reflect the views of the University of Nottingham. Email
>     communications with the University of Nottingham may be monitored
>     where permitted by law.
>
>
>
>
>     --
>     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
>     For more options, visit https://groups.google.com/d/optout.
>
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
> --
> 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
> 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.

[-- Attachment #2: Type: text/html, Size: 5567 bytes --]

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-07 14:05        Peter LeFanu Lumsdaine
2018-11-07 14:28          Ulrik Buchholtz
@ 2018-11-07 20:00          Michael Shulman
1 sibling, 0 replies; 46+ messages in thread
From: Michael Shulman @ 2018-11-07 20:00 UTC (permalink / raw)
To: Peter LeFanu Lumsdaine; +Cc: Ulrik Buchholtz, HomotopyTypeTheory

On Wed, Nov 7, 2018 at 6:05 AM Peter LeFanu Lumsdaine
<p.l.lumsdaine@gmail.com> wrote:
>> As I tried to say, I find that precategory is the novel concept, and that both strict category and univalent category should be familiar to category theorists. (They have a mental model for when one notion is called for or the other, but we can make the distinction formal.)
>
> I would argue both are familiar to traditional category theorists.  It’s not unusual to make use of, for instance, the small model for FinSet where the set of objects is taken as N — call this FinSet_N, say.  Category theorists would certainly say that there’s a difference in character between FinSet_N and FinSet itself: FinSet_N is small; and I think they would also agree that they’re conscious informally of an extra character FinSet has, which in HoTT can be precisely expressed as its univalence.
>
> But do you really think they don’t consider FinSet_N to be a category??  I find that very hard to believe: I am pretty sure that most traditional category theorists would consider FinSet_N a category without any doubt at all, which really seems to imply that the standard concept of category is more like “precategory” than “univalent category”.

This is a really interesting question.  Traditional category theorists
do of course consider FinSet_N to be a category; in particular, it
*is* a category according to the definition of "category" in ZFC.

One could view this situation as analogous to that of truncated and
untruncated Sigmas.  When formalizing mathematics in ZFC, there are no
untruncated Sigmas.  When formalizing mathematics in MLTT, there are
no truncated Sigmas.  But when formalizing mathematics in HoTT, we
have both truncated and untruncated Sigmas.  We used to ask the
question "when formalizing mathematics in HoTT, should the quantifier
'there exists' be interpreted as a truncated Sigma or an untruncated
Sigma?"  (This is what led to the somewhat-awkward use of the word
"merely" in the book.)  But more recently a number of us seem to
believe that that's the wrong question, as it presupposes that
mathematics has *already* been interpreted into first-order logic,
which destroys the *natural* distinction between truncated and
untruncated Sigma.  Instead we should directly interpret mathematics
into HoTT, choosing truncated and untruncated Sigmas as appropriate
for the mathematics, without feeling the need to pass through
first-order logic.

Similarly, when formalizing category theory in ZFC, there are no
univalent categories, only strict ones; thus we have to carefully
ignore the strictness when working with categories that "should" be
univalent.  I don't know if there is any foundational theory in which
*all* categories are univalent.  But when formalizing category theory
in HoTT, we have both; and so one might argue that it's wrong to ask
whether the word 'category' should refer to strict categories or
univalent ones, and instead we should use one or the other as
appropriate for the mathematics -- and thus the general word
'category' should refer to something that includes both of them, such
as precategories.

Is that roughly the point you are making, Peter?

I can't deny that there is something to this argument.  However, I
have two objections to it, or at least to its conclusion.  The first
is that the analogy breaks down in the following way.  The awkwardness
of formalizing mathematics in first-order logic comes from
*conflating* truncated and untruncated Sigmas.  Thus, the problem is
solved in HoTT by simply distinguishing them.  However, the
awkwardness of formalizing category theory in ZFC comes not merely
from conflating strict categories with univalent ones, but because
doing category theory with strict categories is *intrinsically*
awkward, whereas most applications of category theory involve only
univalent categories (or more precisely, categories that *should* be
univalent), so that awkwardness shouldn't be necessary.  I think this
is Eric's point: doing category theory with univalent categories is
*nicer* than doing it in ZFC, whereas doing category theory with
strict categories is *no better* than doing it in ZFC.  Why wouldn't
we want to emphasize one of the "selling points" of HoTT in our
terminology?  The strict categories are still there whenever we need
them, but giving them a slightly derogatory red-herring adjective is
appropriate because they are, for the most part, less well-behaved,
and not what the subject of "category theory" is primarily about.

My second objection is to the jump from "something that includes both
strict and univalent categories" to "precategories".  One can argue
that traditional category theorists have a notion of "category" that
includes both strict categories and univalent categories, but I would
argue that their notion does *not* include precategories *other* than
strict and univalent ones; instead it is something more like the
"union" of strict categories and univalent categories, which is much
smaller than the world of precategories.  As evidence, I suggest that
to a traditional category theorist, the statement "a fully faithful
and essentially surjective functor is a (strong) equivalence" is
either "just true", "becomes true if you set up the definitions
correctly", or "becomes true if you assume the axiom of choice"
(depending on the particular category theorist's attitude towards the
axiom of choice).  In HoTT, this statement for univalent categories is
"just true" without any axiom of choice (one way in which doing
category theory with univalent categories is nicer), while this
statement for strict categories is related to the axiom of choice in
exactly the same way as it is in ZFC.  But this statement for general
precategories is *just false*!!  This is easy to see: let Y be any
type, considered as a univalent groupoid, let f : X -> Y be any
surjection of types, and make X into a precategory in the unique way
such that f becomes a fully faithful functor.  Then f is also
essentially surjective, but for it to be an equivalence the surjection
f must have a section; and there are plenty of surjections of types
that have no section, such as the inclusion of the basepoint of S^1.
So precategories are really weird, and if we define the word
"category" to mean "precategory" then category theorists learning
about HoTT will see things like this and react "whoa, category theory
in HoTT is really weird" -- whereas the correct reaction (when using
univalent categories) is "whoa, category theory in HoTT is really
awesome"!

Moreover, as Ulrik pointed out, there is a notion in traditional
(higher) category theory that (under the standard interpretations of
HoTT) does coincide with precategories.  They're called "flagged
categories": https://arxiv.org/abs/1801.08973.  In particular, they
are *not* called just "categories"!  This to me is additional strong
evidence that the traditional category theorist's notion of "category"
does not include precategories.  So if we in HoTT used "category" to
mean "precategory", then we would actually be *renaming* something
way.

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

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
@ 2018-11-07 20:01                Michael Shulman
2018-11-08 21:37                Martín Hötzel Escardó
1 sibling, 0 replies; 46+ messages in thread
From: Michael Shulman @ 2018-11-07 20:01 UTC (permalink / raw)
To: Peter LeFanu Lumsdaine; +Cc: Ulrik Buchholtz, HomotopyTypeTheory

On Wed, Nov 7, 2018 at 7:55 AM Michael Shulman <shulman@sandiego.edu> wrote:
> I doubt there is *any*
> choice of terminology for plain MLTT without UA *or* UIP that is
> sensible in that it can be specialized to the right terminology upon
> the addition of either of these two inconsistent axioms.

Well, with tongue slightly in cheek, here is one such definition: a
category is a precategory C such that (if UA holds then C is
univalent).  (-:

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

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-07 16:54              Thorsten Altenkirch
2018-11-07 16:56                Thorsten Altenkirch
@ 2018-11-08 11:58                Thomas Streicher
2018-11-08 12:23                  [HoTT] " Emily Riehl
 (2 more replies)
1 sibling, 3 replies; 46+ messages in thread
From: Thomas Streicher @ 2018-11-08 11:58 UTC (permalink / raw)
To: Thorsten Altenkirch; +Cc: Ulrik Buchholtz, Homotopy Type Theory

Thorsten asked why I prefer to have strict equality on categories.
The answer is that one needs it in category theory typically when
And the latter is most useful in many contexts in particular when
understanding geometric morphisms. This by the way also extends to
Grothendieck fibrations in quasicategories as in Joyal and Lurie's
accounts.

Thomas

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

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

* Re: [HoTT] Precategories, Categories and Univalent categories
2018-11-08 11:58                Thomas Streicher
@ 2018-11-08 12:23                  " Emily Riehl
2018-11-08 12:28                    Emily Riehl
2018-11-08 16:10                    Thomas Streicher
2018-11-08 14:38                  [HoTT] " Michael Shulman
2018-11-08 16:01                  Thorsten Altenkirch
2 siblings, 2 replies; 46+ messages in thread
From: Emily Riehl @ 2018-11-08 12:23 UTC (permalink / raw)
To: Homotopy Type Theory

There’s a (2-categorical) characterization of fibrations due to Ross Street that I like that works well in the (∞,1)-categorical context. In quasi-categories this captures the class of maps that Joyal/Lurie call “cartesian fibrations” but this definition can be used for other models of (∞,1)-categories as well.

A functor p : E —> B between (∞,1)-categories is a cartesian fibration if the corresponding functor p^2 : E^2 —> B/p admits a right adjoint right inverse (right adjoint whose counit is invertible).

A functor p : E —> B between (∞,1)-categories is a discrete cartesian fibration (aka right fibration) if the corresponding functor p^2 : E^2 —> B/p is an equivalence.

Here E^2 is the (∞,1)-category of arrows in E (the cotensor with the walking arrow category 2) while B/p is a pullback of B^2 along p : E —> B in the codomain variable.

If p : E —> B is an isofibration (in models, this is the notion of fibration in the corresponding model category; eg the Joyal model structure for quasi-categories) then p^2 : E^2 —> B/p is also an isofibration and you can modify the right adjoint right inverse so that the right adjoint is a strict section and the counit is an identity. This can be technically convenient — the adjunction is now a fibered adjunction and can be pulled back more easily — but strict equality doesn’t feel necessary to me in this context.

Best,
Emily

—
Assistant Professor, Dept. of Mathematics
Johns Hopkins University
www.math.jhu.edu/~eriehl

> On Nov 8, 2018, at 6:58 AM, Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote:
>
>
> Thorsten asked why I prefer to have strict equality on categories.
> The answer is that one needs it in category theory typically when
> And the latter is most useful in many contexts in particular when
> understanding geometric morphisms. This by the way also extends to
> Grothendieck fibrations in quasicategories as in Joyal and Lurie's
> accounts.
>
> Thomas
>
>
> --
> 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.

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

* Re: [HoTT] Precategories, Categories and Univalent categories
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
From: Emily Riehl @ 2018-11-08 12:28 UTC (permalink / raw)
To: Homotopy Type Theory

I should have added references. Street’s original papers are here:

“Fibrations and Yoneda’s lemma in a 2-category"

“Fibrations in bicategories"
http://www.numdam.org/article/CTGDC_1980__21_2_111_0.pdf

For a rough draft of the (∞,1)-categorical story, see Chapter 5 of this:
http://www.math.jhu.edu/~eriehl/elements.pdf

Best,
Emily

—
Assistant Professor, Dept. of Mathematics
Johns Hopkins University
www.math.jhu.edu/~eriehl

> On Nov 8, 2018, at 7:23 AM, Emily Riehl <eriehl@math.jhu.edu> wrote:
>
>
> There’s a (2-categorical) characterization of fibrations due to Ross Street that I like that works well in the (∞,1)-categorical context. In quasi-categories this captures the class of maps that Joyal/Lurie call “cartesian fibrations” but this definition can be used for other models of (∞,1)-categories as well.
>
> A functor p : E —> B between (∞,1)-categories is a cartesian fibration if the corresponding functor p^2 : E^2 —> B/p admits a right adjoint right inverse (right adjoint whose counit is invertible).
>
> A functor p : E —> B between (∞,1)-categories is a discrete cartesian fibration (aka right fibration) if the corresponding functor p^2 : E^2 —> B/p is an equivalence.
>
> Here E^2 is the (∞,1)-category of arrows in E (the cotensor with the walking arrow category 2) while B/p is a pullback of B^2 along p : E —> B in the codomain variable.
>
> If p : E —> B is an isofibration (in models, this is the notion of fibration in the corresponding model category; eg the Joyal model structure for quasi-categories) then p^2 : E^2 —> B/p is also an isofibration and you can modify the right adjoint right inverse so that the right adjoint is a strict section and the counit is an identity. This can be technically convenient — the adjunction is now a fibered adjunction and can be pulled back more easily — but strict equality doesn’t feel necessary to me in this context.
>
> Best,
> Emily
>
> —
> Assistant Professor, Dept. of Mathematics
> Johns Hopkins University
> www.math.jhu.edu/~eriehl
>
>> On Nov 8, 2018, at 6:58 AM, Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote:
>>
>>
>> Thorsten asked why I prefer to have strict equality on categories.
>> The answer is that one needs it in category theory typically when
>> And the latter is most useful in many contexts in particular when
>> understanding geometric morphisms. This by the way also extends to
>> Grothendieck fibrations in quasicategories as in Joyal and Lurie's
>> accounts.
>>
>> Thomas
>>
>>
>> --
>> 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.

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

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

* Re: [HoTT] Precategories, Categories and Univalent categories
2018-11-08 12:28                    Emily Riehl
@ 2018-11-08 14:01                      Thomas Streicher
0 siblings, 0 replies; 46+ messages in thread
From: Thomas Streicher @ 2018-11-08 14:01 UTC (permalink / raw)
To: Emily Riehl; +Cc: Homotopy Type Theory

Dear Emily,

thanks for the various references. I was aware of Street's
generalization which is obtained from Grothendieck fibrations by
closing up under categorical equivalences.

But when one works with fibrations P : XX -> BB then it is intrinsic to
have have reindexing functors u^* : P(I) -> P(J) for all u : J -> I in
the base. And these one doesn't have in case of Street fibrations.

For me Grothendieck fibrations are a most useful tool for

1) categorical logic
2) category theory over toposes or even more general base categories
3) conceptual understanding of geometric morphisms and properties of them

and there the stronger notion of Grothendieck is indispensible.

For Street fibrations fibers over isomorphic objects need not be
equivalent anymore. That appears to me as counter intuitive. But,
well, speaking about fibers is evil anyway.

Thomas

PS  (1) Admittedly, in HoTT one needs fibrations less since one has
universes available. If I had to defense the HoTT view I would say
that fibrations are meaningless and they were used by the old category
theorists only because they lacked universes.

(2) In ordinary category theory, at least in topos theory, speaking about
internal categories is very important. I guess that is an eval notion
because it is built on equality of objects. Is there something like an
"internal quasicat"?

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

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-08 11:58                Thomas Streicher
2018-11-08 12:23                  [HoTT] " Emily Riehl
@ 2018-11-08 14:38                  " Michael Shulman
2018-11-08 21:08                    Thomas Streicher
2018-11-08 16:01                  Thorsten Altenkirch
From: Michael Shulman @ 2018-11-08 14:38 UTC (permalink / raw)
To: Thomas Streicher; +Cc: Thorsten Altenkirch, Ulrik Buchholtz, homotopytypetheory

Actually, you don't need strict equality on categories to talk about
strict Grothendieck fibrations in type theory:
https://ncatlab.org/nlab/show/displayed+category
On Thu, Nov 8, 2018 at 3:58 AM Thomas Streicher
>
> Thorsten asked why I prefer to have strict equality on categories.
> The answer is that one needs it in category theory typically when
> And the latter is most useful in many contexts in particular when
> understanding geometric morphisms. This by the way also extends to
> Grothendieck fibrations in quasicategories as in Joyal and Lurie's
> accounts.
>
> Thomas
>
>
> --
> 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.

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-08 11:58                Thomas Streicher
2018-11-08 12:23                  [HoTT] " Emily Riehl
2018-11-08 14:38                  [HoTT] " Michael Shulman
@ 2018-11-08 16:01                  Thorsten Altenkirch
2018-11-08 19:39                    Thorsten Altenkirch
From: Thorsten Altenkirch @ 2018-11-08 16:01 UTC (permalink / raw)
To: Thomas Streicher; +Cc: Ulrik Buchholtz, Homotopy Type Theory

Hi Thomas,

two answers: the first is that in this particular case one doesn't need
strict equality because one can present this as an indexed structure in
type theory, e.g. assume as given a category C then a fibration F is a
structure with the following components (here I assume that the base cat C
is given by objects |C|, morphisms C(_,_) and so on.

|F| : |C| -> U
Fm : C(x,y) -> |F|(x) -> |F|(y) -> U
id_F : Fm id a a
comp_F : Fm f b c -> Fm g a b -> Fm (f o g) a c
coe : C(x,y) -> |F|(y) -> |F|(x)
coh : (p : C(x,y)) -> Fm(p,coe(p,x,a),a)

The 2nd answer is that this is not always possible and the most well known
example are semi-simplicial types. In this case we can produce indexed
structures for all finite approximations but we can't generate the
approximations in a uniform way (the question is actually an open
problem). However, you don't want to force your categories to be struct
but you want to be able to talk about your univalent, non-strict
categories from a strict metatheoretic perspective. This can be realized
by a 2-level type theory as for example explained in our paper [1]
http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf

Cheers,

Thorsten

[1] @InProceedings{altenkirch_et_al:LIPIcs:2016:6561,
author ={Thorsten Altenkirch and Paolo Capriotti and Nicolai Kraus},
title ={{Extending Homotopy Type Theory with Strict Equality}},
booktitle ={25th EACSL Annual Conference on Computer Science Logic (CSL
2016)},
pages ={21:1--21:17},
series ={Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN ={978-3-95977-022-4},
ISSN ={1868-8969},
year ={2016},
volume ={62},
editor ={Jean-Marc Talbot and Laurent Regnier},
publisher ={Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
URL ={http://drops.dagstuhl.de/opus/volltexte/2016/6561},
URN ={urn:nbn:de:0030-drops-65612},
doi ={http://dx.doi.org/10.4230/LIPIcs.CSL.2016.21},
annote ={Keywords: homotopy type theory, coherences, strict equality,
homotopy type system}
}

On 08/11/2018, 11:58, "Thomas Streicher"

>Thorsten asked why I prefer to have strict equality on categories.
>The answer is that one needs it in category theory typically when
>And the latter is most useful in many contexts in particular when
>understanding geometric morphisms. This by the way also extends to
>Grothendieck fibrations in quasicategories as in Joyal and Lurie's
>accounts.
>
>Thomas
>
>

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
attachment.

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.

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

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

* Re: [HoTT] Precategories, Categories and Univalent categories
2018-11-08 12:23                  [HoTT] " Emily Riehl
2018-11-08 12:28                    Emily Riehl
@ 2018-11-08 16:10                    Thomas Streicher
1 sibling, 0 replies; 46+ messages in thread
From: Thomas Streicher @ 2018-11-08 16:10 UTC (permalink / raw)
To: Emily Riehl; +Cc: Homotopy Type Theory

> A functor p : E ???> B between (???,1)-categories is a cartesian fibration if the corresponding functor p^2 : E^2 ???> B/p admits a right adjoint right inverse (right adjoint whose counit is invertible).

That's not the definition on the nLab nor is it the one in Lurie and
also not in Joyal's writings.

Thomas

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

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-08 16:01                  Thorsten Altenkirch
@ 2018-11-08 19:39                    Thorsten Altenkirch
0 siblings, 0 replies; 46+ messages in thread
From: Thorsten Altenkirch @ 2018-11-08 19:39 UTC (permalink / raw)
To: Thorsten Altenkirch, Thomas Streicher
Cc: Ulrik Buchholtz, Homotopy Type Theory

Sorry, I was to quick pressing send. We need the category to have homsets
C : |C| -> |C| -> Set which means that the equations of a category are
propositional. Similar we need to say

Fm : C(x,y) -> |F|(x) -> |F|(y) -> Set

and add fibred id and composition and the laws (again propositional).
Thorsten

On 08/11/2018, 16:01, "homotopytypetheory@googlegroups.com on behalf of
Thorsten Altenkirch" <homotopytypetheory@googlegroups.com on behalf of
Thorsten.Altenkirch@nottingham.ac.uk> wrote:

>Hi Thomas,
>
>two answers: the first is that in this particular case one doesn't need
>strict equality because one can present this as an indexed structure in
>type theory, e.g. assume as given a category C then a fibration F is a
>structure with the following components (here I assume that the base cat C
>is given by objects |C|, morphisms C(_,_) and so on.
>
>|F| : |C| -> U
>Fm : C(x,y) -> |F|(x) -> |F|(y) -> U
>id_F : Fm id a a
>comp_F : Fm f b c -> Fm g a b -> Fm (f o g) a c
>coe : C(x,y) -> |F|(y) -> |F|(x)
>coh : (p : C(x,y)) -> Fm(p,coe(p,x,a),a)
>
>The 2nd answer is that this is not always possible and the most well known
>example are semi-simplicial types. In this case we can produce indexed
>structures for all finite approximations but we can't generate the
>approximations in a uniform way (the question is actually an open
>problem). However, you don't want to force your categories to be struct
>but you want to be able to talk about your univalent, non-strict
>categories from a strict metatheoretic perspective. This can be realized
>by a 2-level type theory as for example explained in our paper [1]
>http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf
>
>Cheers,
>
>Thorsten
>
>[1] @InProceedings{altenkirch_et_al:LIPIcs:2016:6561,
>author ={Thorsten Altenkirch and Paolo Capriotti and Nicolai Kraus},
>title ={{Extending Homotopy Type Theory with Strict Equality}},
>booktitle ={25th EACSL Annual Conference on Computer Science Logic (CSL
>2016)},
>pages ={21:1--21:17},
>series ={Leibniz International Proceedings in Informatics (LIPIcs)},
>ISBN ={978-3-95977-022-4},
>ISSN ={1868-8969},
>year ={2016},
>volume ={62},
>editor ={Jean-Marc Talbot and Laurent Regnier},
>publisher ={Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
>URL ={http://drops.dagstuhl.de/opus/volltexte/2016/6561},
>URN ={urn:nbn:de:0030-drops-65612},
>doi ={http://dx.doi.org/10.4230/LIPIcs.CSL.2016.21},
>annote ={Keywords: homotopy type theory, coherences, strict equality,
>homotopy type system}
>}
>
>
>
>
>
>On 08/11/2018, 11:58, "Thomas Streicher"
>
>>Thorsten asked why I prefer to have strict equality on categories.
>>The answer is that one needs it in category theory typically when
>>And the latter is most useful in many contexts in particular when
>>understanding geometric morphisms. This by the way also extends to
>>Grothendieck fibrations in quasicategories as in Joyal and Lurie's
>>accounts.
>>
>>Thomas
>>
>>
>
>
>
>
>This message and any attachment are intended solely for the addressee
>and may contain confidential information. If you have received this
>attachment.
>
>Any views or opinions expressed by the author of this email do not
>necessarily reflect the views of the University of Nottingham. Email
>communications with the University of Nottingham may be monitored
>where permitted by law.
>
>
>
>
>--
>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

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
attachment.

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.

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

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-08 14:38                  [HoTT] " Michael Shulman
@ 2018-11-08 21:08                    Thomas Streicher
2018-11-08 21:30                      Michael Shulman
From: Thomas Streicher @ 2018-11-08 21:08 UTC (permalink / raw)
To: Michael Shulman; +Cc: Thorsten Altenkirch, Ulrik Buchholtz, homotopytypetheory

> Actually, you don't need strict equality on categories to talk about
> strict Grothendieck fibrations in type theory:
> https://ncatlab.org/nlab/show/displayed+category

This is indexed and not fibered (see my MR review of this paper).

Thomas

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

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-08 21:08                    Thomas Streicher
@ 2018-11-08 21:30                      Michael Shulman
2018-11-09 11:56                        Thomas Streicher
From: Michael Shulman @ 2018-11-08 21:30 UTC (permalink / raw)
To: Thomas Streicher; +Cc: Thorsten Altenkirch, Ulrik Buchholtz, homotopytypetheory

It may be "indexed" in the sense that it involves maps into a
universe, but it is not an "indexed category" as the term is usually
used, since the latter is a pseudofunctor into Cat rather than a lax
functor into Span.  In particular, a displayed category can be a
fibration, an opfibration, both, or neither, while an indexed category
always corresponds to at least a fibration.  A displayed category is a
refinement of a functor in the same way that a dependent type is a
refinement of a function: you can always recover the total category by
taking Sigma-types, and thereby formulate all of the theorems
as a displayed category is that it solves precisely the problem at
issue, giving a way of talking about two objects being "in the same
(strict) fiber" without invoking equality of objects in the base
category.

Requiring the type of objects of a category to be an h-set does also
recover the ability to talk about strict fibers, but the resulting
theory of "Grothendieck fibrations" would be pretty useless for HoTT,
since almost no naturally-occurring categories have this property or
can even be replaced by equivalent categories that have this property.
If we want a theory of categories that includes important things like
the category of sets, and toposes and geometric morphisms constructed
from it, we cannot require all categories to have h-sets of objects
(i.e. to be "strict categories").  Thus, to talk about fibrations, we
have to either use something like displayed categories, or a weaker
notion of fibration such as mentioned by Emily (in which case one
simply talks about "essential fibers" rather than strict fibers, and
these do have reindexing functors and all the other behavior one would
expect).

On Thu, Nov 8, 2018 at 1:08 PM Thomas Streicher
>
> > Actually, you don't need strict equality on categories to talk about
> > strict Grothendieck fibrations in type theory:
> > https://ncatlab.org/nlab/show/displayed+category
>
> This is indexed and not fibered (see my MR review of this paper).
>
> Thomas
>
> --
> 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.

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

* [HoTT] Re: Precategories, Categories and Univalent categories
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-08 21:35  Martín Hötzel Escardó
2 siblings, 0 replies; 46+ messages in thread
From: Martín Hötzel Escardó @ 2018-11-08 21:35 UTC (permalink / raw)
To: Homotopy Type Theory

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

On Wednesday, 7 November 2018 10:03:17 UTC, Ali Caglayan wrote:
>
> 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.

[-- Attachment #1.2: Type: text/html, Size: 1615 bytes --]

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-07 20:01                Michael Shulman
@ 2018-11-08 21:37                Martín Hötzel Escardó
2018-11-08 21:43                  Michael Shulman
From: Martín Hötzel Escardó @ 2018-11-08 21:37 UTC (permalink / raw)
To: Homotopy Type Theory

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

We have two separate issues here:

(1) What is the appropriate notion of category for univalent
mathematics.

(2) What is the right terminology for it.

There is also a separate, orthogonal question,

(3) Whether there is a foundation-independent (dubbed "agnostic")
notion of category, which gives the right notion for each
foundation, *and* can be formulated in MLTT (without K or
univalence).

Regarding (3), even if this is possible (assuming the question
makes sense), it is not given by any of the proposed notions, and
this should not be regarded as surprising or shocking.

(This raises the question of whether there is a categorical
definition of category, for people who would like to see category
theory itself as a foundation.)

Regarding (1), I think the arguments by Ulrik, Paolo, Mike and
Eric (Finster) are pretty convincing: "univalent category" is the
right notion of category for univalent mathematics.

However, it *is* common and useful in mathematics to formulate
and prove theorems with minimal hypotheses, and then what is
called a pre-category, and what Thorsten called a wild category,
often arise naturally and unavoidably as part of the building
blocks of mathematics.

Regarding (2), I would say, in view of (the answer to) (3), that
it is probably better to avoid the naked terminology "category"
in HoTT/UF, as it would give the wrong impression of *capturing*
a universal, pre-existing, foundation-independent notion of
category (in particular compatible with the ZFC view of what a
category is, which has evilness as a built-in feature):

* Then "univalent category" could mean, ambiguously but
consistently, both

(a) a pre-category that satisfies a certain technical
condition analogous to the univalence axiom for
types, or

(b) "the appropriate notion of category for univalent
mathematics".

(c) In both cases, (a) and (b), the
adjective "univalent" makes sense. In (b), it
would be not in opposition to "category", but
instead in opposition to e.g. "ZFC category".

Martin

On Wednesday, 7 November 2018 15:55:45 UTC, Michael Shulman wrote:
>
> I strongly agree with Ulrik.  Perhaps the point that's not getting
> across is that we are not talking about terminology for MLTT in
> general, but specifically for HoTT (with univalence).  The terminology
> to be decided on doesn't have to make sense or come out to anything
> meaningful in type theory with UIP, and we shouldn't expect it to.
> The terminology in MLTT+UIP should be different from that for MLTT+UA,
> because they are different theories and relate to "traditional"
> mathematics in different *incompatible* ways.  I doubt there is *any*
> choice of terminology for plain MLTT without UA *or* UIP that is
> sensible in that it can be specialized to the right terminology upon
> the addition of either of these two inconsistent axioms.
> On Wed, Nov 7, 2018 at 6:27 AM Peter LeFanu Lumsdaine
> <p.l.lu...@gmail.com <javascript:>> wrote:
> >
> > On Wed, Nov 7, 2018 at 3:14 PM Ulrik Buchholtz <ulrikbu...@gmail.com
> <javascript:>> wrote:
> >>
> >> On Wednesday, November 7, 2018 at 2:58:28 PM UTC+1, Thorsten Altenkirch
> wrote:
> >>>
> >>> As I tried to say, I find that precategory is the novel concept, and
> that both strict category and univalent category should be familiar to
> category theorists. (They have a mental model for when one notion is called
> for or the other, but we can make the distinction formal.)
> >>>
> >>>
> >>> This is too clever!
> >>>
> >>>
> >>>
> >>> If you just transcribe the traditional definition of a category in
> type theory you end up with what in the HoTT book is called precategory.
> This is confusing for the non-expert even though you can justify why it
> should be so.
> >>
> >>
> >> No, you get the notion of a strict category, which in some sense is all
> that you directly have in set theory.
> >
> >
> > No in turn: you can arguably get either strict categories, or
> precategories, or what Thorsten dubbed “wild categories” above, since “set”
> in set theory is the (naïve) interpretation of both “set” and “type”.
>  (Just as when you transcribe classical definitions in a constructive
> setting, you sometimes want to read “predicate” just as “predicate” and
> other times as “decidable predicate” — all predicates are decidable
> classically, but that doesn’t mean that their constructive transcription
> should include “decidable” by default.)
> >
> > –p.
> >
> > --
> > 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 <javascript:>.
>
> > 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.

[-- Attachment #1.2: Type: text/html, Size: 7439 bytes --]

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-08 21:37                Martín Hötzel Escardó
@ 2018-11-08 21:43                  Michael Shulman
2018-11-09  4:43                    Andrew Polonsky
From: Michael Shulman @ 2018-11-08 21:43 UTC (permalink / raw)
To: Martin Hotzel Escardo; +Cc: HomotopyTypeTheory

If one wants a name for "pre-category" that sounds less derogatory,
one could say "flagged category".  Talking about "flagged categories",
"strict categories", and "univalent categories" will always be
unambiguous, and individual papers could declare that plain "category"
will locally mean one or another as desired.
On Thu, Nov 8, 2018 at 1:37 PM Martín Hötzel Escardó
<escardo.martin@gmail.com> wrote:
>
> We have two separate issues here:
>
> (1) What is the appropriate notion of category for univalent
> mathematics.
>
> (2) What is the right terminology for it.
>
> There is also a separate, orthogonal question,
>
> (3) Whether there is a foundation-independent (dubbed "agnostic")
> notion of category, which gives the right notion for each
> foundation, *and* can be formulated in MLTT (without K or
> univalence).
>
> Regarding (3), even if this is possible (assuming the question
> makes sense), it is not given by any of the proposed notions, and
> this should not be regarded as surprising or shocking.
>
> (This raises the question of whether there is a categorical
> definition of category, for people who would like to see category
> theory itself as a foundation.)
>
> Regarding (1), I think the arguments by Ulrik, Paolo, Mike and
> Eric (Finster) are pretty convincing: "univalent category" is the
> right notion of category for univalent mathematics.
>
> However, it *is* common and useful in mathematics to formulate
> and prove theorems with minimal hypotheses, and then what is
> called a pre-category, and what Thorsten called a wild category,
> often arise naturally and unavoidably as part of the building
> blocks of mathematics.
>
> Regarding (2), I would say, in view of (the answer to) (3), that
> it is probably better to avoid the naked terminology "category"
> in HoTT/UF, as it would give the wrong impression of *capturing*
> a universal, pre-existing, foundation-independent notion of
> category (in particular compatible with the ZFC view of what a
> category is, which has evilness as a built-in feature):
>
>      * Then "univalent category" could mean, ambiguously but
>        consistently, both
>
>             (a) a pre-category that satisfies a certain technical
>                 condition analogous to the univalence axiom for
>                 types, or
>
>             (b) "the appropriate notion of category for univalent
>                  mathematics".
>
>             (c) In both cases, (a) and (b), the
>                 adjective "univalent" makes sense. In (b), it
>                 would be not in opposition to "category", but
>                 instead in opposition to e.g. "ZFC category".
>
> Martin
>
>
> On Wednesday, 7 November 2018 15:55:45 UTC, Michael Shulman wrote:
>>
>> I strongly agree with Ulrik.  Perhaps the point that's not getting
>> across is that we are not talking about terminology for MLTT in
>> general, but specifically for HoTT (with univalence).  The terminology
>> to be decided on doesn't have to make sense or come out to anything
>> meaningful in type theory with UIP, and we shouldn't expect it to.
>> The terminology in MLTT+UIP should be different from that for MLTT+UA,
>> because they are different theories and relate to "traditional"
>> mathematics in different *incompatible* ways.  I doubt there is *any*
>> choice of terminology for plain MLTT without UA *or* UIP that is
>> sensible in that it can be specialized to the right terminology upon
>> the addition of either of these two inconsistent axioms.
>> On Wed, Nov 7, 2018 at 6:27 AM Peter LeFanu Lumsdaine
>> <p.l.lu...@gmail.com> wrote:
>> >
>> > On Wed, Nov 7, 2018 at 3:14 PM Ulrik Buchholtz <ulrikbu...@gmail.com> wrote:
>> >>
>> >> On Wednesday, November 7, 2018 at 2:58:28 PM UTC+1, Thorsten Altenkirch wrote:
>> >>>
>> >>> As I tried to say, I find that precategory is the novel concept, and that both strict category and univalent category should be familiar to category theorists. (They have a mental model for when one notion is called for or the other, but we can make the distinction formal.)
>> >>>
>> >>>
>> >>> This is too clever!
>> >>>
>> >>>
>> >>>
>> >>> If you just transcribe the traditional definition of a category in type theory you end up with what in the HoTT book is called precategory. This is confusing for the non-expert even though you can justify why it should be so.
>> >>
>> >>
>> >> No, you get the notion of a strict category, which in some sense is all that you directly have in set theory.
>> >
>> >
>> > No in turn: you can arguably get either strict categories, or precategories, or what Thorsten dubbed “wild categories” above, since “set” in set theory is the (naïve) interpretation of both “set” and “type”.  (Just as when you transcribe classical definitions in a constructive setting, you sometimes want to read “predicate” just as “predicate” and other times as “decidable predicate” — all predicates are decidable classically, but that doesn’t mean that their constructive transcription should include “decidable” by default.)
>> >
>> > –p.
>> >
>> > --
>> > 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.

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

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-08 21:43                  Michael Shulman
@ 2018-11-09  4:43                    Andrew Polonsky
2018-11-09 10:18                      Ulrik Buchholtz
From: Andrew Polonsky @ 2018-11-09  4:43 UTC (permalink / raw)
To: Homotopy Type Theory

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

The intuitive notion of a category is given by the dependently-sorted
algebraic theory of categories.

In the ZFC metatheory, a standard model of this theory yields the usual
mathematical concept of a category.

In the MLTT metatheory, a standard model of this theory yields the concept
of a precategory.

The subtle issue is how to treat the equality predicate, appearing in the
identity and associativity axioms.

In set theory, equality is a former of atomic formulae, which are a
different syntactic category than sets (which interpret the types/domains
of the given language).

In type theory, equality is interpreted as any other type, in accordance
with "the formulae-as-types notion of construction".

However, more modern type theories, like HoTT or CubicalTT, have a
different, "native" conception of equality, so the "natural" notion of
category in these theories will accordingly be different as well.

One day, there might be a metatheory which is generally accepted as
providing a superior "natural" notion of a category, that avoids the
awkward points of the set-theoretic one.

Until then, it is best to be precise with language, always being explicit
which specific concept is meant.

Cheers,
Andrew

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

[-- Attachment #1.2: Type: text/html, Size: 1990 bytes --]

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-09  4:43                    Andrew Polonsky
@ 2018-11-09 10:18                      Ulrik Buchholtz
2018-11-09 10:57                        Paolo Capriotti
From: Ulrik Buchholtz @ 2018-11-09 10:18 UTC (permalink / raw)
To: Homotopy Type Theory

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

On Friday, November 9, 2018 at 5:43:15 AM UTC+1, Andrew Polonsky wrote:
>
> The intuitive notion of a category is given by the dependently-sorted
> algebraic theory of categories.
>

Maybe for you! But not for me: I don't even know what a dependently-sorted
algebraic theory is, where and how such a thing has models, nor what the
particular theory you're thinking of is.

But that reminds me of a MATHEMATICAL question. Consider the well-known
essentially algebraic theory T whose models in Set are strict categories.
What are the models of T in infinity-groupoids? (Or in an arbitrary
(infinity,1)-topos?)

> However, more modern type theories, like HoTT or CubicalTT, have a
> different, "native" conception of equality, so the "natural" notion of
> category in these theories will accordingly be different as well.
>

In cubical type theories, the two notions of equality (path types and the
inductive Id-family) are equivalent, so they give equivalent notions
wherever they are used.

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

[-- Attachment #1.2: Type: text/html, Size: 1896 bytes --]

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-09 10:18                      Ulrik Buchholtz
@ 2018-11-09 10:57                        Paolo Capriotti
0 siblings, 0 replies; 46+ messages in thread
From: Paolo Capriotti @ 2018-11-09 10:57 UTC (permalink / raw)
To: Homotopy Type Theory

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

On Fri, 9 Nov 2018, at 10:18 AM, Ulrik Buchholtz wrote:
> On Friday, November 9, 2018 at 5:43:15 AM UTC+1, Andrew Polonsky wrote:
> >
> > The intuitive notion of a category is given by the dependently-sorted
> > algebraic theory of categories.
> >
>
> Maybe for you! But not for me: I don't even know what a dependently-sorted
> algebraic theory is, where and how such a thing has models, nor what the
> particular theory you're thinking of is.

Let's say we define a *dependently-sorted algebraic theory* to just be a
CwF. A model for it is a CwF-morphism into Set (or more generally into a
CwF). The theory of categories would then be the opposite of Cat_{fp} (I
mean finitely presentable, *not* locally finitely presentable), or
alternatively you can define it inductively as the syntax of a type theory
(but then you have to prove an initiality theorem!).

I'm not sure how this kind of presentation translates to ∞-categories
though.

> But that reminds me of a MATHEMATICAL question. Consider the well-known
> essentially algebraic theory T whose models in Set are strict categories.
> What are the models of T in infinity-groupoids? (Or in an arbitrary
> (infinity,1)-topos?)

Nice question!

I guess by model here you mean a left exact ∞-functor T → Space, where T is
regarded as an ordinary category with finite limits. I think such models
are equivalent to Segal spaces, but without completeness. Or at least, I
don't see where completeness would come from.

I find it quite an illuminating way to look at Segal spaces, by the way.
You get the space of n-simplices by mapping the iterated pullback of the
object of arrows in T (i.e. the object that stands for sequences of
composable arrows). The Segal condition is the preservation of that
pullback. It's essentially the same idea as in the definition of Γ-Spaces.

Best,
Paolo

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

[-- Attachment #1.2: Type: text/html, Size: 2766 bytes --]

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-08 21:30                      Michael Shulman
@ 2018-11-09 11:56                        Thomas Streicher
2018-11-09 13:46                          Michael Shulman
From: Thomas Streicher @ 2018-11-09 11:56 UTC (permalink / raw)
To: Michael Shulman; +Cc: Thorsten Altenkirch, Ulrik Buchholtz, homotopytypetheory

Benedikt and Peter essentially employ an old result of Benabou saying that
functors to BB correspond normalized lax functor from BB^op to Dist,
the bicategory of distributors. But, obviously, the forward direction requires
equality of objects.
Accordingly, they can't express composition of functors in terms of
the associated normalized lax functors.

Even classically, going from fibrations to indexed categories involves
choice. But going from functors to normalized lax functors just
requires equality of objects.

Thomas

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

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-09 11:56                        Thomas Streicher
@ 2018-11-09 13:46                          Michael Shulman
2018-11-09 15:06                            Thomas Streicher
From: Michael Shulman @ 2018-11-09 13:46 UTC (permalink / raw)
To: Thomas Streicher; +Cc: Thorsten Altenkirch, Ulrik Buchholtz, homotopytypetheory

Right, the *forward* direction requires either equality of objects or
using "essential fibers" instead of fibers.  That's what I meant by
saying a displayed category is a "refinement" of a functor: you can
make a functor from a displayed category, but the opposite direction
is harder.  That doesn't mean that you can't express composition of
functors in terms of displayed categories: it just means you can't (or
shouldn't) do it in the naive way by first making your displayed
categories into functors, composing them, and then going back to a
displayed category.  Instead you just have to "lift" functor
composition to displayed categories in the same way that we lift
function composition to Sigma-types.

Suppose D is a displayed category over C, with types of objects obD(x)
: Type and types of morphisms D(f) : D(x) -> D(y) -> Type for x:ob(C)
and f:hom_C(x,y).  Then we can form a total category Sigma(C)D whose
type of objects is Sigma(x:ob(C)) obD(x) and whose types of morphisms
are similar Sigma-types.  Now suppose we have a further displayed
category E over Sigma(C)D.  Then applying associativity of
Sigma-types, we can construct a displayed category Sigma(D)E over C,
with type of objects ob(Sigma(D)E)(x) = Sigma(y:obD(x))obE(x,y) and so
on, whose total category is equivalent (indeed, definitionally
isomorphic, if Sigma-types have definitional beta and eta) to
Sigma(Sigma(C)D)E such that its projection functor corresponds to the
composite of the two functors.
On Fri, Nov 9, 2018 at 3:56 AM Thomas Streicher
>
> Benedikt and Peter essentially employ an old result of Benabou saying that
> functors to BB correspond normalized lax functor from BB^op to Dist,
> the bicategory of distributors. But, obviously, the forward direction requires
> equality of objects.
> Accordingly, they can't express composition of functors in terms of
> the associated normalized lax functors.
>
> Even classically, going from fibrations to indexed categories involves
> choice. But going from functors to normalized lax functors just
> requires equality of objects.
>
> Thomas
>
> --
> 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.

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

* Re: [HoTT] Re: Precategories, Categories and Univalent categories
2018-11-09 13:46                          Michael Shulman
@ 2018-11-09 15:06                            Thomas Streicher
0 siblings, 0 replies; 46+ messages in thread
From: Thomas Streicher @ 2018-11-09 15:06 UTC (permalink / raw)
To: Michael Shulman; +Cc: Thorsten Altenkirch, Ulrik Buchholtz, homotopytypetheory

Didn't deny that it's possible in principle for this very simple case.
But something trivial gets unnaturally complicated when changing foundations.
That's already showing that the new foundation is not superior in all
aspects but actually much worse in particular cases.

This is not unexpected anway that different formalisms have different
advantages and drawbacks. The interesting thing would be to find out
what is easier and what is more cumbersome in which framework.

As I said in a previous mail. Traditional approaches didn't have
universes and fibrations were partly invented to overcome this
shortcoming at the price of having to externalize reasoning.

But there is also extensional type theory with universes. Maybe that's
better than the other 2 approaches.

But one cannot say beforehand which setting is better for what.

What experience tells us is that different setting are good/bad for
different purposes.

That's the point I wanted to make. From my side no need for further
discussion...

Thomas

> Right, the *forward* direction requires either equality of objects or
> using "essential fibers" instead of fibers.  That's what I meant by
> saying a displayed category is a "refinement" of a functor: you can
> make a functor from a displayed category, but the opposite direction
> is harder.  That doesn't mean that you can't express composition of
> functors in terms of displayed categories: it just means you can't (or
> shouldn't) do it in the naive way by first making your displayed
> categories into functors, composing them, and then going back to a
> displayed category.  Instead you just have to "lift" functor
> composition to displayed categories in the same way that we lift
> function composition to Sigma-types.
>
> Suppose D is a displayed category over C, with types of objects obD(x)
> : Type and types of morphisms D(f) : D(x) -> D(y) -> Type for x:ob(C)
> and f:hom_C(x,y).  Then we can form a total category Sigma(C)D whose
> type of objects is Sigma(x:ob(C)) obD(x) and whose types of morphisms
> are similar Sigma-types.  Now suppose we have a further displayed
> category E over Sigma(C)D.  Then applying associativity of
> Sigma-types, we can construct a displayed category Sigma(D)E over C,
> with type of objects ob(Sigma(D)E)(x) = Sigma(y:obD(x))obE(x,y) and so
> on, whose total category is equivalent (indeed, definitionally
> isomorphic, if Sigma-types have definitional beta and eta) to
> Sigma(Sigma(C)D)E such that its projection functor corresponds to the
> composite of the two functors.
> On Fri, Nov 9, 2018 at 3:56 AM Thomas Streicher

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

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

end of thread, back to index

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


Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Newsgroup available over NNTP:
nntp://inbox.vuxu.org/vuxu.archive.hott

AGPL code for this site: git clone https://public-inbox.org/ public-inbox`