search

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.
https://rzk-lang.github.io/sHoTT/
45 stars 12 forks source link

definition of a representable covariant family #98

Closed jonalfcam closed 1 year ago

jonalfcam commented 1 year ago

I'm starting work on 9.10 and probably the definition of Yoneda embedding (def 9.3).

fizruk commented 1 year ago

Regarding the Yoneda embedding, if you haven't started, it seems #100 has it.

jonalfcam commented 1 year ago

Great! I hadn't seen anyone claim it on the issues page. I won't have to do it!

cesarbm03 commented 1 year ago

Hey Jonathan, I just saw this now. I made some progress on the Yoneda embedding over the weekend. I should comment on the issue then. Sorry about it.

emilyriehl commented 1 year ago

Minor comments about the markdown portion. Otherwise I think this is okay to merge.

jonalfcam commented 1 year ago

Thanks for taking a look. I'll try to default to rzk code blocks in the future.

jonalfcam commented 1 year ago

Looking at what it takes to formalize this, it seems there is a need for a bunch of "hom behaves well with respect to equivalences of underlying types" statements. That is, if $A \simeq B$ then we would like $\text{hom}_A (a, a') \simeq \text{hom}_B (f a, f a')$. This statement then requires some statements about "natural equivalences." I believe to prove this one needs some trivial but useful statements about the functoriality of hom with respect to equality. For instance, under no assumptions about $A$, $\text{hom}_A (a, x) = \text{hom}_A (a, y)$ if $x = y$. Given their somewhat basic nature, I'd be tempted to include these shortly after the definition of hom. Then it is reasonably easy to prove that every property of hom is respected by equivalence of types.

It is also possible that I'm being dense and I've missed that this is already implemented or doesn't need to be.

jonalfcam commented 1 year ago

It is also possible that they are trivial enough to not require their own names, but it seems somewhat useful.

jonalfcam commented 1 year ago

Eh. I was trying to do something too general, and I think this needs univalence. I will revert to working with less general types.