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.
Julius Hamilton (May 19 2024 at 14:28):I am wondering if there is terminology to distinguish between what something is defined “in terms of” or “with reference to”, vs. what something is.
For example, a cone is defined “with reference to” a diagram. That is why it is technically called, say, “a cone of a functor”, or, “a cone over a diagram”. We cannot define a cone without a specifying a diagram. It exists in relation to it.
A cone also requires the specification of an object, . For some functor and for an object , a cone “from to ” is a family of morphisms.
So a cone requires an object and a functor to be defined, but “what it is” is a family of morphisms.
Is there terminology that would allow you to ask, “What is a cone?”, where I want to know the second case - that eliminating context, it is “a family of morphisms”. ?
Nathan Corbyn (May 19 2024 at 15:22):I'm not sure I quite understand the question, but a concise way to describe a cone is as a natural transformation (see here under 'Cones over a diagram').
Spencer Breiner (May 19 2024 at 15:39):I would say that this misses the idea that "what something is" should include not only the data needed to specify it, but also the data to distinguished it from another thing of the same kind.
In this case, the family of arrows is sufficient to specify a cone, but different cones may share the same family of arrows (over different diagrams)
Jean-Baptiste Vienney (May 19 2024 at 17:01):It’s not answering your question but there is a small ambiguity in asking “What is a cone?”. It could mean what is a cone in general or what is a cone in particular. By the second sense I think to “a” as it is used when you ask “How can someone know who is a person?”.
Kevin Carlson (May 21 2024 at 02:36):Usually formal mathematics avoids any aspects of these questions that might become philosophically nontrivial; for instance, one might specify that "a cone" is a triple of a functor, an object, and a family of maps satisfying the cone condition, or one might say that "a cone over with tip " is the only concept that's being defined, without giving any notion of "a cone" at all. Interestingly, the latter gives "cones" as a dependent family of sets, while the former gives "cones" as the fibered family formed by the "sum type" or "Grothendieck construction' of the dependent family.
Julius Hamilton (May 21 2024 at 02:47):That sounds interesting.
I was thinking that from the perspective of type theory, I basically mean the “top level type”, of a composite type. For example, a function from groups to integers is most fundamentally a function, not a group.
Maybe there is a formal operation in type theory that is sort of like a forgetful functor where you can forget the details and focus on what the most definitive “type” of something is?
In programming, the return type of a function is important information. It determines what you can do with the output, what methods can or cannot be called. That is what I think of as the “fundamental type”. When I say is a family of morphisms, I cannot say, “What is the domain of ?” A function has a domain. A family does not.
So that’s the rough idea.
Kevin Carlson (May 21 2024 at 03:30):Type-theoretically, I'd say that a cone is a term of the type for some and . You could then construct the type of all cones over functors as , and the type of all cones by a further $$\Sigma$ over the domain and codomain on which the variable depends. Is this $$\Sigma$ something like the "forgetful" operation you're looking for?
Julius Hamilton (May 21 2024 at 10:08):I’m not sure, but all the messages I’ve received in this thread have been stimulating, and over time I’ll be able to come back to my question with a new perspective.