search

mikeshulman / Coq-HoTT

Homotopy type theory
http://homotopytypetheory.org/
Other
12 stars 4 forks source link

Equivalences in ooCat.v #44

Closed Alizter closed 4 years ago

Alizter commented 4 years ago

I am opening this issue as a discussion about the notions of equivalences in ooCat.v

It occurred to me earlier that if an ooCat has a terminal object and "pullbacks" (whatever that means), we could define a notion of "homotopy fiber". Then we could ask if a map's fibers are terminal in the category, which I think corresponds to equivalences by contractible fibers. This might be a more coherent notion of equivalence, at least for categories with hfibers.

mikeshulman commented 4 years ago

That doesn't work because an object of a general category may not have any global points (maps from the terminal object) and yet still be nontrivial.

I realized recently that it is actually quite easy to define a fully coherent notion of equivalence in an oo-category: just use one of the coherent HoTT notions, like bi-invertibility or half-adjoint equivalences, at all levels in a coinductive definition.

However, after talking to Tslil again this week, I also have some important changes to suggest to the whole oo-category structure. Hopefully I can get them written down soonish.

Alizter commented 4 years ago

@mikeshulman How exactly does this definition of equivalence work? On paper at least.