yoneda

Stream: maths

[Johan Commelin]

@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.

[Scott Morrison]

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.

[Reid Barton]

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

[Reid Barton]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

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 : C \to C$ which was attached to $C$ by a type class, but I think that detail doesn't matter.

[Johan Commelin]

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

[Reid Barton]

And then I also had natural transformations $i_0$, $i_1 : \mathrm{id} \to I$, $p : I \to \mathrm{id}$, $v : I \to I$, all of which had the same issue...

[Johan Commelin]

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

[Johan Commelin]

I think this could then replace coe_to_fun.

[Reid Barton]

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

[Reid Barton]

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.

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Scott Morrison]

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

[Reid Barton]

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

[Scott Morrison]

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.

[Reid Barton]

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

[Scott Morrison]

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.

[Reid Barton]

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.

[Scott Morrison]

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.

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

I think for me they come from things like: $i_0$ is a natural transformation $\mathrm{id} \to I$. So the naturality law for $i_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.

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

and then rw says "nope"

[Reid Barton]

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"

[Mario Carneiro]

what is that?

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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.

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

In this case, functor.obj F X

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Reid Barton]

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:

[Mario Carneiro]

ah, that brings me back to metamath days

[Johan Commelin]

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?

[Johan Commelin]

@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.

[Reid Barton]

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.

[Reid Barton]

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.

[Johan Commelin]

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

[Johan Commelin]

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.

[Johan Commelin]

@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".)

[Reid Barton]

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.

[Johan Commelin]

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

[Johan Commelin]

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?

[Scott Morrison]

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.

[Scott Morrison]

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...

[Scott Morrison]

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.

[Johan Commelin]

I haven't yet looked in detail.

[Johan Commelin]

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?

[Reid Barton]

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)?

[Johan Commelin]

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?

[Reid Barton]

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?

[Scott Morrison]

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.)

[Scott Morrison]

Maybe this is a small cost.

[Scott Morrison]

What should the objects and morphisms be?

[Scott Morrison]

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

[Johan Commelin]

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

[Johan Commelin]

And functors preserving limits and such.

[Scott Morrison]

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.

[Johan Commelin]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Reid Barton]

pi = product of an arbitrary family?

[Scott Morrison]

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

[Scott Morrison]

Yes.

[Scott Morrison]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

Options:

[Scott Morrison]

1. leave it open for others to modify

[Scott Morrison]

2. close it for now

[Reid Barton]

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"

[Scott Morrison]

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

[Reid Barton]

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

[Reid Barton]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Scott Morrison]

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

[Scott Morrison]

I have reduced my PR to just the plain limits.

[David Michael Roberts]

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

[Scott Morrison]

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.

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

Except ... that it is...

[Scott Morrison]

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.

[Scott Morrison]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

("We" = "I", perhaps)

[Reid Barton]

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

[Reid Barton]

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

[Scott Morrison]

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

[Scott Morrison]

has_limits itself could be defined as has_limits_of id

[Scott Morrison]

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.

[Reid Barton]

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

[Scott Morrison]

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

[Scott Morrison]

Just the allowed diagrams?

[Reid Barton]

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)

[Scott Morrison]

I see.

[Reid Barton]

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

[Reid Barton]

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)

[Reid Barton]

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

[Scott Morrison]

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.

[Scott Morrison]

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

[Reid Barton]

Sounds great!

[Reid Barton]

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

[Johan Commelin]

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:

[Scott Morrison]

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. :-)

[David Michael Roberts]

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)

[Johan Commelin]

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

[David Michael Roberts]

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.

[Scott Morrison]

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

[Scott Morrison]

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

[Reid Barton]

Yeah that's a tough one. top_arrow?

[Scott Morrison]

Or should parallel_pair := bool??

[Mario Carneiro]

I like 0 and 1 for the objects

[Scott Morrison]

As in def parallel_pair := fin 2?

[Scott Morrison]

Or

inductive parallel_pair | _0 | _1

??

[Mario Carneiro]

probably not literally

[Mario Carneiro]

like the second

[Mario Carneiro]

I just mean as names

[Scott Morrison]

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

[Mario Carneiro]

0 and 1 are achievable

[Scott Morrison]

Oh, how?

[Mario Carneiro]

add an instance

[Reid Barton]

has_zero has_one

[Scott Morrison]

ah, I see.

[Scott Morrison]

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

[Reid Barton]

Probably

[Mario Carneiro]

I would call them zero and one

[Mario Carneiro]

and then use 0 and 1 as notation

[Mario Carneiro]

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

[Scott Morrison]

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

[Scott Morrison]

Sounds reasonable.

[Scott Morrison]

On to the morphisms, then. :-)

[Mario Carneiro]

yeah...

[Scott Morrison]

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

[Mario Carneiro]

no bright ideas there. left and right seem reasonable?

[Scott Morrison]

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

[Reid Barton]

surely they're top and bottom?

[Mario Carneiro]

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

[Reid Barton]

Which way do you draw your equalizers??

[Scott Morrison]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Reid Barton]

I was going to bring up binary things next.

[Mario Carneiro]

which one is that?

[Mario Carneiro]

A > B < C?

[Scott Morrison]

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

[Mario Carneiro]

left and right, definitely

[Reid Barton]

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.

[Scott Morrison]

... 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.

[Reid Barton]

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

[Reid Barton]

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

[Scott Morrison]

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

[Reid Barton]

Yes, and it should also just be less work overall

[Scott Morrison]

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?

[Scott Morrison]

I maybe prefer the last?

[Mario Carneiro]

I think I do too

[Scott Morrison]

or something with terms fst and snd?

[Scott Morrison]

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

[Mario Carneiro]

the problem with that is they aren't maps

[Mario Carneiro]

I would get the two confused

[Scott Morrison]

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

[Reid Barton]

left and right are nice for inl and inr though

[Mario Carneiro]

is it the same category being reused?

[Scott Morrison]

I don't see why not.

[Mario Carneiro]

ok, then I agree with Reid

[Reid Barton]

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

[Mario Carneiro]

although I guess technically one is the op of the other

[Reid Barton]

Yes, technically it should be the op

[Scott Morrison]

Great, I will use side with left and right.

[Reid Barton]

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

[Scott Morrison]

Finally, pullbacks and pushouts

[Mario Carneiro]

Can we steal the same names?

[Scott Morrison]

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

[Reid Barton]

middle??

[Reid Barton]

Is anyone going to actually see these names?

[Mario Carneiro]

left - inl > 1 < inr - right

[Mario Carneiro]

left < fst - 0 - snd > right

[Scott Morrison]

okay, sounds good to me

[Scott Morrison]

except...

[Reid Barton]

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

[Reid Barton]

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

[Scott Morrison]

remember the morphisms there are terms of one-element types

[Scott Morrison]

maybe we should just make all those morphisms types punit.

[Scott Morrison]

and not have names at all

[Scott Morrison]

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

[Mario Carneiro]

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

[Reid Barton]

As they say, no names is good names

[Scott Morrison]

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

[Scott Morrison]

etc

[Reid Barton]

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

[Mario Carneiro]

I think types by case analysis is a bad idea

[Scott Morrison]

remember hom : obj -> obj -> Type

[Reid Barton]

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

[Scott Morrison]

maybe I'm confused here

[Reid Barton]

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

[Mario Carneiro]

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

[Scott Morrison]

I see

[Scott Morrison]

okay, that does sound good

[Scott Morrison]

but makes it harder to name things. :-)

[Reid Barton]

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

[Reid Barton]

Er, free category on a graph construction

[Mario Carneiro]

I was just about to say the same

[Mario Carneiro]

this is a graph, not a cat

[Reid Barton]

which I do have written down somewhere

[Scott Morrison]

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

[Reid Barton]

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

[Mario Carneiro]

really? I wouldn't have expected that

[Scott Morrison]

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

[Reid Barton]

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

[Reid Barton]

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)

[Scott Morrison]

yes

[Scott Morrison]

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

[Reid Barton]

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

[Scott Morrison]

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

[Reid Barton]

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

[Reid Barton]

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

[Scott Morrison]

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

[Reid Barton]

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.

[Mario Carneiro]

Oh hey, are graphs an example of has_hom?

[Reid Barton]

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

[Mario Carneiro]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Reid Barton]

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"

[Reid Barton]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

yeah, simple graphs solve the problem

[Reid Barton]

I guess actual graph theorists would call this a multigraph

[Reid Barton]

Anyways graphs would also be examples of has_hom in any case

[Reid Barton]

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.

[Reid Barton]

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?)

[Reid Barton]

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

[Kevin Buzzard]

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.

[Scott Morrison]

@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.

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

(deleted)

[Scott Morrison]

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. :-)

[Reid Barton]

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

[Johan Commelin]

@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).

[Johan Commelin]

@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?