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.
Morgan Rogers (he/him) (Sep 06 2020 at 13:02):Continued from here
This is all great as long as you are interpreting your theory in a category which has enough structure to interpret the syntax for any choice of interpretation of the signature. Following Fabrizio's example, if my syntax includes exponentials/hom-objects, then any interpration of the signature extends to an interpretation of the whole syntax/language in a nice way. But what about when that only sometimes holds? There may still be some valid models, but I have to prove that all of the interpretations of the syntax give well-defined structures :grimacing:
Morgan Rogers (he/him) (Sep 06 2020 at 13:05):For example, any category with a terminal object contains a model of a group: the trivial group on the terminal object, since the product of the terminal object with itself is still the terminal object. But not every such category has products (or more generally, is a monoidal category).
Morgan Rogers (he/him) (Sep 06 2020 at 13:10):There is no general solution to this problem, but there are partial solutions. The main one is to look for subcategories which are closed under the required structure. In the exponential/hom-set example, we would need to look at subcategories of exponentiable objects. Some care must be taken to ensure that these categories still have the rest of the structure needed to interpret the syntax (eg we still need closure unter the monoidal product too!), and we won't always get all of the models of our theory this way. But when we get lucky, we'll find a big "good" subcategory where we can work safely with the structures we want to.
Morgan Rogers (he/him) (Sep 06 2020 at 13:12):Sorry for side-tracking the discussion this is the :sweat_smile: this is the area of stuff I'm working on right now, and I felt a compulsion to write about it. I may move it elsewhere later :innocent:
Jacques Carette (Sep 06 2020 at 14:12):Wherever you do discuss this, please do continue! I have grad students implementing a lot of the underlying things you mention (various manipulations on signatures and languages, inside a host logic but also transporting between logics). We're walking a fine line between programming things for which we know there exists current meta-theory that says that what we're doing is meaningful, and hacking things up that 'seem' to work, but might be meaningless at the level of generality we're doing it [i.e. we're missing side conditions.]
Including things like Zero objects for various theories (you mention group). I'm quite sure our constraints for the validity of that are not quite right. [Sometimes we don't care, as some meta-operations are not guaranteed to give non-trivial theories; but if they do non-trivial theories 'for free', that we surely would like to know.]
Morgan Rogers (he/him) (Sep 06 2020 at 15:44):For my current project I'm actually reverse-engineering a logic from a class of categories. If done successfully, this circumvents the kinds of problems that you're describing because by construction I will be able to interpret all of the syntax in my theory in the categories I care about. This hints at an alternative approach to the one I mentioned above: if your target category can't interpret all of the syntax in your theory, see if you can move down to a smaller fragment of logic, or across to a fragment which is sufficiently expressive for your purposes, and which can be interpreted in your target category.
As a hypothetical example, suppose your categories don't have infinite unions of subobjects, but it does have power objects. That means that we can't interpret full geometric logic (which requires arbitrary small disjunctions of formulae to be interpretable), but we can interpret some second-order logic. Then we still have a way of talking about local rings, which can be axiomatised in either fragment (at least in a way that gives equivalent models in ).
Morgan Rogers (he/him) (Sep 06 2020 at 15:50):Making this kind of leap requires deep familiarity with the structural nature of your target category, though. When it comes to computer science, that means choosing a type theory/category of types, and doing the work to understand the consequences of such a choice. This is a world I find rather intimidating, so I need for context if I'm going to dive into it.
Nathanael Arkor (Sep 06 2020 at 19:05):Out of curiosity, what class of categories are you interested in (if you don't mind answering)? Or was your hypothetical example not so hypothetical?
Morgan Rogers (he/him) (Sep 07 2020 at 08:15):Nathanael Arkor said:
Out of curiosity, what class of categories are you interested in (if you don't mind answering)?
It's a class which I don't have a good name for, which I'm provisionally calling pre-regular, although that is a Bad Name since is already something by that name in the literature, and the link to regular categories is rather weak.
Call an indexing category a funnel if it has a weakly terminal object. The categories I am looking at are those having all funneling colimits (colimits of diagrams indexed by funnels) and their class of strict epimorphisms is stable; I'm not assuming that pullbacks exist, but that any cospan where one leg is a strict epimorphism can be completed to a commutative square where the opposite side is also a strict epimorphism. Introducing them like this hides why this is a nice class to study, but you can already see that if such a category is to interpret a theory, then since it doesn't typically have finite limits or colimits, several of the most basic logical operations in algebraic, regular, coherent, geometric or first-order logic have to go out of the window.
Nathanael Arkor (Sep 07 2020 at 12:20):What are a couple of motivating examples of these categories?
Morgan Rogers (he/him) (Sep 07 2020 at 12:45):The objects isomorphic to quotients of representables in any presheaf topos form such a category. From that perspective, they present an alternative to completing sites under finite limits. Rather than giving more examples, I'll just plug the paper on "supercompactly generated toposes" that I'm hoping will be in a state to put online by the end of next week. The pursuit of a logic for these categories will form the basis for another paper which is already in the works :wink:
Nathanael Arkor (Sep 07 2020 at 13:21):Looking forward to taking a look!
Jacques Carette (Sep 07 2020 at 13:32):@[Mod] Morgan Rogers you asked about my context. I have not really tried to pin down a single target category. In fact, I am much more interested in a bunch of such categories (they probably form a lower semi-lattice). What I can about is the eventual functionality: I want to be able to write things in a reasonable meta-language that can then be interpreted in Agda, Coq, Isabelle/HOL, HOL-Light, and so on. A preview of that can seen from our preliminary work at CICM 2020 paper.
I see as being able to reason about structured syntax (and its eventual interpretation).
A good test of such a framework (that Universal Algebra fails) is to take the dependently-typed definition of a Category and automatically derive the definition of its homomorphisms (aka Functors), the homomorphisms of those (aka Natural Transformations), and from the definition of equivalence of categories. In theory, I think I know how, but I don't have adequate meta-theory that justifies all the steps. Of course, it should equally well apply to a very large set of 'theories' defined in the same meta-language.
Nathanael Arkor (Sep 07 2020 at 13:38):Do you mean you want to prove that a definition of homomorphism is the correct one, internal to the programming language the framework is written in, or would an external proof be sufficient?
Nathanael Arkor (Sep 07 2020 at 13:40):(Because the correct definition of homomorphism will be given by an interpretation of the theory of categories, e.g. as a GAT, in itself — but perhaps this is not sufficient for your purposes.)
Morgan Rogers (he/him) (Sep 07 2020 at 13:49):Jacques Carette said:
I want to be able to write things in a reasonable meta-language that can then be interpreted in Agda, Coq, Isabelle/HOL, HOL-Light, and so on.
I figured it would be something like this: each of these languages is built on a different type theory. A quick google mentions "unified theory of dependent types", "predicative Calculus of (co)Inductive Constructions" and "weak type theory" for the first three respectively. I don't know the details of any of these, but I can still make general comments: the type constructions you need in order to express (generalised) algebraic theories are some of the most basic ones, so most if not all of the type theories employed in functional programming languages will interpret them; you won't have any trouble just building models of these theories. What you were saying about results regarding the categories of these things, on the other hand, will be more subtle. Certainly such results are constrained by the corresponding properties (existence of limits etc) in the underlying category of types.
Jacques Carette (Sep 07 2020 at 14:03):@Nathanael Arkor I want to generate the definition of homomorphism. A la Universal Algebra. Eventually, I want a Universal-Algebra like theory of manipulations of GATs into (parametrized) GATs.
It's probably worthwhile mentioning that I really want the computer scientist's approach to all of this. It's all about folds and syntactic manipulations, backed by a meta-theory that says that the syntactic manipulations have a good denotational semantics.
Nathanael Arkor (Sep 07 2020 at 14:16):The definition of homomorphism is given inductively by the definition of (endo-)"interpretation of a GAT" in Cartmell's paper. If you define a group as a GAT, and look at the definition of interpretation of the GAT of groups in the GAT of groups, it should be the classical definition of a group homomorphism (and likewise for non-algebraic structures). The approach of Cartmell is already very syntactic (some would say too syntactic).
Nathanael Arkor (Sep 07 2020 at 14:16):In what sense are you using the term "parameterised GAT"?
Jacques Carette (Sep 07 2020 at 14:22):I need to reread Cartmell.
By parametrized, I mean that the GAT has a non-empty context. The definition of homomorphism assumes two structures are in context. Putting them in the GAT itself (via a Sigma type) is a hack.
Reid Barton (Sep 07 2020 at 14:24):Or maybe an example like "a monoidal structure on a given category"?
Nathanael Arkor (Sep 07 2020 at 14:31):The definition of homomorphism assumes two structures are in context.
Right, you have to have two definitions: of a GAT, and a GAT homomorphism (which is defined in terms of a source and target).
Putting them in the GAT itself (via a Sigma type) is a hack.
I think this is more than a hack: it ought to establish that the category of GATs is cartesian-closed (though I don't believe this has been worked out anywhere).
Jacques Carette (Sep 08 2020 at 13:28):@Reid Barton I'm not sure I understand your suggestion?
@Nathanael Arkor I agree that the fact that the category of GATs is (likely) cartesian-closed is not a hack. This is however related to the bundling-unbundling problem that most proof assistants have. One issue with internalizing the parameters is that it forces the universe level up, which is definitely undesirable.
Reid Barton (Sep 08 2020 at 13:31):Just an example where you'd want to consider additional algebraic structure in the context of some already existing algebraic structure.
Your example of homomorphisms seems a bit too special because presumably the notion of homomorphism of structures has a special status.
Jacques Carette (Sep 08 2020 at 13:52):There's also 'signature' (strip out the equations), 'term algebra' (which come in different variations depending on how you parametrize by a theory of free variables), product theory, 'evaluator' (from the term language back into the theory), 'staged terms' (which mix both the term algebra and the language), induction principle, recursor, relational interpretation, and many more. We've got about 1/3 of our list implemented.
Our library of 227 theories (spanning 316 lines of code) becomes a library of 5047 definitions which, when pretty-printed, take up 106468 lines of code. Current practice would have those 100K lines written by a human. The actual 'information content' is much, much smaller.
Morgan Rogers (he/him) (Sep 08 2020 at 14:19):With those numbers, I can see why one would put the effort into building a universal library! I appreciate what you're trying to do.
I think the cartesian-closed structure of a category of GATs doesn't quite give you what you want for homomorphisms. I worked it out to be the following... For algebraic theories over respective signatures , a model of the theory consists of a mapping between the signatures (sorts to sorts, function symbols to function symbols), a model of , a model of , and functions for each sort of , such that if is a function symbol in , we have .
That not only involves going up a level, understanding the collections of sorts and function symbols of a signature as types rather than fundamental, it also includes too much stuff: I don't want homomorphisms to be allowed to swap two sorts or two function symbols of a theory.
Rafaël Bocquet (Sep 09 2020 at 07:26):Jacques Carette said:
Nathanael Arkor I want to generate the definition of homomorphism. A la Universal Algebra. Eventually, I want a Universal-Algebra like theory of manipulations of GATs into (parametrized) GATs.
It's probably worthwhile mentioning that I really want the computer scientist's approach to all of this. It's all about folds and syntactic manipulations, backed by a meta-theory that says that the syntactic manipulations have a good denotational semantics.
Have you read "Constructing Quotient Inductive-Inductive Types" (https://akaposi.github.io/finitaryqiit.pdf) ? It seems to be exactly what you ask for.
Jacques Carette (Sep 09 2020 at 11:23):I have. And I've had conversations with the authors.
It solves a different, interesting problem. Of course, 'solves' here is a big word, since none of the systems that I'm interested in actually implement QIIT !
The structures that I want to generate "fit" in the current systems. So new structures are not needed.