# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeJun 1st 2017

somebody created Freyd category

• CommentRowNumber2.
• CommentAuthorRodMcGuire
• CommentTimeJun 1st 2017
• (edited Jun 1st 2017)

The definition given is:

• a small category $\mathbb{V}$ with finite products;
• a small category $\mathbb{C}$;
• an action of $\mathbb{V}$ on $\mathbb{C}$ (with the finite products providing a symmetric monoidal structure for $\mathbb{V}$)
• an identity-on-objects functor $\mathbb{V} \to \mathbb{C}$ that preserves the actions.

What does “an identity-on-objects functor” mean? I’ve come across this phase several times but I can’t google up a definition.

In the Stanton paper reference I linked the doi, giving

In that paper Stanton says:

A Freyd category comprises two categories with the same objects: one V, whose morphisms denote pure, value judgements, and one C, whose morphisms denote judgements of computations, together with an identity-on-objects functor J : V → C.

Was that $\mathbb{V}$ and $\mathbb{C}$ have the same objects left out of the definition, is that some how a consequence, or is a more restricted definition?

EDIT: Levy’s book, Call-By-Push-Value: A Functional/Imperative Synthesis, is readable (somewhat) as a Google Book. There is given:

Definition B.10 Let C be a cartesian category and K a category such that ob K = ob C - we write a morphism in K as $f: A \to B$. A Freyd category from C to K consists of

• an identity-on-objects functor i from C to K
• a left C-action on K, extending (along i) the canonical left C-action on C.
• CommentRowNumber3.
• CommentAuthorMike Shulman
• CommentTimeJun 1st 2017

An identity-on-objects functor $V\to C$ is a functor whose underlying function $ob(V) \to ob(C)$ is an identity function. In particular, this implies that $ob(V) = ob(C)$ as sets.

• CommentRowNumber4.
• CommentAuthorRodMcGuire
• CommentTimeJun 1st 2017

An identity-on-objects functor $V\to C$ is a functor whose underlying function $ob(V) \to ob(C)$ is an identity function. In particular, this implies that $ob(V) = ob(C)$ as sets.

That definition seems rather nonsensical. How can one have an identity function between two different sets?

Were I to create a nLab page identity-on-objects functor would the below be a better definition?

An identity-on-objects functor $V\to C$ is between two categories with its underlying object function $ob(V) \to ob(C)$ a bijection. One can regard the categories as having as having the same set of objects, $ob(V) = ob(C)$, which makes the object function the identity.

• CommentRowNumber5.
• CommentAuthorMike Shulman
• CommentTimeJun 1st 2017

How can one have an identity function between two different sets?

Well, as given to us, they’re not known to be the same set, but asserting that some given function between them is an identity function entails in particular that they are the same set, since identity functions have equal domain and codomain.

Of course this only makes sense in an “evil” context where we can talk about equality of sets as a proposition to be proven. Otherwise one should either talk about the function on objects being a bijection — or, better, talk about categories enriched in $Set^{\to}$, as with M-categories. But I would object to defining “identity on objects functor” to mean a bijection on objects, since that’s manifestly not what the words mean.

• CommentRowNumber6.
• CommentAuthorRichard Williamson
• CommentTimeJun 1st 2017
• (edited Jun 1st 2017)

I would say the main point of the definition is that even if $\mathbb{V}$ and $\mathbb{C}$ have the same set of objects, there is no need for a functor between them to be the identity function between the object sets: we are requiring that it does have this property.

I do have some sympathy for Rod’s point, though: I myself would probably state explicitly at the outset that $\mathbb{V}$ and $\mathbb{C}$ have the same set of objects, rather than leaving it implicit. I.e. I would define an identity on objects functor only between categories whose object sets are the same.

• CommentRowNumber7.
• CommentAuthorMike Shulman
• CommentTimeJun 1st 2017

Of course.

1. (My first paragraph was intended for Rod in case it helped clarify :-))

• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeJun 2nd 2017
• (edited Jun 2nd 2017)

Just as a reminder: The person who created the entry (some Bram Geron according to the signature of rev1) is clearly not hanging around here. So it’s probably futile to lament deficiencies of his note here. You should just open the entry and edit it accordingly.

• CommentRowNumber10.
• CommentAuthorRodMcGuire
• CommentTimeJun 2nd 2017
• (edited Jun 2nd 2017)

Urs

Just as a reminder: The person who created the entry (some Bram Geron according to the signature of rev1) is clearly not hanging around here. So it’s probably futile to lament deficiencies of his note here.

Bram Geron has been here since July 2015 and has done minor edits to around 12 pages. Freyd Category appears to be his first content creation. (from his website linked from his nLab page he says he is a student of Paul Blain Levy who came up with Freyd Categories. Maybe he just needs more time or encouragement.)

I’ve created the page identity-on-objects functor. It is pretty basic with no mention of size or evilness.

An identity-on-objects functor $F: \mathbb{A}\to \mathbb{B}$

• Is between categories with the same objects - $Obj = ob(\mathbb{A}) = ob(\mathbb{B})$.
• Has as its underlying object function $F_{ob}: Obj \to Obj$ the identity function on $Obj$.

I’ve updated Freyd category to link that along with saying that $\mathbb{V}$ and $\mathbb{C}$ have the same objects, footnoted that this is implied or required by having an identity-on-objects functor.

EDIT: Google says that identity–on-objects shows up on 126 nLab pages. I don’t know how many of those usages are compatible with the definition I gave and which of those pages should be linked to the definition.

• CommentRowNumber11.
• CommentAuthorUrs
• CommentTimeJun 3rd 2017
• (edited Jun 3rd 2017)

Rod: What I am saying is that he does not seem to be participating here on the $n$Forum. He should. The HomePage asks people who make edits on the $n$Lab to announce their edits here on the $n$Forum. Many do not. (I am suspecting the fact that the $n$Forum requires a login is off-putting, I wish instead the $n$Forum were open, but I don”t know how to change it.) If you know him, maybe you could contact him personally.

• CommentRowNumber12.
• CommentAuthorbgeron
• CommentTimeJun 5th 2017
Hi all,

Thanks to Noam for pointing me to this discussion. I didn't read the homepage far/thoroughly enough to realise that my presence and activity here would be appreciated :) Thanks, Urs, for making this post and realising I'm not really on the nForum.

Thanks Urs and Rod for expanding/formatting the stub entry on Freyd categories I made. I just quickly made the entry because I keep forgetting what a Freyd category is and it's tiresome to look it up otherwise. I don't really have anything else to say about them really!

In case I forget to check the nForum for replies, you're welcome to ping me at firstname @ firstname . xyz.

Cheers, Bram
• CommentRowNumber13.
• CommentAuthormaxsnew
• CommentTimeSep 21st 2017

I updated the references to make clear that this was introduced earlier by Power-Thielecke, not by Levy.

Also, I’m currently reading/using a lot of these papers on modelling effects using monads and I’ve noticed the nlab material is quite thin. Would it be a welcome addition to write more about it? In my experience you end up with a lot of structures that seem very bizarre from a category-theoretic POV like Freyd categories and premonoidal categories that use non-natural transformations and identity-on-objects functors, so it seems like the kind of thing that goes against the nlab philosophy.

• CommentRowNumber14.
• CommentAuthorTodd_Trimble
• CommentTimeSep 21st 2017

What does “locally $\emptyset$-presentable” mean?

• CommentRowNumber15.
• CommentAuthorTodd_Trimble
• CommentTimeSep 21st 2017

Max, I’m sure it would be welcome.

• CommentRowNumber16.
• CommentAuthorUrs
• CommentTimeSep 21st 2017

I’m currently reading/using a lot of these papers on modelling effects using monads and I’ve noticed the nlab material is quite thin. Would it be a welcome addition to write more about it?

• CommentRowNumber17.
• CommentAuthorDavidRoberts
• CommentTimeSep 21st 2017

It occurs to me that an identity on objects functor $C\to D$ can be defined for a wider class of categories, if we consider them defined in a dependently typed way. Namely, given a collection $O$ of objects we have homs $C(x, y)$ and $D(x, y)$ for $x,y:O$ and functions $C(x, y) \to D(x, y)$ that preserve composition.

• CommentRowNumber18.
• CommentAuthorMike Shulman
• CommentTimeSep 22nd 2017

An identity-on-objects functor is also just a category enriched over $Set^\to$, and as mentioned at premonoidal category it can be defined more abstractly using the funny tensor product on $Cat$. So I don’t think they are un-categorical.

• CommentRowNumber19.
• CommentAuthorRodMcGuire
• CommentTimeSep 22nd 2017
• (edited Sep 22nd 2017)

Mike, I saw your changes to identity-on-objects functor.

I think what we need is a name for the structure which is two categories sharing the same objects. Might I suggest twin category, though this might be misleading because it really isn’t a category.

E.g. you can’t just have a functor from some category to a twin pair. Something must be provided to specify which twin component the functor goes to, somewhat like

• $F: A \to first(Twin)$

Maybe category twins for the name? (even better metaphorically might be the name conjoined twins but that may be too gruesome, and “conjoined” might be assumed to have a mathematical not anatomical meaning)

Edit: How about category siblings? with the metaphor being they share things (objects). Though the metaphor is somewhat off in that it might convey that they have some notion of parent that they share.

• CommentRowNumber20.
• CommentAuthorRodMcGuire
• CommentTimeSep 22nd 2017

There is another need for a general name for a structure of conjoined categories that share the same objects. Namely a subcategory of category shares objects with the category and if it is a wide subcategory it has the same objects, as does a structure composed of two wide subcategories.

There are all sorts of extra things you can do with subcategories that depend on (some) of their objects being the same that you can’t do with a family of unconjoined categories.

• CommentRowNumber21.
• CommentAuthorMike Shulman
• CommentTimeSep 22nd 2017

Why do you think we need a name for two categories with the same objects and no relation between their arrows? I can’t think of any examples where such a thing arises. A wide subcategory is the same as an M-category. And I haven’t thougt about this before, but I suspect that a category equipped with an arbitrary subcategory could be identified with a category enriched over a certain 2-object bicategory or double category.

• CommentRowNumber22.
• CommentAuthormaxsnew
• CommentTimeSep 22nd 2017

Added a brief idea section.

• CommentRowNumber23.
• CommentAuthorTodd_Trimble
• CommentTimeSep 22nd 2017

I’m still wondering (cf. #14) what a locally $\emptyset$-presentable category is. Is it a case of some tricky negative thinking or some such thing?

• CommentRowNumber24.
• CommentAuthorMike Shulman
• CommentTimeSep 22nd 2017

I’m wondering that too.

• CommentRowNumber25.
• CommentAuthorMike Shulman
• CommentTimeSep 23rd 2017

Well, “locally $\emptyset$-presentable” was added in the original version of the page by Bram Geron, who may not be reading the forum, and the doi link in the citation given is broken. But I found another copy of the paper cited here, and it looks like what is meant is a “locally $D$-presentable category” where $D$ is the “empty sound doctrine”; see sections 2.2, 3.1, and 3.2.

• CommentRowNumber26.
• CommentAuthorSam Staton
• CommentTimeDec 28th 2021

Little bit more detail about the Freyd category from a strong monad.

• CommentRowNumber27.
• CommentAuthorSam Staton
• CommentTimeDec 28th 2021

A bit more background in the opening paragraph.

• CommentRowNumber28.
• CommentAuthorUrs
• CommentTimeDec 28th 2021

I have added some hyperlinks to keywords and author names; and I fixed the grammar of the second sentence (“…consisting of a category that model[s]…”).