A variant of the WildCat Yoneda lemma

[jdchristensen]

Here's one form of the Yoneda lemma currently in the library:

Definition opyon_equiv {A : Type} `{HasEquivs A} `{!Is1Cat_Strong A}
           (a b : A)
  : (opyon1 a $<~> opyon1 b) -> (b $<~> a).

In the case where A is the wild category of types, this requires us to provide an equivalence (a -> c) <~> (b -> c) in order to get an equivalence a <~> b. But without Funext, an equivalence a <~> b only gives us maps back and forth between a -> c and b -> c which compose to the identities up to pointwise homotopy. Moreover, that weaker data is sufficient for the proof of Yoneda to go through. And I believe all of this works for any wild category A, using the graph structure on the hom types of A.

So I'd like to generalize Yoneda to this situation. I think the way to do it is to define the wild category of (1-)graphs, and to regard the representable functor as landing there. The statement would look essentially the same, and the proof would be slightly different.

Does this make sense? Does anyone already have some code related to this?

[Alizter]

I think that this would make sense and I am interested to see how you find it useful.

The proof of the wild yoneda lemma always irked me in a few ways.

1. The first being the somewhat artificial requirement of having equivalences.
2. The fact that we require the category to be strong. (If you like to think of yoneda as a strictification procedure this is a disappointing assumption).
3. The fact that we use Fun11 with no clear way to generalize to 2-functors due to our (useful) incoherent transfors (transformations between natural transformations). Having an nice way to do this would be helpful for the 3x3 lemma. (it is the only blocker infact!)

The fact that you have a new proof makes me hopeful that we can relax 1 and perhaps change the situation with 3. (2 is another mess but I don't think we know how to (or if) we can fix that).

[jdchristensen]

@Alizter My use case is that I think I can prove some equivalences between joins in a clean way using the Yoneda lemma, but my existing arguments don't need Funext, and I'd have to add Funext if I want to use the current version of the Yoneda lemma. That's not a big deal, but as I walked to work this morning I sketched a proof that doesn't need the equivalences, so should avoid needing Funext. And it just seems to fit better with the wild category philosophy of getting to choose the higher cells, rather than using the native path types. I'm not sure if this will avoid the requirement that the category be strong, but it might.

I'm not sure what you mean by your third point. For one, it's Fun01 that seems to be used, not Fun11.

On a practical note, have you already got some code that defines the wild category of graphs? (Do we have any wild categories of some kinds of wild category?)

[Alizter]

@Alizter My use case is that I think I can prove some equivalences between joins in a clean way using the Yoneda lemma, but my existing arguments don't need Funext, and I'd have to add Funext if I want to use the current version of the Yoneda lemma. That's not a big deal, but as I walked to work this morning I sketched a proof that doesn't need the equivalences, so should avoid needing Funext. And it just seems to fit better with the wild category philosophy of getting to choose the higher cells, rather than using the native path types. I'm not sure if this will avoid the requirement that the category be strong, but it might.

That sounds very exciting, I look forward to it.

On a practical note, have you already got some code that defines the wild category of graphs? (Do we have any wild categories of some kinds of wild category?)

I did some experimentation a while back with packing our typeclasses; getting A : Type to be coerced to A : Cat if an instance was available etc. The performance was varied and was difficult to debug when things went wrong. I would therefore suggest doing

Record Graph := {
  carrier :> Type;
  is1graph_carrier : IsGraph carrier;  
}.

And being careful with the is1graph_carrier lemma. Making it an instance might cause problems when there are lots of combinable instances. Doing a Hint Immediate is probably the best option; as (I think) it will cut the typeclass search as soon as it starts to go down the rabbit hole.

I had a look through my old branches, and I don't think I have anything more useful than this suggestion that you can use. If you are feeling experimental you can try my suggestion in #1641 since we bumped to 8.17. That will let you coerce (A : Type) to (A : Graph).

Good luck!

[jdchristensen]

To make the discussion more concrete, here is what I mean in the case where A is Type:

(* Special case of opyon_equiv for [A] being [Type], but using the graph structure on [a -> c] (i.e., [==]) instead of the path structure [=]. *)
Definition opyon_equiv' (a b : Type)
  (f : forall c, opyon1 a c -> opyon1 b c)
  (fn : forall c d (h : opyon1 a c) (k : c -> d), k o (f c h) == f d (k o h))
  (g : forall c, opyon1 b c -> opyon1 a c)
  (gn : forall c d (h : opyon1 b c) (k : c -> d), k o (g c h) == g d (k o h))
  (gf : forall c (h : opyon1 a c), g c (f c h) == h)
  (fg : forall c (h : opyon1 b c), f c (g c h) == h)
  : (b $<~> a).
Proof.
  snrapply (equiv_adjointify (f a idmap) (g b idmap)).
  - refine (pointwise_paths_concat (gn _ _ idmap (f a idmap)) _).
    exact (gf _ idmap).
  - refine (pointwise_paths_concat (fn _ _ idmap (g b idmap)) _).
    exact (fg _ idmap).
Defined.

Edited to directly use composition of homotopies, and to add these remarks:

No equality of paths is used, no identity homotopies are used, and no inverse homotopies are used. Composition of homotopies is used, but only in the proof, not in the hypotheses. So I think it would work if we consider the hom sets to be graphs, or to be 01 categories. Not sure what is best.

[jdchristensen]

For a general wild category A, you need to assume that the natural transformations respect the homotopies (e.g. apf below), that they are natural up to pointwise homotopy, and that they are inverse up to pointwise homotopy. And then it all goes through without needing that A is strong. So all that's left is to package this up by having opyon land in graphs.

(* Here's the version for any wild 1-category, with the assumptions spelled out by hand. *)
Definition opyon_equiv'' {A : Type} `{HasEquivs A}
           (a b : A)
  (f : forall c, opyon1 a c -> opyon1 b c)
  (apf : forall c (h k : opyon1 a c), (h $== k) -> f c h $== f c k)
  (fn : forall c d (h : opyon1 a c) (k : c $-> d), k $o (f c h) $== f d (k $o h))
  (g : forall c, opyon1 b c -> opyon1 a c)
  (apg : forall c (h k : opyon1 b c), (h $== k) -> g c h $== g c k)
  (gn : forall c d (h : opyon1 b c) (k : c $-> d), k $o (g c h) $== g d (k $o h))
  (gf : forall c (h : opyon1 a c), g c (f c h) $== h)
  (fg : forall c (h : opyon1 b c), f c (g c h) $== h)
  : (b $<~> a).
Proof.
  srapply (cate_adjointify (f a (Id a)) (g b (Id b))).
  - refine ((gn _ _ (Id b) (f a (Id a))) $@ _).
    refine (apg a _ _ (cat_idr (f a (Id a))) $@ _).
    apply gf.
  - refine ((fn _ _ (Id a) (g b (Id b))) $@ _).
    refine (apf b _ _ (cat_idr (g b (Id b))) $@ _).
    apply fg.
Defined.

[jdchristensen]

It turned out to be a bit trickier than I expected to be able to convert the above hypotheses into NatEquiv between opyon taking values in an appropriate category. NatEquiv obviously requires the target category to satisfy HasEquivs. HasEquivs requires the target category to satisfy Is1Cat. And there doesn't seem to be an obvious way to make graphs into a 1-category using pointwise edges as the two-cells, since those don't form a groupoid. I considered changing HasEquivs to only assume what is strictly needed for the definition (Is01Cat, Is2Graph, and maybe a third thing), but then it becomes a bit artificial, since there is no reason to prefer one direction over the other for various 2-cells. So instead I'm considering opyon to be valued in 0-groupoids, which do form a 1-category and do satisfy HasEquivs. Interestingly, I had to use biinvertibility to define the equivalences, rather than half-adjoint equivalences, since I found that I needed higher structure to make the proof of adjointification go through, while this is trivial for biinvertible maps.

In any case, it all works, and you get a logical equivalence between NatEquiv of opyon_0gpd functors and equivalence of the representing objects, without needing HasMorExt or Is1Cat_Strong for either implication.

I'll make a PR as soon as I finish cleaning it up a bit.

(BTW, the reason I want to use NatEquiv to package up the hypotheses is that I want to be able to compose various natural equivalences to produce the natural equivalence between the opyon functors.)