Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: reference request

John van de Wetering (Nov 29 2020 at 18:31):

Not sure if there was already a topic for asking about specific references, so I made one (please move it if I'm wrong).

John van de Wetering (Nov 29 2020 at 18:32):

I'm looking for the canonical reference for Frobenius algebras

John van de Wetering (Nov 29 2020 at 18:32):

Would anyone here happen to know what that would be?

John van de Wetering (Nov 30 2020 at 10:18):

What I've found so far: In this 1987 paper they have a notion of 'discrete' object that is a Frobenius algebra https://www.sciencedirect.com/science/article/pii/0022404987901216
But, in this 1969 Lawvere paper, he already has a notion called Frobenius algebra that seems to be equivalent: https://link.springer.com/content/pdf/10.1007/BFb0083085.pdf
The way he defines it makes me think that there must be an even older paper using the categorical definition of a Frobenius algebra

John Baez (Nov 30 2020 at 17:25):

Dd you try @Joachim Kock's history of Frobenius algebras? He writes:

Bill Lawvere knew about the categorical characterisation of Frobenius algebras in 1967, but he did not explicitly write the Frobenius equation. In Chapter 2, I write that the first explicit appearance of the Frobenius equation is in the lecture notes of Quinn (published in 1995, lectures from 1991). This turns out to be wrong...

John van de Wetering (Nov 30 2020 at 22:18):

I was expecting this to be a straightforward question, I didn't realise the answer was this complicated :P

John van de Wetering (Nov 30 2020 at 22:18):

Guess I will have to cite more then one paper then

Spencer Breiner (Apr 14 2021 at 22:06):

Hi all. Does anyone know where I can refer to the adjunction between operads and monoidal categories? I didn't see it in a cursory look through Leinster or Yau, though it's probably in one of those two somewhere. Thanks!

Spencer Breiner (Apr 14 2021 at 22:07):

Any variant will probably do, but symmetric monoidal categories and multicategories/colored operads is most relevant.

Nathanael Arkor (Apr 14 2021 at 22:13):

The canonical reference is Hermida's Representable Multicategories.

Mike Shulman (Apr 15 2021 at 01:17):

A general version is in section 9 of A unified framework for generalized multicategories.

Spencer Breiner (Apr 15 2021 at 16:08):

Thanks Nathanael Arkor & Mike Shulman!

Christian Williams (Apr 22 2021 at 21:49):

$\lambda$-calculi are equivalent to cartesian closed categories. similarly $\lambda$-calculi with equality types should be equivalent to cartesian closed categories with equalizers (aka "properly CCCs" in the Elephant). anyone know a reference for this?

Fawzi Hreiki (Apr 22 2021 at 22:45):

There's this paper which gives a dependent type theory corresponding to categories with finite limits. It seems fairly straightforward to just add function types to obtain what you want.

Mike Shulman (Apr 23 2021 at 03:05):

What do you mean by "equality types"? If you mean equality types in a dependent type theory, then it's not so easy to formulate a dependent type theory corresponding to cartesian closed categories that aren't locally cartesian closed. Just asking for non-dependent function-types $A\to B$ instead of $\Pi$-types isn't good enough: since type formers can be applied in any context, semantically this already requires that all slice categories are cartesian closed, which is equivalent to local cartesian closure.

Mike Shulman (Apr 23 2021 at 03:06):

The best theory I can think of for CCCs with finite limits would be a logic with equality over STLC, so that you have equality propositions but not equality types.

Christian Williams (Apr 23 2021 at 04:40):

I think I'm seeing in Jacobs Ch3 what you're referring to, but I'm confused why we need to bring in logic over STLC. why isn't Eq just another type former like product?

Christian Williams (Apr 23 2021 at 04:49):

I guess it's different because it's parameterized by terms rather than types.

Christian Williams (Apr 23 2021 at 04:53):

so it looks like the codomain fibration of a finitely complete category $cod_C:[I,C]\to C$ has "fibered equality", and I think that should give STLC+equality.

Christian Williams (Apr 23 2021 at 04:54):

oh, maybe just the subobject fibration, yeah.

Christian Williams (Apr 23 2021 at 04:54):

I wasn't expecting to have to bring in this extra structure, but I guess that's fine. thanks for the pointer.

Christian Williams (Apr 23 2021 at 05:01):

it feels weird to say $Eq(f,g):Prop$ when there is no Prop, no subobject classifier.

Christian Williams (Apr 23 2021 at 05:06):

I guess Prop just refers to the total category of the subobject fibration.

Christian Williams (Apr 23 2021 at 05:07):

any way, I can see that the answer is here, but it is often not easy to find things in Jacobs. it has a lot but it's all mixed together.

Christian Williams (Apr 23 2021 at 05:14):

Fawzi Hreiki said:

There's this paper which gives a dependent type theory corresponding to categories with finite limits. It seems fairly straightforward to just add function types to obtain what you want.

thanks for the reference; it looks good. but I'm having trouble understanding how these rules encode an equalizer:
ext-equality.png

Christian Williams (Apr 23 2021 at 05:16):

I picture the universal property and expect the inference rules to encode the property directly. though maybe it's not always that simple.

Christian Williams (Apr 23 2021 at 05:22):

I should take this to another thread.

Verity Scheel (Apr 23 2021 at 15:16):

I can try to help with the type theory side of this:

The third rule (E-Eq) is where the magic happens: in the formal language of type theories, it says something like “if you have a proof that $c =_{C} d$, then you may treat $c$ and $d$ as equal in the type theory”. It goes by the name equality reflection, it’s what makes the theory “extensional”. (The terminology is confusing, see https://ncatlab.org/nlab/show/extensional+type+theory#definitional_extensionality for more.)

But anyways, if you know that you can treat $c$ and $d$ the same (that’s what the judgment $c = d \in C$ means, roughly speaking), then you can get stuff like Leibniz rule ($F(c)$ and $F(d)$ must also be the same), and I guess the universal property.

Christian Williams (Apr 23 2021 at 16:06):

but they're not equal; they're just a pair of parallel morphisms, and we want to specify the subobject of terms that are equalized by them.

Verity Scheel (Apr 23 2021 at 16:55):

Yeah, this specifies the equality type. You can form equalizers using it along with the indexed sums: https://ncatlab.org/nlab/show/equalizer#in_type_theory

Verity Scheel (Apr 23 2021 at 17:08):

But it looks like they interpret the equality type via equalizers of the interpretations in the appropriate category (page 1116), so it is actually an equalizer in the interpretation even though it doesn't quite look like one internally.

Christian Williams (Apr 23 2021 at 17:10):

okay I see, thanks

Verity Scheel (Apr 23 2021 at 17:22):

Proposition 5.11 (page 1130) gives the construction of pullbacks.