By the way, if you know LaTeX, then you can use that in comments. Just be sure to select the filter Markdown+Itex (below the comment box) before adding your comment.

]]>I think they’re fixed now – thanks for bringing this to attention.

]]>Mor(y,z) f o sub(x,y,z) id(x) =f and id(z) o sub(x,y,z) f=f

One more correction? ]]>

First time suggester, long time reader.

I learned many maths in school. including complex calculus, but no category theory, so forgive my misunderstandings.

I believe there are errors on lines of identity-on-objects functor:

for each object x:Ob and y:Ob and morphism f:

Mor(x,y) f o sub(x,y,z) id(x) =f and id(y) o sub(x,y,z) f=f

Shouldn't it read ?

for each object x:Ob and y:Ob and morphism f:

Mor(y,z) f o sub(x,y,z) id(x) =f and id(z) o sub(x,y,z) f=f

I placed location dots and went through the compositions because I'm not sure I understand, but as written there are discontinuities from source to destination with it as written. ]]>

second source doesn’t actually ever talk about identity-on-objects functors.

Anonymous

]]>first source has no relevance to this article anymore since the relevant material was moved to equivalent-on-objects functor

Anonymous

]]>copied some relevant information from categories with the same collection of objects

Anonymous

]]>I rewrote the initial few paragraphs on the definitions to take into account Mike Shulman’s comment. Also definition 1.2 was missing the fact that the functions $F(x,y):A(x, y) \to B(x, y)$ of the “identity-on-object functor” should preserve composition of morphisms and the identity morphism, so I added those in

Anonymous

]]>If the intent of definition 1.1 is to be interpreted in univalent type theory where “$F_{\mathrm{ob}}$ is the identity” means $\prod_{x:\mathrm{Ob}} {\mathrm{ Id}}(F_{\mathrm{ ob}}(x),x)$, then I suppose you can say that this doesn’t violate the principle of equivalence, but it’s also not a correct definition of “identity on objects functor”, because it’s not equivalent to definition 1.2 in that context. I think Definition 1.2 is the only correct definition, in any foundations, that satisfies the principle of equivalence.

]]>Can whichever Anomymous who started this thread edit their first comment to include a link to

where this page was created and includes a lot of discussion?

EDIT: or is it probable that Anonymous/Guests posting in these threads are unable to edit their comments and a Lab Elf needs to do the edit?

If so this is another reason for Guests to pick some pseudonym to use when posting.

]]>examples moved to equivalent-on-objects functor

Anonymous

]]>Conjecture: In type theory, identity-on-objects dagger functors, which are a particular kind of identity-on-objects functor between dagger categories which additionally preserve the dagger structure of the dagger categories, between univalent dagger categories in a univalent universe are equivalent to dagger equivalences of univalent dagger categories.

]]>adding explanation of the relation between identity-on-object functors, bijective-on-object functors, equivalent-on-object functors, and essentially surjective functors, strict categories, univalent categories, and univalent universes in type theory

Anonymous

]]>If we say that definition 1.2 is only a bijective-on-objects functor and not an identity-on-objects functor, then we could create another article equivalent-on-objects functor for definitions 1.3 and 1.4, and say that an isomorphism of categories as defined in the HoTT book is a fully faithful equivalent-on-objects functor.

]]>So, do we restrict the definition of identity-on-objects functor to definition 1.1, and say that structural set theories like ETCS and SEAR cannot define identity-on-objects functors, only bijective-on-objects functor?

]]>cross linked with bijective-on-objects functor

Anonymous

]]>I started this page back in 2017 because I was confused by the newly created page Freyd category.

There is a bunch of discussion at: nForum: freyd-category

]]>the equivalence of categories is specifically adjoint equivalence

Anonymous

]]>adding source for definition of isomorphism of categories

Anonymous

]]>fixing example: every isomorphism of categories is a fully faithful identity-on-objects functors. Equivalences of categories are only identity-on-objects functors if the two categories are univalent.

Anonymous

]]>maxsnew wrote:

Is this an edit war between two anonymous ppl?

Probably not, but I second the sentiment: The edit history makes a confusing impression. Anonymous, would you mind choosing a distinguishable pseudonym? You’ll still remain operationally as anonymous as before (if this is really so important??) but we have a better chance to interact with you.

I really think we should emphasize what’s written in the “On the other hand,” paragraph.

That seems like a very good point. Unfortunately, just this paragraph was deleted in rev 11.

]]>The article states

However, both these definitions still nevertheless violate the principle of equivalence, for the same reason that the translation of the usual definition of a Grothendieck fibration or strict creation of limits into type theory violates the principle of equivalence

How does definition 1.3 violate the principle of equivalence? Unlike the case for Grothendieck fibrations, it doesn’t talk about equality of objects at all.

Unless I suppose one wants to require the correct notion of equality of objects in categories to explicitly be the isomorphisms of the core groupoid of the categories, in which case then categories still violate the principle of equivalence and one really needs univalent categories in the definitions.

]]>Is this an edit war between two anonymous ppl?

]]>reverting the rename: one uses displayed categories instead of identity-on-objects functors if one is concerned about violating the principle of equivalence.

Anonymous

]]>