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: theory: type theory

Topic: cats in types

Faré (Apr 14 2020 at 04:43):

I've seen category theory packages for Agda, Coq, to a point Haskell. They all seemed somewhat heavyweight and/or unsatisying, especially compared to what usually passes for "trivial" in category theory.

Has there been a study of what kind of automated type inference is or isn't sufficient or necessary to trivialize the type-correct treatment of casual category theory notation?

Faré (Apr 14 2020 at 04:46):

Goal: be able to write something as succinct as is commonplace on this forum, and get a fully type-annotated term that makes sense in dependent type theory (or whatever is appropriate) with an appropriate level of generality.

Faré (Apr 14 2020 at 04:46):

(Or is that already trivial in Coq or Agda or Idris?)

Dan Doel (Apr 14 2020 at 04:55):

Some of it may be the approach used. I haven't looked in a while, but the stuff in Agda I've seen is formalizing the symbolic reasoning of 'universal arrow' and diagram chasing type arguments. I'm not sure that's ever going to look nice, and most of the elegant arguments you see people use here aren't going to be like that.

Dan Doel (Apr 14 2020 at 04:56):

Like, it isn't even nice (if you ask me) in the category theory books that try to take that approach.

James Wood (Apr 14 2020 at 08:02):

There are various things lacking. One is that the theory implemented by most of today's MLTT-style proof assistants has a rather poor notion of equality for use in category theory. This forces us to be very explicit about equality, and adds difficulty to any reasoning or automation about equality. Apart from that, there is the orthogonal issue that in many cases, the proof engineering technology is still lacking. Often, we want to work up to easily checked equality, which is not offered out of the box (this is to say we want to work in a free structure, taking all of the equations the free structure gives for granted). This has been done for some instances, but seems to take a lot of work for each new bit of structure we introduce (and is typically rather uncompositional). For where it has been done, I like the way Conor McBride did it here, where equational reasoning can be interspersed with automated steps.

Thibaut Benjamin (Apr 14 2020 at 09:04):

I know different ways of doing this : the first thing you can do, if you want to define categories in a proof assistant, is to rely on axiom K or UIP or something like that, that basically ensures proof irrelevance of everything you define. If you are not familiar with this construction, it says that whenever you have two terms of the same identity type, they are automatically equal (well to be precise, that's UIP, proof-irrelevance is a bit weaker, and axiom K a bit stronger). So basically the only thing that matters with equality types is if they are inhabited. In other words we only care to know if two things are equal and not how two things are equal. This matches well enough what most people encounter when doing category theory, and you can develop some category theory in this framework - but you will run into some problems quite quickly, in fact as soon as you want to talk about limits and colimits, since they are defined only up to isomorphism, so the simple sentence "let $C$ be a category with finite limits" is not at all easy to express, you have to give an explicit choice of a limit for each finite diagram, and keep track of these choices properly, it becomes a real mess.
An option to solve this is the one of univalent categories as defined in HoTT, and here I will assume some familiarity with the language of HoTT. In univalent categories, you want an arbitrary type of objects, but really a set of morphism (meaning two morphisms can only be equal in at most one way - UIP for morphisms if you want), and then you throw in all the axioms of a category, plus univalence. Univalence states that the type of equality between two objects is equivalent to the type of isomorphisms between those objects. So in short, it is an axiomatisation of categories in which equality of objects is defined to be isomorphism. This makes the problem of choice of limits much better, since any two choices are isomorphic, and hence equal, so there is really just one choice.
To my knowledge, these have been implemented in the UniMath library, but from my little experience with it, its use is still quite difficult

Thibaut Benjamin (Apr 14 2020 at 10:51):

I should also point out that you can formulate the "internal language" of categories in type theory. This is I think a bit different than what you are looking for, as it is a type theory in its own right, and not a development you would do internally to Coq or Agda, but it goes like this

• introduce a type $\bullet$ which is always defined - a term of type $\bullet$ is an object of the category
• introduce a type constructor $\to$, which given two terms $t$ and $u$ of type $\bullet$ lets you introduce the type $t\to u$. A term of type $t \to u$ is a morphism from the object $t$ to the object $u$
• introduce a constructor $\mathrm{id}$, which given a term $t$ of type $\bullet$ spits out a term $\mathrm{id}(t)$ of type $t\to t$
• introduce a constructor $\mathrm{comp}$ which given two terms $f$ and $g$ of type $t\to u$ and $u\to v$ spits out a term $comp f g$ of type $t \to v$
• these satisfy the equalities $\mathrm{comp} (\mathrm{comp} f g) h \equiv \mathrm f (\mathrm{comp} g h)$ and $\mathrm{comp} (\mathrm{id}(t), f) \equiv f$ and $\mathrm{comp}(f,\mathrm{id}(u)) \equiv f$.
  Anything that you can define in a category, you can define it type theoretically in this type theory. But you wouldn't go very far, as it only axiomatize one category, there is no functor, no adjoint functor... You could probably define what is a monad as being an operation on the syntax, but that seems like it's making things more complicated instead of making them simpler.

There may be a way to axiomatize the category of categories as a type theory, and really do actual category theory with a suitable type theory, but I am not aware of it

James Wood (Apr 14 2020 at 11:02):

Thibaut Benjamin said:

There may be a way to axiomatize the category of categories as a type theory, and really do actual category theory with a suitable type theory, but I am not aware of it

I think the relevant keyword is “directed type theory”.

Reid Barton (Apr 14 2020 at 11:37):

It might help if @Faré could give examples of what seemed "heavyweight and/or unsatisfying".

Thibaut Benjamin (Apr 14 2020 at 11:49):

James Wood said:

Thibaut Benjamin said:

There may be a way to axiomatize the category of categories as a type theory, and really do actual category theory with a suitable type theory, but I am not aware of it

I think the relevant keyword is “directed type theory”.

Thanks, I looked this up and found a paper "2 dimensional directed type theory" by Licata and Harper, it seems to do the job indeed. Most of the result are thouhg point towards directed homotopy type theory, that would give a type theory whose types are $(\infty,1)$-categories. That is probably too much compared to the initial question. I will try to check this "2-dimensional" case, I didn't know about it

Faré (Apr 14 2020 at 13:54):

@Reid Barton I am unhappily not sophisticated enough to give a good answer, but the treatment of equality, of quotients, etc., seems particularly heavyweight, e.g. involving setoids everywhere. Maybe that's now solved in Cubical Agda, HoTT Coq, etc.

Reid Barton (Apr 14 2020 at 15:01):

Ah yes, the explicit setoids are somewhat tolerable at best. But in a system with quotients (like Lean, or I think they can be encoded similarly in Coq) there's no need to work with these "setoid-enriched" categories.

Reid Barton (Apr 14 2020 at 15:04):

In fact I gave up on Agda for formalization of mathematics long ago (before HoTT was really a thing, I think) for precisely this reason of needing setoids in category theory.

Dan Doel (Apr 14 2020 at 15:15):

Yeah, there's a history of a huge gap there in (intensional) type theory, and even though there have been ideas of how to plug it for a long time, they haven't been implemented in most systems.

Dan Doel (Apr 14 2020 at 15:21):

The homotopy inspired version might end up being better than any of the rest, though, so it's nice that that one's actually getting implemented. :slight_smile:

Andre Knispel (Apr 16 2020 at 10:12):

This issue was one of the main motivations for me to start working on meta-cedille. I recently gave a demo about it, where I demonstrated the possibility to work and reason in an internal logic that has been formalized in the type theory. There is still some work to be done to reason nicely within categories, but all of that can be done by the user (i.e. no need to change the system). It can also replace types with setoids without syntactic overhead and I see no reason why you shouldn't be able to do cubical or something in there as well (again, with out syntactic overhead and without changing the underlying system), so multiple of the paths that are proposed here are possible in there.

Andre Knispel (Apr 16 2020 at 10:14):

The talk I gave is linked on the wiki there