Comments (11)
I gave it another try. Much of which is now checked-in, so that there is a definition of 2-Category
now. And it is indeed 'Strict', and some other stuff along with it.
But it eventually breaks down. Again, extensionality is an issue. For example, the category Functors
with objects Functor
and NaturalTransformation
as morphism, cannot have ≡
as its object equality; well, it can, but nothing about it is provable. [Proof relevance would also be a problem, but extensionality hits first].
My thinking is that Strict category theory is a very Set-based phenomenon, where it makes sense to have a single, global equality relation, and where proofs are not first-class. As some of it does work, it is checked in. But I would not be heartbroken if that was reverted. There's also some incomplete code in the Strict2Cat
branch, to show where things really hopelessly break down.
My conclusion is that in ITT/MLTT, 'Strict' categories must actually be "locally strict" in the sense that Obj must be a Setoid, in the same way that currently Hom is Setoid enriched. Of course, just like \o-resp-~~ needs to be added for things to work, something similar would be needed too.
from agda-categories.
So in branch Strict, I implemented a lot of Strict category theory, with a particular design in mind: That
Category
itself wouldn't be parametrized by an equality, but would use the surrounding propositional equality≡
instead.
Could you elaborate a bit on that? It seems a strange thing to do in an intensional type theory, no? Since category theory traditionally assumes an "extensional" meta-logic, it would surprise me if one could express many interesting things using such a weak notion of equality. Doesn't one either have to go with Bishop's approach of using setoids, or go the HoTT route and assume additional axioms (e.g. univalence)?
My conclusion is that in ITT/MLTT, 'Strict' categories must actually be "locally strict" in the sense that Obj must be a Setoid, in the same way that currently Hom is Setoid enriched.
That seems reasonable to me. And for some constructions I believe it's actually necessary (see my comments in #41). Of course this will complicate definitions substantially.
But, I don't think that the difference of strict vs. weak category theory does/should ultimately come down to a particular choice of equality, or to object sets vs. object setoids. I think it comes down do the choice of coherence maps (unitors, associators, etc.)
The nLab page on bicatgories lists strict 2-categories as an example of bicategories:
Any strict 2-category is a bicategory in which the unitors and associator are identities.
Why not use this as a definition instead? Whatever the (local) notion of equality on morphisms is, it gives rise a notion of identity that can then be used to figure out the right "strictification", either directly or (where possible) by defining the weak structure first and then instantiating it to the strict case. Even though this sounds trivial, it is generally not: because we are in an intensional metatheory, identities (in the categorical sense) may have more structure than expected. E.g. in an extensional setting the domain and codomain of an identity are definitionally equal, but here they need not be. They need only be equal up to the identity the next level up.
For example, in #42, I propose a rework of functor equality that is based on this idea: strict functor equality is natural isomorphism where every component is an identity. But the domain and codomain of these identities need not agree definitionally.
Another example is the Gorthendieck construction. There's now an implementation for pseudofunctors, that involves a whole bunch of up-to-coherent-natural-iso constructions that would all have been identities in an extensional setting.
from agda-categories.
It's important to remember that I'm partly teaching myself category theory [the subtler points thereof] and constructive type theory while doing this. I'm an 'analyst' by training (i.e. the Pure Math version) and then evolved into a computer scientist. So I'm self-taught on almost all we're talking about here, which means that I have weird holes in my understanding.
In particular, I may well have made a really sub-optimal choice for Strict. If nothing else, under Strict, I should have assumed K. It would have worked quite a bit better. And indeed, choosing to use ≡
might simply have been a misguided choice. But I learned stuff by trying to push this through!
Yes, traditional CT does assume an extensional meta-logic. Here, in Agda, it is interesting to see exactly when that comes in. In the old library, some of that was swept under the carpet by using irrelevance, which is definitely where some things break down.
There might already be 2 HoTT-based libraries of CT (one in 'plain' Agda but assuming univalence, another in cubical Agda), but my understanding is that both are still fairly small. And certainly doing CT a la HoTT would be best done in cubical Agda. But that's a different library (no less interesting!).
Having said that, I definitely like the suggestion of starting from bicategory and understanding strictness as having certain data "be identities". One question though: how do we know that something 'is an identity' ? From the source code, it is straightforward. But internally in Agda, what is "is an identity" ?
from agda-categories.
It's important to remember that I'm partly teaching myself category theory [the subtler points thereof] and constructive type theory while doing this. (...) And indeed, choosing to use
≡
might simply have been a misguided choice. But I learned stuff by trying to push this through!
Oh, well that sounds like an excellent project! I taught myself Agda by mechanizing type system proofs, and I learned a lot about both in the process. Ever since then, I feel I don't really understand a proof unless I mechanized it (irrespective of whether it's my own proof or someone else's). When it comes to category theory, I'm largely self-taught as well, so I'm grateful to you and @HuStmpHrrr that there's now an Agda library that allows me to explore CT in more detail and play around with them.
BTW, have you considered collecting your insights and experiences and publish them somewhere? I would be very interested to hear what you've learned. And in general, it would be nice to have some pedagogical resources for people with a programming/types background that are interested in category theory and vice-versa. And I don't mean people who want to use categories for programming — there's plenty of resources for that — I mean resources for understanding CT and TT foundations.
Yes, traditional CT does assume an extensional meta-logic. Here, in Agda, it is interesting to see exactly when that comes in. In the old library, some of that was swept under the carpet by using irrelevance, which is definitely where some things break down.
I totally agree. And one of the things I particularly like about this library is that it does not use "clever tricks" or fancy language features to cut corners. I'm really interested to see how much of "vanilla" category theory can actually be mechanized constructively, in "vanilla" MLTT, in practice.
One question though: how do we know that something 'is an identity' ? From the source code, it is straightforward. But internally in Agda, what is "is an identity" ?
I'm not sure I understand the question. What do you mean by 'internally in Agda'?
What I have in mind is that the precise meaning of 'identity' (and thus of 'strict') will depend on the context, i.e. the categories involved. Since categories already carry around a (local) notion of identity, that should be the thing that tells us what the right notion of strictness is.
I realize this is rather vague. I'm thinking of this as a guiding principle, rather than a general recipe. Maybe it would help to work out a few examples?
from agda-categories.
Yes, we're definitely planning to write up what we've learned. Outline is ready.
Re: identity - yes, I definitely think some examples would help. The notion of 'strict' in MLTT is still fuzzy for me. There are clearly some things that are strict already implemented; the accompanying functors have idf
and (generally) refl
or other 'free' proof obligations, or the accompanying natural transformations have id
arrows uniformly. But that's kind of a meta-theoretic observation.
from agda-categories.
There's been a lot of discussion on this issue, but I'm still not entirely sure what to try next. There are intriguing ideas above, but rereading it all, I don't quite know what to try.
I would still be curious to see how far one can push things through via using ≡
as the equality, but of course in a setting with K as well. But this may well be doomed - so if someone can enlighten me as to that, I would most appreciate it!
from agda-categories.
First, a question. I'm still confused in what sense using one equality or the other determines whether a categorical structure is strict or weak (in the category-theoretical sense).
Concepts I would consider strict:
- the category Cat (as in
Instance.StrictCats
), - enriched categories (e.g.
Category
and2-Category
in this library), - functor equality (
Functor.Equivalence
in this library).
Concepts I would consider weak/non-strict:
- the category Ho(Cat) (as in
Instance.Cats
), - bicategories and weakly enriched categories (e.g.
Bicategory.Instance.Cats
) - natural isomorphism.
I fail to see how this relates to choosing ≡
as the equality on morphisms. With the exception of functor equality, none of these even involve ≡
in the current library. So what's the connection?
I would still be curious to see how far one can push things through via using
≡
as the equality, but of course in a setting with K as well. But this may well be doomed - so if someone can enlighten me as to that, I would most appreciate it!
I think problems would mostly crop up in instances and constructions. For example:
- working with quotients, e.g. proving
Sets
is (finitely) cocomplete/has equalizers/pushouts; - working with structures that have "proof-irrelevant" parts and/or are equal up-to some (proof-irrelevant) equivalence, e.g. the category of binary relations (
≡
is too strict an equality), spans, etc. — this is obviously related to the previous point; - working with extensional equality, e.g. proving
Sets
is cartesian closed.
Though I have not checked any of these, so there might be something I'm missing.
from agda-categories.
To clarify, my question/confusion is ultimately about the title of this issue: "Strict Category Theory". Maybe you just mean something different by "strict".
If that's the case, then maybe I should open a separate issue that is about how to organize strict vs. weak constructions (in the categeorical sense), which is what I thought this issue was about.
from agda-categories.
More relevant discussion at #44 and #58.
from agda-categories.
So I think it might be time to revisit this. What is quite clear is that the word 'strict' is used for a lot of different things in CT, and should not all be lumped together. So this 'issue' really ought to be several issues, with this one closed as obsolete/confused. I then think every one of the separate issues can be tackled separately.
The reason I'm not just doing that myself, is that I need some help to figure out what are the separate issues involved!
from agda-categories.
And now I am closing it, but I left a link on the projects page.
from agda-categories.
Related Issues (20)
- Discrepancy of `unique` of `Product` and `unique` of `IsPullback` HOT 1
- Spelling mistake in Categories.Morphism.HeterogeneousIdentity HOT 1
- Suggested improvements for `IsPullback` HOT 1
- Bicategory terminology HOT 4
- Field names for RegularEpi/RegularMono are nondescriptive HOT 6
- Move Everything.agda to src. HOT 10
- Naming of fields in CartesianClosed Functor HOT 2
- Maybe the Hom version of Adjunction can be fully polymorphic? HOT 1
- Pull out adjunction between products and exponentials HOT 1
- Move Categories.Category.Diagram.Span to Categories.Diagram.Span
- Remove Categories.Category.Equivalence HOT 1
- `!-unique₂` takes implicit args in `Terminal`, whereas it takes explicit ones in `Initial` HOT 1
- ramp up stdlib version? HOT 14
- Caching on CI seems to be broken HOT 12
- NaturalNumber -> NNO? HOT 1
- Trivial solution set for Adjoint functor theorem HOT 8
- Yoneda is broken HOT 6
- Big dagger-category to-do list
- Support stdlib 2.0 HOT 4
- agda-categories should list compatibility versions on README HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from agda-categories.