search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.25k stars 193 forks source link

Prove O_inverts_functor_coeq with Funext-free Yoneda #1259

Open mikeshulman opened 4 years ago

mikeshulman commented 4 years ago

I don't have time to do this right now, but here's an approach that I think will work:

  1. Improve WildCat/Yoneda to talk about 0-groupoid-valued functors (and probably thereby remove the notion of "strong" 1-category.
  2. Prove a version of equiv_functor_sigma for equivalences of 0-groupoids and displayed categories.
  3. Prove a version of the universal property for coequalizers using 0-groupoids (see Homotopy/Suspension for a similar universal property for suspensions).
  4. Prove that this universal property is natural with respect to functor_coeq (again, see Homotopy/Suspension for the idea)
  5. Repeat the current proof using equivalences of 0-groupoids instead of equivalences of types.
mikeshulman commented 4 years ago

In principle it should also be possible to do this with cubical technology rather than wild category technology. That's what I tried this afternoon, but it got too hairy. The wild category approach requires more machinery but should be easier to keep track of (at least, that was my experience in the case of suspension).

mikeshulman commented 4 years ago

As discussed at #1264, the wild categories approach would also have advantages, so someone should try it.

Alizter commented 7 months ago

Update on this issue:

(1) has been done and has been very successful in doing funext-free proofs in various places.

We finally have displayed categories thanks to @gio256, so (2) is something that could be done soon.

(3) is something we should do for most of our HITs, starting with one for GraphQuotient.

I'm not yet sure about (4) and (5) but presumably it should be straightforward.

jdchristensen commented 7 months ago

(1) also mentions getting rid of "strong" wild-categories. Is that possible? Is it reasonable? They seem to be used in many places.

Alizter commented 7 months ago

@jdchristensen I think it is still useful to have the strong version around, but we could remove it from places that don't need it (which we probably don't have a lot of). I know some people were interested in "univalent completions" and I would assume that a Rezk completion is possible for a wildcat, however this is not something I see as being actually useful in practice, but rather as a metatheoretic nicety. It's the same reason we don't use univalence everywhere instead of equivalences since at the end of the day, univalence terms block computations. (I guess this is something HOTT will fix).