Yoneda lemma using 0-groupoids #1745

jdchristensen · 2023-09-02T12:13:03Z

This PR adds a covariant Yoneda lemma using the representable functor Hom a - that lands in the 1-category of 0-groupoids. This is based on discussion in #1744.

I've marked this as WIP for now, as I'd like feedback, e.g. on naming, but also on anything else. I will likely also add the dual version if this looks good.

jdchristensen · 2023-09-02T15:37:52Z

The main question I have about naming is that I used a mix of "zerogpd" and "0gpd". I prefer the latter, but needed to use the former when this occurred at the start of a name, since names can't start with a digit. I could switch to "zerogpd" everywhere, or I could just drop the "zero" and use "gpd"; but maybe that is misleading.

Alizter · 2023-09-02T16:32:58Z

You could also just use Setoid.

Another thing to do is use _0gpd but starting with an underscore in OCaml really denotes an unused value. Not the same in Coq but could be suggestive.

jdchristensen · 2023-09-02T19:01:27Z

I added the dual version and also made some other cleanups.

jdchristensen · 2023-09-02T19:02:27Z

I removed the Draft label, but am still interested in more thoughts about the naming.

Alizter · 2023-09-03T14:45:05Z

What's the difference with the definition in EquivGpd again? Or let me phrase this question a little differently:

Which is the correct definition of equivalence? (i.e. which one has a univalence principle)

jdchristensen · 2023-09-03T16:19:02Z

What's the difference with the definition [of equivalence] in EquivGpd again?

Good question. I'll have to think about this some more to be sure. The definition I gave is directly modelled on what happens for types, and what you get between the Yoneda functors in a general 1-category when you have an isomorphism between the representing objects. The definition in EquivGpd seems a bit arbitrary to me, but it would be good to understand how the two compare. If anyone else has any insight, let us know. It looks like @mikeshulman added this file in 2020.

My definition is the following:

Class ZeroGpdIsEquiv {G H : ZeroGpd} (f : G $-> H) := {
  zerogpd_equiv_inv : H $-> G;
  zerogpd_eisretr : f $o zerogpd_equiv_inv $== Id H;
  zerogpd_equiv_inv' : H $-> G;
  zerogpd_eissect' : zerogpd_equiv_inv' $o f $== Id G;
}.

My thinking is that the 1-cells in a 0-dimensional object should be treated like the paths there.

With the definition in EquivGpd.v, it follows that

(** The inverse is an inverse, up to unnatural transformations *)
Definition eisretr0gpd_inv {A B : Type} (F : A -> B) `{IsEquiv0Gpd A B F}
  : F o equiv0gpd_inv F $=> idmap.

I'm not sure what $=> is here, but I guess it's just a homotopy of the underlying functions? So that's different from what I have, which is a natural transformation between 0-functors.

jdchristensen · 2023-09-03T17:17:04Z

So that's different from what I have, which is a natural transformation between 0-functors.

I take it back. First, what I have is also only a homotopy. Second, I have now proved that the two notions are logically equivalent. (I'm not sure if the types of equivalences are the same; that may be too much to hope for.)

This means that some reorganization should be done. The definition I gave is very natural, since it is modelled on what we are used to for types, and it makes HasEquivs easy to prove. Maybe the EquivGpd.v file should be moved into the ZeroGroupoid.v file, and updated to be an alternate description of the equivalences, along with proofs of various properties they have?

I'm switching this back to a Draft.

About the naming, I should switch to the convention in EquivGpd.v, where 0gpd is used as a suffix wherever possible, except that I prefer _0gpd. The name of the category itself has to be ZeroGpd, I think. I could name the morphisms ZeroFunctor or Morphism_0Gpd, and the equivalences Equiv_0Gpd.

mikeshulman · 2023-09-04T06:10:49Z

The definition in EquivGpd seems a bit arbitrary to me, but it would be good to understand how the two compare. If anyone else has any insight, let us know. It looks like @mikeshulman added this file in 2020.

I don't remember what I was thinking in 2020, but I expect I assumed that any two definitions would be logically equivalent, and chose one that I thought was simple or useful. Looking at the rest of the file EquivGpd suggests that perhaps I had some independent use for essentially surjective 0-functors, and figured that since I had to do all the work proving their properties already, I might as well piggyback on that by reusing as much of it as I could for equivalences by using a definition of equivalence that builds on essential surjectivity. And some grepping suggests that the intended application of essential surjectivity was in Homotopy/Suspension.

mikeshulman · 2023-09-04T06:12:40Z

I don't see any principled reason for the definition I gave to be "the" definition of equivalences of 0-groupoids, versus something logically equivalent to it. So if you think your version would work better in that slot, feel free to try it out as far as I'm concerned.

jdchristensen · 2023-09-04T13:49:44Z

@mikeshulman Thanks for pointing out the work in Homotopy/Suspension.v. I had only grepped for EquivGpd, so I had thought the definition wasn't used. I'll have to think more about the best way to proceed. What you did in Homotopy/Suspension has a lot of similarity to what I'd like to do for other complicated types.

jdchristensen · 2023-09-04T16:48:56Z

If you regard types A and B as 0-groupoids using their path types, then my definition is exactly the same as bi-invertibility, which, in the presence of Funext, is a proposition and is equivalent to IsEquiv. However, I'm pretty sure the definition in EquivGpd is not a proposition in general, even under Funext. For example, if F is the identity map on the circle S^1, then the SplEssSurj part is a proposition, but the essentially injective part is a set that contains the integers and is probably equivalent to the integers. So I think my definition should be the official definition, and the lemmas showing that it is equivalent to the definition in EquivGpd can be used where needed.

I also think that many things in EquivGpd won't be needed, since they will follow from general WildCat results about 1-categories which satisfy HasEquivs.

I'll see how it works out...

mikeshulman · 2023-09-04T17:57:10Z

Yes, that makes sense. I'm curious why it matters though? My perspective on 0-groupoids was that their morphisms are a replacement for path-types, and that we consider any two parallel morphisms to be "the same", i.e. they are setoids, not "typeoids".

…equivalent

jdchristensen · 2023-09-04T22:27:44Z

@mikeshulman I don't think it matters too much, but I think that it's nice that we can get a definition that specializes to the right thing when applied to types. In fact, we could probably define the 1-category structure on Type by pulling it back along the functor to ZeroGpd. And I suspect that there will be situations where using the bi-invertible definition will allow some iffs to be Equivs (assuming Funext).

That said, I think the injective and essentially surjective definition is more convenient in the applications you used it for (Suspension.v and Abelianization.v). You have less to prove with that definition, and what you get out is directly applicable to ExtendableAlong. I tried converting things, and the proofs became more complicated. Also, ZeroGpd is necessarily bundled (to be the underlying type of a category), and that makes a bunch of things awkward. In fact, it was even awkward trying to merge some overlapping material from EquivGpd and ZeroGpd. So I'm not going to try to do that anymore, and I recommend that we let both definitions serve their purpose, and that we include the lemmas that show that they are logically equivalent.

To me, the only thing that remains is the naming. Would there be any objection to me renaming the definition from EquivGpd to InjSplEssSurj or SplEssSurjInj or something like that? And then I would change the comments that mention "equivalences" accordingly. Or we could use IsEquiv0Gpd'.

The second naming thing is whether we go with 0gpd or _0gpd as the suffix. EquivGpd.v uses the former and ZeroGroupoid.v uses the latter, and I'd like to standardize on one of them.

jdchristensen · 2023-09-05T23:23:41Z

After experimenting a bit, I think it looks good to use IsSurjInj and similar names, without the 0gpd suffix. If we later need to disambiguate this, we can decide then how to do so.

Does this look good to merge?

Alizter · 2023-09-06T12:28:42Z

I want to give it one more look over.

Alizter · 2023-09-07T12:11:13Z

theories/WildCat/ZeroGroupoid.v

+Defined.
+
+(** We define equivalences of 0-groupoids.  The definition is chosen to provide what is needed for the Yoneda lemma, and to match the concept for types, with paths replaced by 1-cells.  We are able to match the biinvertible definition.  The half-adjoint definition doesn't work, as we can't prove adjointification.  We would need to be in a 1-groupoid for that to be possible.  We could also use the "wrong" definition, without the eisadj condition, and things would go through, but it wouldn't match the definition for types. *)
+Class IsEquiv_0Gpd {G H : ZeroGpd} (f : G $-> H) := {


We could eventually generalise this for an arbitrary category. It might be interesting to compare different notions of equivalence we have in this generality and see if they coincide when certain properties of the category are present.

That's a nice idea! I'll think about it in a few days. (I'm sick right now so won't be touching any of this for a while.)

Get well soon!

@Alizter It turns out that your idea worked well, so I've now added cat_hasequivs that shows that any wild 1-category has a HasEquivs structure. It's not an instance, since it might not be the desired structure in some situations.

One minor downside is that this loses the composite coercion Equiv_0Gpd G H >-> G -> H that used to exist. With the domain class generalized to any 1-category, the composite coercion no longer makes sense in general, since a general 1-category doesn't have the coercion G $-> H >-> G -> H that 0-groupoids has. And my understanding is that Coq doesn't search for composites of coercions dynamically, but just keeps track of the composites that work all of the time. I tried dozens of ways around this, but none worked. Not a big deal.

Alizter

Nice stuff!

jdchristensen · 2023-09-11T20:25:33Z

theories/WildCat/Equiv.v

@@ -8,7 +8,7 @@ Declare Scope wc_iso_scope.

 (** * Equivalences in wild categories *)

-(** We could define equivalences in any wild 2-category as bi-invertible maps, or in a wild 3-category as half-adjoint equivalences.  However, in concrete cases there is often an equivalent definition of equivalences that we want to use instead, and the important property we need is that it's logically equivalent to (quasi-)isomorphism. *)
+(** We could define equivalences in any wild 1-category as bi-invertible maps, or in a wild 2-category as half-adjoint equivalences.  However, in concrete cases there is often an equivalent definition of equivalences that we want to use instead, and the important property we need is that it's logically equivalent to (quasi-)isomorphism. In [cat_hasequivs] below, we show that bi-invertible maps do provide a [HasEquivs] structure for any wild 1-category. *)


2 and 3 changed to 1 and 2 here, since the library convention is that a wild 1-category has 2-cells.

Alizter · 2023-09-12T09:34:22Z

theories/WildCat/Equiv.v

+
+(** * There is a default notion of equivalence for a 1-category, namely bi-invertibility. *)
+
+(** We do not use the half-adjoint definition, since we can't prove adjointification for that definition. *)


When we copy-paste the adjointification proof for Type, I'm curious to see what exactly is stopping us from having it for the arbitrary case.

The claim is that a complicated composite of 2-cells is equal to another 2-cell. The proof uses associativity of 2-cell composition, that inverses act as inverses, and many similar things. But in a 1-category we assume nothing about the operations on the 2-cells.

@jdchristensen I would still be surprised to see adjointification work when we have (2(,1))-cats.

Alizter · 2023-09-12T09:35:56Z

theories/WildCat/Yoneda.v

-  - pose proof (gn := is1natural_natequiv _ _ g).
-    refine ((isnat (alnat:=gn) g (f a (Id a)) (Id b))^$ $@ _).
-    refine (fmap (g a) (cat_idr (f a (Id a))) $@ _).
+  (* Coq can't find the composite Coercion from equivalences of 0-groupoids to Funclass, so we make names for the underlying natural transformations of [f] and its inverse. *)


Can you not define this coercion explicitly for 0-groupoids?

Alizter · 2023-09-12T09:38:39Z

theories/WildCat/ZeroGroupoid.v

-  - intros g r s.
-    exact (Build_IsEquiv_0Gpd _ _ f g r g s).
-Defined.
+Definition equiv_fun_0gpd {G H : ZeroGpd} (f : G $<~> H) : G -> H


What I mean is, what happens when you declare this as a coercion:

Coercion equiv_fun_0gpd : CatEquiv' >-> Funclass.

Since CatEquiv' is defined for all 1-categories with equivs, this doesn't satisfy the uniform inheritance condition. I tried it anyways, and it locally fixes the problem, but it causes problems in other files. Coq adds it to the graph of coercions and seems to try applying the coercion even when the CatEquiv' comes from a different category. And it doesn't apply the coercions that it should in those cases. Coq doesn't seem to have a way to have a coercion defined only part of a Class.

I also tried making a new domain for the coercion, something like:

Definition Equiv_0Gpd (G H : ZeroGpd) := G $<~> H.

and defining equiv_fun_0gpd as a coercion from that domain. That satisfies the uniform inheritance condition, but doesn't get picked up when we have f : G $<~> H, but only when we have f : Equiv_0Gpd G H, even though the two are definitionally equivalent.

@jdchristensen Its reasonable not to assume the uniform inheritance condition, we can even disable the warning locally. The fact that it causes issues elsewhere is concerning however I'll need to think about it.

@Alizter Yes, initially I went that route and disabled the warning, but then Yoneda.v broke. And I think I see why, and why there's no easy way to work around it. Coq just remembers a coercion graph whose nodes are the various domains and codomains. And if a coercion is defined only partially on a Class, e.g. on G $<~> H only when G and H are 0-groupoids, then it has no way to store this restriction. So presumably it tries the coercion which gives a (silent) internal error, and then it doesn't try another coercion that does in fact work.

The first two of these do work, but the third fails:

Definition test1 {G H : ZeroGpd} (f : G $<~> H) : G $-> H := f. Definition test2 {G H : ZeroGpd} (f : G $-> H) : G -> H := f. Fail Definition test3 {G H : ZeroGpd} (f : G $<~> H) : G -> H := f.

The second one is using a coercion of Morphism_0Gpd to Funclass, with Coq realizing that in this situation, G $-> H is definitionally equivalent to Morphism_0Gpd. But the composite coercion is not in the coercion graph, and rightly so, since it doesn't work for every equivalence of 1-categories.

I tried adding an Identity coercion, and again it fixed the issue locally, but then caused a problem elsewhere, for the same reason: It didn't satisfy the uniform inheritance condition, so it was really only partially defined.

As far as I can see, unless the coercion mechanism was made a lot more sophisticated, or search was done to find paths dynamically, there's no way to handle this kind of situation. (But some expert will probably show me a trick that does handle it!)

@pi8027 As I posted it, I realized that my example doesn't capture the situation. The domain A should also depend on a parameter. Here is an example showing what is going on.

Parameter Afam : nat -> Type. Parameter B C : Type. Definition Bfam : nat -> Type := fun n => match n with O => B | _ => nat end. Parameter f : forall n, Afam n -> Bfam n. Coercion f : Afam >-> Bfam. Parameter g : B -> C. Coercion g : B >-> C. Parameter a : Afam 0. Check a : Bfam 0. Fail Check a : C. Parameter b : Bfam 0. Check b : C. (* This works... *) Check (a : Bfam 0) : C.

@jdchristensen The solution I suggested still seems to work, although it does not respect the uniform inheritance condition:

Parameter f : forall n, Afam n -> Bfam n. Coercion f : Afam >-> Bfam. Coercion f' (x : Afam 0) : B := f 0 x.

@pi8027 When I add the analogous thing in my real development, a different coercion fails to be found. In my real development, I have f : CatEquiv 42 foo bar, and that type is definitionally equal to NatEquiv foo bar. I'm trying to write f a. In the coercion graph there are now two relevant entries:

[ef0; fun_0gpd] : CatEquiv >-> Funclass (reversible) [nattrans_natequiv; trans_nattrans] : NatEquiv >-> Transformation

The first one is the new one, with ef0 the coercion that doesn't satisfy uniform inheritance. It does not apply in this case, since ef0 only applies to CatEquiv 17 (I'm making up 42 and 17 here; these are like the nat argument in Afam and Bfam above). The coercion that should apply is the second one. But Coq doesn't find it. My theory is that it finds the first one, tries to apply it, and gets an error, so it gives up.

@pi8027 I found a way to reproduce this:

Set Printing Coercions. Parameter A B C : Type. Definition Afam : nat -> Type := fun n => match n with S O => A | _ => nat end. Definition Bfam : nat -> Type := fun n => match n with O => B | _ => nat end. Parameter k : A -> C. Coercion k : A >-> C. Parameter f : forall n, Afam n -> Bfam n. Coercion f : Afam >-> Bfam. Parameter g : B -> C. Coercion g : B >-> C. Parameter a0 : Afam 0. Check a0 : Bfam 0. (* via f *) Fail Check a0 : C. (* g (f 0 a0) not found *) Parameter a1 : Afam 1. Check a1 : Bfam 1. (* via f *) Check a1 : C. (* via k *) Parameter b : Bfam 0. Check b : C. (* via g *) (* This works... *) Check (a0 : Bfam 0) : C. (* Add coercion that doesn't satisfy uniform inheritance: *) Coercion f' (x : Afam 0) : B := f 0 x. (* Now this works: *) Check a0 : C. (* But now this fails: *) Fail Check a1 : C. Print Graph.

@jdchristensen I would report this upstream in Coq so at least the other devs are aware of the issue.

jdchristensen · 2023-09-12T21:05:06Z

I'll go ahead and merge this soon unless someone says they'd like more time to review it.

jdchristensen marked this pull request as draft September 2, 2023 12:13

jdchristensen requested review from Alizter and mikeshulman September 2, 2023 12:13

jdchristensen marked this pull request as ready for review September 2, 2023 19:01

jdchristensen marked this pull request as draft September 3, 2023 17:17

jdchristensen force-pushed the yoneda branch from 0955f5a to 8054bf0 Compare September 3, 2023 17:23

jdchristensen added 9 commits September 4, 2023 14:23

Add WildCat/ZeroGroupoid.v

f3a2f1d

WildCat/Yoneda: use 0-groupoids to avoid FunExt, IsStrong

88412cb

WildCat/Yoneda: cleanups to old proofs, e.g. (A:=A^op) instead of @

b85c246

WildCat/Yoneda: add dual of Funext-free Yoneda lemma

c3d5620

Homotopy/ClassifyingSpace: adjust for changes to Yoneda.v

b4764e7

WildCat/ZeroGroupoid and EquivGpd: show that the defns are logically …

da850fb

…equivalent

WildCat/ZeroGroupoid and Yoneda: change naming convention

2569d62

WildCat/Yoneda and ZeroGroupoid: update comments, simplify some proofs

07c8b16

WildCat/ZeroGroupoid: minor cleanups, mainly to comments

8341715

jdchristensen force-pushed the yoneda branch from 8054bf0 to 8341715 Compare September 4, 2023 22:23

WildCat/ZeroGroupoid: add "split" before "essentially surjective"

40c6441

jdchristensen marked this pull request as ready for review September 4, 2023 22:28

WildCat/EquivGpd + dependencies: use IsSurjInj and similar naming

7367f8a

WildCat/EquivGpd + dependencies: update comments as well

7634508

Alizter reviewed Sep 7, 2023

View reviewed changes

Alizter approved these changes Sep 7, 2023

View reviewed changes

WildCat: define HasEquivs for any 1-category, and use it for ZeroGpd

c374bf4

jdchristensen commented Sep 11, 2023

View reviewed changes

Alizter reviewed Sep 12, 2023

View reviewed changes

jdchristensen merged commit 997d3ee into HoTT:master Sep 12, 2023

jdchristensen deleted the yoneda branch September 12, 2023 23:11


		(** * There is a default notion of equivalence for a 1-category, namely bi-invertibility. *)

		(** We do not use the half-adjoint definition, since we can't prove adjointification for that definition. *)

Yoneda lemma using 0-groupoids #1745

Yoneda lemma using 0-groupoids #1745

Conversation

jdchristensen commented Sep 2, 2023

jdchristensen commented Sep 2, 2023

Alizter commented Sep 2, 2023

jdchristensen commented Sep 2, 2023

jdchristensen commented Sep 2, 2023

Alizter commented Sep 3, 2023 • edited Loading

jdchristensen commented Sep 3, 2023

jdchristensen commented Sep 3, 2023

mikeshulman commented Sep 4, 2023

mikeshulman commented Sep 4, 2023

jdchristensen commented Sep 4, 2023

jdchristensen commented Sep 4, 2023

mikeshulman commented Sep 4, 2023

jdchristensen commented Sep 4, 2023 • edited Loading

jdchristensen commented Sep 5, 2023

Alizter commented Sep 6, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Alizter left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jdchristensen Sep 13, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jdchristensen commented Sep 12, 2023

Alizter commented Sep 3, 2023 •

edited

Loading

jdchristensen commented Sep 4, 2023 •

edited

Loading

jdchristensen Sep 13, 2023 •

edited

Loading