Zulip Chat Archive

Stream: maths

Topic: yoneda


view this post on Zulip Johan Commelin (Oct 18 2018 at 10:41):

@Scott Morrison Is there a reason why yoneda takes the category as explicit argument? Now we have to write yoneda C X instead of just yoneda X.

view this post on Zulip Scott Morrison (Oct 18 2018 at 14:38):

Try it: you still wouldn't be able to write yoneda X. The problem is that yoneda C X has a coercion, converting it to (yoneda C).obj X, and the coercion mechanism isn't clever enough to handle yoneda X by filling in C as an implicit argument before using the coercion.

view this post on Zulip Reid Barton (Oct 18 2018 at 14:41):

I guess yoneda.obj X would work then, if the category argument was implicit?

view this post on Zulip Reid Barton (Oct 18 2018 at 14:44):

This coercion stuff has turned out to be a lot more frustrating than expected--it's lovely when it works but Lean's reluctance to use coercions in the presence of metavariables means that they're often a lot more awkward than just writing F.obj X, but then you have the burden of supporting both F X and F.obj X which are different expressions.

view this post on Zulip Johan Commelin (Oct 18 2018 at 14:44):

"and the coercion mechanism isn't clever enough" :sad:

view this post on Zulip Johan Commelin (Oct 18 2018 at 14:45):

I guess this is why Scott didn't use any coercions a couple of months ago...

view this post on Zulip Reid Barton (Oct 18 2018 at 14:46):

If F X and F.obj X were the same expression, one could forgive the elaborator for being picky about where it is willing to insert a coercion

view this post on Zulip Reid Barton (Oct 18 2018 at 14:48):

I think this thing with yoneda C is the same issue I ran into whenever I had to deal with cylinders in my homotopy theory library. There I had a functor I:CCI : C \to C which was attached to CC by a type class, but I think that detail doesn't matter.

view this post on Zulip Johan Commelin (Oct 18 2018 at 14:48):

Could we choose a fancy bracket that looks like ( and ), and turn that into notation for has_apply?

view this post on Zulip Reid Barton (Oct 18 2018 at 14:49):

And then I also had natural transformations i0i_0, i1:idIi_1 : \mathrm{id} \to I, p:Iidp : I \to \mathrm{id}, v:IIv : I \to I, all of which had the same issue...

view this post on Zulip Johan Commelin (Oct 18 2018 at 14:50):

I think wouldn't mind write F(X) with some fancy (). But maybe this is abusing notation and type classes too much.

view this post on Zulip Johan Commelin (Oct 18 2018 at 14:50):

I think this could then replace coe_to_fun.

view this post on Zulip Reid Barton (Oct 18 2018 at 14:52):

It's not clear to me that we would not just end up back in the same situation

view this post on Zulip Reid Barton (Oct 18 2018 at 14:53):

We would still have two things, F.obj X and apply F X. I guess the question is whether we could avoid ever having to write F.obj X. But it would be so much simpler if there was just one thing in the first place.

view this post on Zulip Johan Commelin (Oct 18 2018 at 14:55):

apply F X would be F.obj X by definition.

view this post on Zulip Reid Barton (Oct 18 2018 at 14:55):

It's possible if I had built my homotopy theory library on top of a category theory version with coercions from the start, I could have found a more convenient way to set things up

view this post on Zulip Reid Barton (Oct 18 2018 at 14:56):

But "by definition" is not good enough for simp, rw etc.

view this post on Zulip Reid Barton (Oct 18 2018 at 14:56):

I had a hard time porting a lot of proofs over the transition to use coercions in category theory

view this post on Zulip Reid Barton (Oct 18 2018 at 14:56):

because I had to be careful about the difference between F X and F.obj X

view this post on Zulip Reid Barton (Oct 18 2018 at 14:57):

If I could actually write F X consistently then that might be okay, but I couldn't because of the issues with coercions and metavariables

view this post on Zulip Reid Barton (Oct 18 2018 at 14:58):

In the end I think I wrote some explicit type ascriptions in the statements of the simp lemmas I had defined, so that they could work on the F X version

view this post on Zulip Scott Morrison (Oct 18 2018 at 14:58):

If we can agree that the coercion mechanism is broken, I would very happily rip them back out of the category_theory/.

view this post on Zulip Reid Barton (Oct 18 2018 at 14:59):

For example https://github.com/rwbarton/lean-homotopy-theory/commit/e98dd6f51cd46653bf30c610e60573318443466c#diff-6931c0d6d9d8dda133a6b3ed34b290d5L548

view this post on Zulip Scott Morrison (Oct 18 2018 at 14:59):

The saving of not having to write .obj most of the time is far outweighed by the confusion of sometimes mysteriously having to do so.

view this post on Zulip Reid Barton (Oct 18 2018 at 14:59):

https://github.com/rwbarton/lean-homotopy-theory/commit/e98dd6f51cd46653bf30c610e60573318443466c#diff-f49cdebfeaf5ac27e5bea99a12ad4ca9L129 -- sometimes I needed to help Lean out with the types and other times I didn't; it was hard to predict

view this post on Zulip Scott Morrison (Oct 18 2018 at 15:01):

There's also the issue of why category_theory/ requires so much use of erw rather than rw. This stinks, and I don't have a clear idea of why it happens, but fear that coercions are sometimes to blame.

view this post on Zulip Reid Barton (Oct 18 2018 at 15:02):

I changed a bunch of rw to erw in that commit too, precisely because of the coercion thing. But there are some other situations where you need erw as well.

view this post on Zulip Scott Morrison (Oct 18 2018 at 15:03):

Do you think you can explain any of the others? I unfortunately just try erw and get on with it, and haven't invested the time in seeing what was going wrong.

view this post on Zulip Reid Barton (Oct 18 2018 at 15:05):

I suspect that most of my cases are because I still use the explicit version (nat_trans.app in this case) in my definitions: https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.1/src/homotopy_theory/formal/cylinder/homotopy.lean#L17
and I frequently want to rewrite using the conditions Hi\0, Hi\1

view this post on Zulip Reid Barton (Oct 18 2018 at 15:06):

It was quite unclear to me at first whether the easiest way forward was to use coercions everywhere or to use coercions nowhere or something in between

view this post on Zulip Reid Barton (Oct 18 2018 at 15:07):

Oh you mean the other situations, not related to coercions.

view this post on Zulip Reid Barton (Oct 18 2018 at 15:08):

I think for me they come from things like: i0i_0 is a natural transformation idI\mathrm{id} \to I. So the naturality law for i0i_0 contains stuff like (functor.id C) X in the types and I need it to be X to continue with a subsequent rewrite, and that's why I need erw.

view this post on Zulip Reid Barton (Oct 18 2018 at 15:08):

I don't remember more details off-hand, sorry

view this post on Zulip Reid Barton (Oct 18 2018 at 15:09):

But I know that at least some cases had to do with this specific issue of applying the identity functor

view this post on Zulip Reid Barton (Oct 18 2018 at 15:10):

Like I might want to rewrite using associativity where I have three maps A -> B, B -> X, (functor.id C) X -> (functor.id C) Y

view this post on Zulip Reid Barton (Oct 18 2018 at 15:10):

and then rw says "nope"

view this post on Zulip Reid Barton (Oct 18 2018 at 15:12):

I guess my suggestion might be to rip out coercions for now and then suggest as a wishlist item for :four_leaf_clover: to replace has_coe_to_fun by what I was calling in Orsay "type-indexed notation"

view this post on Zulip Mario Carneiro (Oct 18 2018 at 15:12):

what is that?

view this post on Zulip Reid Barton (Oct 18 2018 at 15:13):

The idea is if F X was actually notation for F.obj X then coercion and non-coercion syntax could all live happily forever.

view this post on Zulip Reid Barton (Oct 18 2018 at 15:13):

Currently, when Lean tries to elaborate F X it sees that the type of F is not a Pi type and then it maybe inserts a coercion

view this post on Zulip Reid Barton (Oct 18 2018 at 15:13):

So I presume this involves reducing the type of F to WHNF at least?

view this post on Zulip Reid Barton (Oct 18 2018 at 15:14):

Then the idea is, allow the user to specify another interpretation of F X as notation which depends on the head of the type of F, or something like that.

view this post on Zulip Reid Barton (Oct 18 2018 at 15:15):

rather than the rule being "if the type of F is a Pi type then produce an application F X, otherwise produce coe_fun_t F X" or whatever it is today

view this post on Zulip Reid Barton (Oct 18 2018 at 15:15):

give the user the chance to add additional rules "if the type of F looks like [...], then produce [...]"

view this post on Zulip Reid Barton (Oct 18 2018 at 15:16):

In this case, functor.obj F X

view this post on Zulip Reid Barton (Oct 18 2018 at 15:22):

By the way, the equiv coercion to fun is another one which has given me a lot of problems, which again is annoying because there are simp rules written in terms of the coercion like e.symm (e x) = x

view this post on Zulip Reid Barton (Oct 18 2018 at 15:25):

I guess the usability of these coercions depends upon the usage patterns. Once the equivs you are working with are not ones which were passed as arguments to your lemma, but things like the equivalence Hom(FX, Y) = Hom(X, GY) induced by an adjunction, then I guess more of these metavariables crop up

view this post on Zulip Mario Carneiro (Oct 18 2018 at 15:27):

I think this can be solved by a simp lemma like e.to_fun = \u e and e.inv_fun = \u e.symm

view this post on Zulip Reid Barton (Oct 18 2018 at 15:30):

Yes, probably; then the next problem is that I might want to define my own simp lemmas whose statements involve applying equivs as functions

view this post on Zulip Reid Barton (Oct 18 2018 at 15:30):

and then I don't know how to write the statement of the lemma in simp normal form except by writing some bulky type ascriptions

view this post on Zulip Mario Carneiro (Oct 18 2018 at 15:31):

I have found that coercions between different function(like) types is a bad idea for this reason

view this post on Zulip Reid Barton (Oct 18 2018 at 15:47):

By the way, when bumping dependencies of your project across a substantial change, I can highly recommend having a separate checkout of the project built against the old version of the deps so that you can figure out how the heck any of your proofs used to work :smile:

view this post on Zulip Mario Carneiro (Oct 18 2018 at 15:57):

ah, that brings me back to metamath days

view this post on Zulip Johan Commelin (Oct 19 2018 at 11:41):

On the topic of coercions in category theory: would it make sense to use coercions to turn specialised shapes (like fork and square and fan) into the general shape cone? Of course we should also prove that have limits means having equalizers, pullbacks, products, etc... Then we might be able to prove a lot of stuff about general limits and use those results on specialised shapes. Or is this wishful thinking?

view this post on Zulip Johan Commelin (Oct 19 2018 at 11:49):

@Reid Barton I really like your idea about type indexed notation! Because then we could also have very clean notation for applying a functor to a morphism.

view this post on Zulip Reid Barton (Oct 19 2018 at 12:53):

Yes, I was just thinking of that as well--it would be nice to have both F X for F.obj X and F f for F.map f. I'm not sure that comes for free with the exact setup I had in mind, where the interpretation of juxtaposition depends only on the type of F, but maybe some slightly different design could handle it.

view this post on Zulip Reid Barton (Oct 19 2018 at 12:59):

I think we may indeed want to arrange things so that equalizers and so on are actually defined as special cases of limits, and then wrap that in a nicer interface (which doesn't involve manually constructing a diagram/functor). The body of facts we have about limits is just going to keep increasing, and duplicating the results for each special shape of limit doesn't make sense.

view this post on Zulip Johan Commelin (Oct 19 2018 at 13:18):

You say "actually defined as". Do you mean defeq? I was suggesting a coercion. But maybe that is not good enough.

view this post on Zulip Johan Commelin (Oct 19 2018 at 13:19):

I do think that these are issues that should be sorted out soon. Because otherwise the refactoring will become a big pain if there is already too much code depending on the current setup.

view this post on Zulip Johan Commelin (Oct 19 2018 at 13:52):

@Reid Barton I suppose the parser could also look at the "token" just following F to see whether it is an object or a hom. (And I assume the parser is smart enough to guess the right "token".)

view this post on Zulip Reid Barton (Oct 19 2018 at 13:53):

I meant defeq but I haven't thought that much about what exact condition we would want.
Here is an example statement: if I have a limit cone in a diagram category then evaluation on any object yields a limit cone. Now we want the same statement for equalizers. If equalizers are defeq to a special case of limits, then we just apply the original statement. If equalizers are only equiv to a special shape of limit, then we need to transport across the equiv on both sides.

view this post on Zulip Johan Commelin (Oct 19 2018 at 13:54):

So all the current machinery should be replaced by constructors yielding a nice API?

view this post on Zulip Johan Commelin (Oct 19 2018 at 13:56):

It's really weird that these definitions are so non-trivial. Why are we so good at unifying concepts, and why can't we teach that trick to a computer?

view this post on Zulip Scott Morrison (Oct 19 2018 at 16:01):

I’d love to be able to do something like this, but at the moment I really don’t see a good option. We can work on constructing diagrams (with some help from tactics) more easily. As an example, if X Y : C, and f g : X \hom Y, there’s no reason why construct_diagram [f,g] couldn’t return a \Sigma (J : Type) [category J], J \func C, automatically deciding the index category J should be the walking parallel pair.

view this post on Zulip Scott Morrison (Oct 19 2018 at 16:02):

If this becomes easy enough, it becomes plausible to start defining “special” limits in terms of general ones. But without a huge improvement in this direction, it’s way too painful to expect a user to talk about equalizers as (defeq) special cases of limits. Just see the hoops I had to jump through to prove that having limits implies having equalizers...

view this post on Zulip Scott Morrison (Oct 19 2018 at 16:05):

Also, @Johan Commelin, I’m not sure if you saw it already, but there’s a second pull request (from the limits-constructions branch) that constructs products and equalizers from limits, etc.

view this post on Zulip Johan Commelin (Oct 19 2018 at 16:05):

I haven't yet looked in detail.

view this post on Zulip Johan Commelin (Oct 19 2018 at 16:12):

I really hope that I will be able to write down a definition of sieve without @s. I must say that my experience with your library has been very positive. Writing things down is really pain-free and automation takes care of a lot of troubles.
Do you have a general guideline for when to add an auto_param in a definition?

view this post on Zulip Reid Barton (Oct 19 2018 at 16:25):

Couldn't we have a function construct_equalizer_diagram {a b} (f g : a \hom b) : walking_fork \func C, and then define equalizer f g := limit (construct_equalizer_diagram f g)?

view this post on Zulip Johan Commelin (Oct 19 2018 at 17:24):

I like this idea. @Scott Morrison , did you try something like this before you settled on the current approach? Do you see problems with it?

view this post on Zulip Reid Barton (Oct 19 2018 at 17:35):

But without a huge improvement in this direction, it’s way too painful to expect a user to talk about equalizers as (defeq) special cases of limits. Just see the hoops I had to jump through to prove that having limits implies having equalizers...

I agree that it is more work starting from scratch to set up the basic definitions of things like equalizers as special cases of limits, but now that you have already jumped through those particular hoops, why would a user also need to?

view this post on Zulip Scott Morrison (Oct 19 2018 at 17:40):

I guess the problem with equalizer f g := limit (construct_equalizer_diagram f g) is that then the user of equalizers has to know the names of the objects and morphisms in the walking_fork. (Separately, I think walking_fork is the wrong name here; the "handle" of the fork is missing at this point.)

view this post on Zulip Scott Morrison (Oct 19 2018 at 17:40):

Maybe this is a small cost.

view this post on Zulip Scott Morrison (Oct 19 2018 at 17:41):

What should the objects and morphisms be?

view this post on Zulip Scott Morrison (Oct 19 2018 at 17:43):

I guess I'm really not seeing where there would be a simplification of the code, however.

view this post on Zulip Johan Commelin (Oct 19 2018 at 17:44):

The simplification would come later, right? For example you have a massive file about deriving products and equalizers from limits. That would simplify.

view this post on Zulip Johan Commelin (Oct 19 2018 at 17:44):

And functors preserving limits and such.

view this post on Zulip Scott Morrison (Oct 19 2018 at 17:44):

Still for any theorem about limits, you need to restate a special version of it for equalizers/products/etc. None of these things require humans to write the proofs at this point.

view this post on Zulip Johan Commelin (Oct 19 2018 at 17:45):

Sorry, maybe I'm dense, but what exactly do you mean?

view this post on Zulip Scott Morrison (Oct 19 2018 at 17:45):

Okay, I agree the files that construct equalizers, products, etc from limits would essentially disappear.

view this post on Zulip Scott Morrison (Oct 19 2018 at 17:46):

Let's think about the construction
def pi.post (f : β → C) (G : C ⥤ D) : G (limits.pi f) ⟶ (limits.pi (G.obj ∘ f)) := ...

view this post on Zulip Reid Barton (Oct 19 2018 at 17:47):

pi = product of an arbitrary family?

view this post on Zulip Scott Morrison (Oct 19 2018 at 17:47):

if limits.pi f is defined as limit (functor.of_function f)

view this post on Zulip Scott Morrison (Oct 19 2018 at 17:47):

Yes.

view this post on Zulip Scott Morrison (Oct 19 2018 at 17:49):

hmm... okay, maybe you guys are right here. :-)

view this post on Zulip Johan Commelin (Oct 19 2018 at 17:49):

Wouldn't you just prove this by limit.post...?

view this post on Zulip Johan Commelin (Oct 19 2018 at 17:50):

Oohh, I really don't know. You guys have written orders of magnitude more code then I have. I'm just a user...

view this post on Zulip Scott Morrison (Oct 19 2018 at 17:50):

So... for now I agree that this is worth exploring.

view this post on Zulip Scott Morrison (Oct 19 2018 at 17:51):

However, I'm hoping to pause for a while on Lean, in not too long, as I have a lot of maths I want to work on.

view this post on Zulip Scott Morrison (Oct 19 2018 at 17:51):

So I'm not sure what to do with this PR in the meantime.

view this post on Zulip Scott Morrison (Oct 19 2018 at 17:51):

Options:

view this post on Zulip Scott Morrison (Oct 19 2018 at 17:51):

1. leave it open for others to modify

view this post on Zulip Scott Morrison (Oct 19 2018 at 17:52):

2. close it for now

view this post on Zulip Reid Barton (Oct 19 2018 at 17:52):

I'm not sure exactly where that "..." was going, but another example to keep in mind is "if D is a complete category then a cone in D^J is a limit cone iff each the value at each j in J is a limit cone"

view this post on Zulip Scott Morrison (Oct 19 2018 at 17:52):

3. strip it down to just limits, not the special cases, and leave those for later

view this post on Zulip Reid Barton (Oct 19 2018 at 17:52):

I have been meaning to suggest that 3 is a good idea anyways

view this post on Zulip Reid Barton (Oct 19 2018 at 17:54):

Because the PR involves a lot of relatively untested design, and I think it's worth it to go and try to prove loads of things about general limits to "kick the tires" and make sure we settle on a design that we want

view this post on Zulip Scott Morrison (Oct 19 2018 at 17:54):

Okay. I will strip it down. Maybe someone else can explore if the special cases defined as suggested above are usable.

view this post on Zulip Johan Commelin (Oct 19 2018 at 17:56):

@Reid Barton How hard would it be to test that on your homotopy lib?

view this post on Zulip Johan Commelin (Oct 19 2018 at 17:57):

Or should we try this on a fork of Scott's lib?

view this post on Zulip Reid Barton (Oct 19 2018 at 18:09):

Probably not that easy since I have some setup of my own to prove a bunch of lemmas about pushouts. Though maybe I could sorry all those proofs and just see how usable it is in the actual homotopy theory part.

view this post on Zulip Johan Commelin (Oct 19 2018 at 18:18):

Yeah, I meant that you just create a branch, and maybe break a couple files, but test this idea on the other files.

view this post on Zulip Johan Commelin (Oct 19 2018 at 18:19):

I'm not suggesting you uproot your master branch (-;

view this post on Zulip Scott Morrison (Oct 19 2018 at 22:06):

@Reid Barton, do you have ideas about how to define all the "walking" categories for limits of special shapes?

view this post on Zulip Scott Morrison (Oct 19 2018 at 22:06):

I have reduced my PR to just the plain limits.

view this post on Zulip David Michael Roberts (Oct 19 2018 at 23:59):

Just as we have finite sets, why not have a collection of finite categories of the usual special shapes?

view this post on Zulip Scott Morrison (Oct 20 2018 at 00:01):

Yes. The point is just to decide the names of the objects and morphisms, because these names will then be fixed forever, and part of the API.

view this post on Zulip Scott Morrison (Oct 20 2018 at 00:02):

Wouldn't you just prove this by limit.post...?

I've just been trying this, and quickly discovered the reason: limit.post assumes that you're in a complete category. However pi.post only assumes you have all products. Therefore you can't call limit.post from pi.post, and we're stuck proving it again.

view this post on Zulip Scott Morrison (Oct 20 2018 at 00:03):

Maybe this is a sign that pi.post is not what we want to provide people anyway.

view this post on Zulip Scott Morrison (Oct 20 2018 at 00:04):

Except ... that it is...

view this post on Zulip Scott Morrison (Oct 20 2018 at 00:04):

Maybe I will finish off "porting" products to the new setup, and then you guys can have a look to see what can be reduced.

view this post on Zulip Scott Morrison (Oct 20 2018 at 00:05):

I'll do products because there no walking categories are required, we just use functor.of_function.

view this post on Zulip Reid Barton (Oct 20 2018 at 00:07):

We probably need things like [has_limits_of_shape J] for other purposes anyways

view this post on Zulip Reid Barton (Oct 20 2018 at 00:08):

e.g. κ\kappa-accessible categories have all κ\kappa-filtered colimits

view this post on Zulip Reid Barton (Oct 20 2018 at 00:08):

("We" = "I", perhaps)

view this post on Zulip Reid Barton (Oct 20 2018 at 00:09):

Similarly we want to talk about functors which preserve finite products or whatever

view this post on Zulip Reid Barton (Oct 20 2018 at 00:11):

or filtered colimits, etc. This seems to me like more evidence that we need to be able to represent special shapes of (co)limits as special cases of general (co)limits so that we can flexibly mix all these notions, though certainly I have not yet tried to construct a specific design for any of this

view this post on Zulip Scott Morrison (Oct 20 2018 at 00:18):

Could we try something like... has_limits_of {A : Type} (Q : A \to \Sigma (J : Type), J \func C)

view this post on Zulip Scott Morrison (Oct 20 2018 at 00:20):

has_limits itself could be defined as has_limits_of id

view this post on Zulip Scott Morrison (Oct 20 2018 at 00:21):

has_products could be defined as has_limits_of A Q with A = \Sigma (b : Type), b \to C, and Q = \lambda p, p.1, functor.of_function p.2.

view this post on Zulip Reid Barton (Oct 20 2018 at 00:21):

That's super general but I think even that level of generality could be useful in specific circumstances.

view this post on Zulip Scott Morrison (Oct 20 2018 at 00:22):

Maybe there's no need to specify the allowed functors?

view this post on Zulip Scott Morrison (Oct 20 2018 at 00:22):

Just the allowed diagrams?

view this post on Zulip Reid Barton (Oct 20 2018 at 00:22):

For example cofibration categories or Waldhausen categories have an axiom which says that you can form a pushout if one of the legs is a cofibration (one of the bits of structure)

view this post on Zulip Scott Morrison (Oct 20 2018 at 00:22):

I see.

view this post on Zulip Reid Barton (Oct 20 2018 at 00:23):

I just hand-crafted this axiom in my project: https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.1/src/homotopy_theory/formal/cofibrations/precofibration_category.lean#L41

view this post on Zulip Reid Barton (Oct 20 2018 at 00:24):

So I know this example off-hand because I already implemented it in Lean. I think this is a pretty rare scenario, but if doesn't make things too much more complicated...? Certainly the common case would be A = (J \func C), or Sigma of that over all J of some form (e.g., J filtered)

view this post on Zulip Reid Barton (Oct 20 2018 at 00:27):

i.e., stick has_limits_of_shape J as a specialization of has_limits_of and a generalization of has_products

view this post on Zulip Scott Morrison (Oct 20 2018 at 00:38):

well, maybe even one more step: has_limits_of, allowing you to specify arbitrary diagrams and arbitrary functors out of those, then has_limits_of_shapes allowing you to specify a class of diagrams, but all functors out of them, then has_limits_of_shape for a single diagram, and then has_binary_products would be a specialisation of that.

view this post on Zulip Scott Morrison (Oct 20 2018 at 00:38):

in any case, I'll give this a go, I guess.

view this post on Zulip Reid Barton (Oct 20 2018 at 00:38):

Sounds great!

view this post on Zulip Reid Barton (Oct 20 2018 at 00:41):

I should really finish up that Grand Plan for formalizing model categories that I started writing a while ago...

view this post on Zulip Johan Commelin (Oct 20 2018 at 04:01):

While we are at it: Do people have strong opinions on whether the homs of a category live in Type v or Sort v? I think if we start doing all sorts of diagrams over preorders (or using preorders as categories in other places) it might help in manipulating the homs if they are just in Prop instead of the whole ulift plift dance.
@Scott Morrison Let me stress that I really love what you've done so far :thank_you:. The only reason that I have these questions is because your code is so good :thumbs_up: that I can't resist using it :stuck_out_tongue_wink:

view this post on Zulip Scott Morrison (Oct 20 2018 at 05:07):

I've tried this before, but it's not possible to use Sort v. Unfortunately at the moment I can't remember why... From memory if you just start at the top and switch it over you run into difficulties quite quickly, if you want to try it yourself. :-)

view this post on Zulip David Michael Roberts (Oct 20 2018 at 06:41):

For example cofibration categories or Waldhausen categories have an axiom which says that you can form a pushout if one of the legs is a cofibration (one of the bits of structure)

Dually, there are many cases where one has a class of morphisms of which pullbacks along arbitrary maps exist (eg submersions, in smooth manifolds)

view this post on Zulip Johan Commelin (Oct 20 2018 at 07:20):

Right. At some point we want to formalise this list: https://stacks.math.columbia.edu/tag/02WE

view this post on Zulip David Michael Roberts (Oct 20 2018 at 07:41):

Well, span and cospan are obvious choices, as is parallel_pair. Then also for each finite set one should have the corresponding discrete category, so as to form products/coproduct. The empty category should be there too, to get terminal/initial objects.

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:42):

No, I want to know what the _objects_ and _morphisms_ inside, for example parallel_pair should be called.

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:43):

Should the objects be source and target, and the morphisms left and right?

view this post on Zulip Reid Barton (Oct 20 2018 at 15:43):

Yeah that's a tough one. top_arrow?

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:43):

Or should parallel_pair := bool??

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:43):

I like 0 and 1 for the objects

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:43):

As in def parallel_pair := fin 2?

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:44):

Or

inductive parallel_pair | _0 | _1

??

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:44):

probably not literally

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:44):

like the second

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:44):

I just mean as names

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:45):

okay, that's what I've done previously. Is there something better that _0 and _1 for the names?

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:45):

0 and 1 are achievable

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:45):

Oh, how?

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:45):

add an instance

view this post on Zulip Reid Barton (Oct 20 2018 at 15:45):

has_zero has_one

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:46):

ah, I see.

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:46):

Isn't it just more confusing to have an inductive type with terms _0, _1, but then give them second names via instances?

view this post on Zulip Reid Barton (Oct 20 2018 at 15:46):

Probably

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:47):

I would call them zero and one

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:47):

and then use 0 and 1 as notation

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:47):

we do that for nat, it's not that confusing

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:47):

okay... And using 0 and 1 as notation via has_zero and has_one will work in pattern matching, etc, just like for nat.

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:47):

Sounds reasonable.

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:47):

On to the morphisms, then. :-)

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:48):

yeah...

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:48):

And the names of objects in pullbacks and pushouts...

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:48):

no bright ideas there. left and right seem reasonable?

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:49):

Except that there's no sense in which the two are actually different...

view this post on Zulip Reid Barton (Oct 20 2018 at 15:49):

surely they're top and bottom?

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:49):

I don't think left and right imply any other difference

view this post on Zulip Reid Barton (Oct 20 2018 at 15:49):

Which way do you draw your equalizers??

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:50):

Yeah, there's that too. top and bottom are probably better.

view this post on Zulip Reid Barton (Oct 20 2018 at 15:50):

(but maybe top and bottom have too many other connotations, with ordering?)

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:50):

I know, it's bugging me that the walking pair is always drawn with the arrows above each other

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:51):

oh -- and if walking_pair is the diagram for an equalizer, what is the diagram for a binary product?

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:51):

but I think that the analogy to posets is important, that's why 0 and 1 are useful

view this post on Zulip Reid Barton (Oct 20 2018 at 15:51):

I was going to bring up binary things next.

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:51):

which one is that?

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:51):

A > B < C?

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:52):

binary product is just the diagram with two objects, no arrows at all

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:52):

left and right, definitely

view this post on Zulip Reid Barton (Oct 20 2018 at 15:52):

In my homotopy theory library I used the convention of naming things like the inclusions of a coproduct with \_0 and \_1, and eventually I got annoyed that I hadn't chosen \_1 and \_2, but it would be a lot of things to change.

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:52):

... I'd been tempted to call that the walking_pair, and the diagram for an equalizer the walking_parallel_pair, but that is contrary to usual usage, I think.

view this post on Zulip Reid Barton (Oct 20 2018 at 15:53):

I assume you're going to define it as discrete of some type?

view this post on Zulip Reid Barton (Oct 20 2018 at 15:53):

The reason is that \_1 and \_2 aligns better with Lean's builtin p.1 and p.2

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:53):

Okay, yeah, I guess that is best, so it's defeq a special case of arbitrarily indexed products.

view this post on Zulip Reid Barton (Oct 20 2018 at 15:54):

Yes, and it should also just be less work overall

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:54):

So is the indexing category for binary_product discrete (fin 2), discrete bool or discrete side, where side is an inductive type with terms left and right?

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:54):

I maybe prefer the last?

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:55):

I think I do too

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:55):

or something with terms fst and snd?

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:55):

That fits better with the naming of projection maps in Lean itself.

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:55):

the problem with that is they aren't maps

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:56):

I would get the two confused

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:56):

yes, but we'll be able to write things like c.\pi fst for the first projection

view this post on Zulip Reid Barton (Oct 20 2018 at 15:56):

left and right are nice for inl and inr though

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:56):

is it the same category being reused?

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:57):

I don't see why not.

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:57):

ok, then I agree with Reid

view this post on Zulip Reid Barton (Oct 20 2018 at 15:57):

Probably it should be... so that we can relate coproducts in C to products in C^op eventually

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:57):

although I guess technically one is the op of the other

view this post on Zulip Reid Barton (Oct 20 2018 at 15:58):

Yes, technically it should be the op

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:58):

Great, I will use side with left and right.

view this post on Zulip Reid Barton (Oct 20 2018 at 15:58):

but we're already writing the category as discrete T where T is the type of its objects

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:58):

Finally, pullbacks and pushouts

view this post on Zulip Mario Carneiro (Oct 20 2018 at 15:59):

Can we steal the same names?

view this post on Zulip Scott Morrison (Oct 20 2018 at 15:59):

it would be nice here if everything is consistent...

view this post on Zulip Reid Barton (Oct 20 2018 at 15:59):

middle??

view this post on Zulip Reid Barton (Oct 20 2018 at 15:59):

Is anyone going to actually see these names?

view this post on Zulip Mario Carneiro (Oct 20 2018 at 16:00):

left - inl > 1 < inr - right

view this post on Zulip Mario Carneiro (Oct 20 2018 at 16:00):

left < fst - 0 - snd > right

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:02):

okay, sounds good to me

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:03):

except...

view this post on Zulip Reid Barton (Oct 20 2018 at 16:03):

I guess those names are technically accurate in some sense, though I find them really confusing

view this post on Zulip Reid Barton (Oct 20 2018 at 16:03):

like, you have fst and snd involved in the diagram for pushouts and vice versa

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:03):

remember the morphisms there are terms of one-element types

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:03):

maybe we should just make all those morphisms types punit.

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:04):

and not have names at all

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:04):

we just have to name the objects here, so we'd have inductive walking_pullback | left | right | one

view this post on Zulip Mario Carneiro (Oct 20 2018 at 16:04):

I don't think so... the type is a inductive family with two elements

view this post on Zulip Reid Barton (Oct 20 2018 at 16:04):

As they say, no names is good names

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:05):

why? we need to have a type of morphisms from left to one, and it contains only inl.

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:05):

etc

view this post on Zulip Reid Barton (Oct 20 2018 at 16:05):

It depends on whether you want to define hom as a single inductive family, or a type defined by case analysis

view this post on Zulip Mario Carneiro (Oct 20 2018 at 16:05):

I think types by case analysis is a bad idea

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:06):

remember hom : obj -> obj -> Type

view this post on Zulip Reid Barton (Oct 20 2018 at 16:06):

I agree it probably makes the finite amount of work it takes to set up these categories and describe functors from them larger

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:06):

maybe I'm confused here

view this post on Zulip Reid Barton (Oct 20 2018 at 16:07):

I don't know if it has any longer term consequences though

view this post on Zulip Mario Carneiro (Oct 20 2018 at 16:07):

inductive hom | inl : hom left 1 | inr : hom right 1

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:07):

I see

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:07):

okay, that does sound good

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:07):

but makes it harder to name things. :-)

view this post on Zulip Reid Barton (Oct 20 2018 at 16:08):

what about identities though? I think the truly correct way to do this is to go through the free graph construction

view this post on Zulip Reid Barton (Oct 20 2018 at 16:08):

Er, free category on a graph construction

view this post on Zulip Mario Carneiro (Oct 20 2018 at 16:08):

I was just about to say the same

view this post on Zulip Mario Carneiro (Oct 20 2018 at 16:08):

this is a graph, not a cat

view this post on Zulip Reid Barton (Oct 20 2018 at 16:08):

which I do have written down somewhere

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:09):

yes... I have this as well. It is extraordinarily painful to use, and this is why I hadn't previously pursued this approach.

view this post on Zulip Reid Barton (Oct 20 2018 at 16:09):

but I'm still not sure whether it makes any difference once we're done defining all these little categories

view this post on Zulip Mario Carneiro (Oct 20 2018 at 16:09):

really? I wouldn't have expected that

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:09):

but Reid, isn't your point that "all these little categories" is not a fixed set?

view this post on Zulip Reid Barton (Oct 20 2018 at 16:09):

Specifically, it should be easy enough to change our mind about the definitions of these categories later, right?
As long as we have a usable interface for building functors out of them

view this post on Zulip Reid Barton (Oct 20 2018 at 16:11):

for example: there is some category called parallel_pair, and to define a functor parallel_pair \func C I have to give you two objects (a b : C) and two maps (f g : a \hom b)

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:11):

yes

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:11):

my preference would be on the first cut to define the slightly larger indexed inductive types for morphisms that include identity morphisms.

view this post on Zulip Reid Barton (Oct 20 2018 at 16:11):

and then... there is some extensionality rule or something... and then it doesn't matter what goes inside. Right?
And nobody really needs to care about the choices of names, since I just renamed everything a b f g anyways

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:12):

and only later to pursue defining these as path categories on graphs (because I don't know how to do this well)

view this post on Zulip Reid Barton (Oct 20 2018 at 16:12):

As long as we can maintain this interface, it shouldn't matter whether we use the free category on a graph, or define hom as an indexed inductive type, or define hom by case analysis

view this post on Zulip Reid Barton (Oct 20 2018 at 16:13):

or define the category as a poset if it happens to be one

view this post on Zulip Scott Morrison (Oct 20 2018 at 16:13):

I can't see to find my previous attempt to construct equalizers, based on a free category, out of limits, which was so unpleasant...

view this post on Zulip Reid Barton (Oct 20 2018 at 16:14):

I admit I never actually used my free category construction to do anything. I was going to use it to prove that Cat has coequalizers... but I didn't.

view this post on Zulip Mario Carneiro (Oct 20 2018 at 16:15):

Oh hey, are graphs an example of has_hom?

view this post on Zulip Reid Barton (Oct 20 2018 at 16:15):

That depends on what has_hom means exactly--this example was in the back of my mind when commenting on that aspect of Simon's PR

view this post on Zulip Mario Carneiro (Oct 20 2018 at 16:16):

assuming categories extend it, it must mean the notation, with hom and objects

view this post on Zulip Reid Barton (Oct 20 2018 at 16:16):

I think Scott convinced me at one point that it was better to not build category on top of graph, but I don't remember why exactly... maybe if we rename graph to has_hom it is more palatable, haha

view this post on Zulip Mario Carneiro (Oct 20 2018 at 16:18):

I kind of want to reserve the name graph for small has_homs

view this post on Zulip Reid Barton (Oct 20 2018 at 16:19):

Mario I'm glad you agree--there's this discussion about what to rename has_hom to in Simon's PR, which is really "the data of a category without the laws"

view this post on Zulip Reid Barton (Oct 20 2018 at 16:19):

That would just be specializing the universe parameters of has_hom to be equal right?

view this post on Zulip Mario Carneiro (Oct 20 2018 at 16:20):

I think so? I'm not sure that's small enough. Maybe it doesn't make sense

view this post on Zulip Mario Carneiro (Oct 20 2018 at 16:21):

I want graph A : Type u when A : Type u

view this post on Zulip Mario Carneiro (Oct 20 2018 at 16:21):

but there's no way I'm going to get that

view this post on Zulip Reid Barton (Oct 20 2018 at 16:21):

A graph is a set of vertices, together with a set of edges from a to b for each a and b

view this post on Zulip Reid Barton (Oct 20 2018 at 16:21):

Well, if graph isn't allowed to have multiple edges...

view this post on Zulip Mario Carneiro (Oct 20 2018 at 16:22):

yeah, simple graphs solve the problem

view this post on Zulip Reid Barton (Oct 20 2018 at 16:22):

I guess actual graph theorists would call this a multigraph

view this post on Zulip Reid Barton (Oct 20 2018 at 16:24):

Anyways graphs would also be examples of has_hom in any case

view this post on Zulip Reid Barton (Oct 20 2018 at 16:25):

Anyways anyways, my overall claim is that these names don't really matter either, because people should only be using the interface like parallel_pair_functor f g.

view this post on Zulip Reid Barton (Oct 20 2018 at 16:30):

Maybe that means the things to do is to pick the variable names which appear in the interface (like f and g?) and then choose the names of generating morphisms based on them in some systematic way (like F and G?)

view this post on Zulip Reid Barton (Oct 20 2018 at 16:31):

or whatever naming convention seems least likely to collide with other relevant things, maybe F is a bad name

view this post on Zulip Kevin Buzzard (Oct 20 2018 at 17:51):

The reason is that \_1 and \_2 aligns better with Lean's builtin p.1 and p.2

I was surprised once when I realised that the builtin notation was not p.0 and p.1 but presumably could have been, given that Lean was written by CS people.

view this post on Zulip Scott Morrison (Oct 21 2018 at 05:02):

@Reid Barton, @Johan Commelin, I experimented with a new design for "special" shape limits. Now they are all defined as special cases of limits. If you want to have a quick look, see https://github.com/leanprover-community/mathlib/tree/limits-others-new/category_theory/limits.

view this post on Zulip Scott Morrison (Oct 21 2018 at 05:03):

I think it looks reasonable. I would like to try proving some things about limits in functor categories, and make sure they immediately imply the corresponding results about pullbacks/products/etc.

view this post on Zulip Scott Morrison (Oct 22 2018 at 23:13):

I'm going to make other fundamental changes, I think.

view this post on Zulip Scott Morrison (Oct 22 2018 at 23:14):

(deleted)

view this post on Zulip Scott Morrison (Oct 22 2018 at 23:15):

I'm going to change cone F at least so that it is an object, bundled with a natural transformation from the constant functor (with value that object) to F. I may go all the way and just define cone F as a special case of a comma category. That had, long ago, been my initial version of limits, but I was having too much trouble with it. Having learnt a few things, I think it's viable again, so will try again. :-)

view this post on Zulip Reid Barton (Oct 22 2018 at 23:19):

I wanted exactly this description in order to prove that right adjoints preserve limits

view this post on Zulip Johan Commelin (Oct 23 2018 at 06:42):

@Scott Morrison Cool! That sounds like a good generalisation.
Concretely, you had a definition of sheaves, and I have almost generalised it to arbitrary sites. The real test case is probably going to be sheafification, and more generally pushforward and pullbacks of sheaves (and the fact that those are adjoint).

view this post on Zulip Johan Commelin (Oct 23 2018 at 08:57):

@Scott Morrison How general are you planning to set up comma categories? Only slices over an object, or the general thing where you start with two functors?


Last updated: May 10 2021 at 08:14 UTC