search

emilyriehl / yoneda

comparative formalizations of the Yoneda lemma for 1-categories and infinity-categories
http://emilyriehl.github.io/yoneda/
60 stars 6 forks source link

Yoneda's lemma in Agda with a directed interval #19

Open fredrik-bakke opened 1 year ago

fredrik-bakke commented 1 year ago

Half a year ago I tried my hand at formalizing some simplicial type theory in Agda with an axiomatized directed interval. I had no idea what I was doing back then, and still don't for that matter, but managed to get some basic things written down. As far as I got was writing down (the) two definitions for Segal types and proving they are equivalent.

What I'm wondering is, would you be interested in having a formalization of Yoneda's lemma in this system as well? I think it could be at least informative to have a side-by-side comparison between formalizations in Rzk and Agda with a directed interval, and I would also appreciate some feedback on the latter (it may be that my original approach is a bit off).

If you are interested in this, I'll consider what I can get done this fall, or if I should just push some unfinished formalizations without a Yoneda lemma.

emilyriehl commented 1 year ago

@fredrik-bakke I do think this would be an interesting comparison. If I understand you correctly you'd be using a directed interval satisfying axioms similar to ours but without extension types. In that setting, I'd be particularly interested in comparing the proofs of associativity of composition in Segal types. That was the bit that Mike and I always assumed would be annoying.

Were you proposing to host those formalizations here or keep them in a separate linked repository?

fizruk commented 1 year ago

I am too interested to see formalisations in Agda.

Also, I wonder if it would make sense to have formalisations in 2+ languages available for easy comparison using Content tabs feature for code blocks. At least for the simplicial HoTT part.

jonweinb commented 1 year ago

@fredrik-bakke Thank you, I'm very interested in this, too; not last for similar reasons as @emilyriehl!

@fizruk Thanks, that seems like a great suggestion to me!

fredrik-bakke commented 1 year ago

That's great to hear!

@fredrik-bakke I do think this would be an interesting comparison. If I understand you correctly you'd be using a directed interval satisfying axioms similar to ours but without extension types. In that setting, I'd be particularly interested in comparing the proofs of associativity of composition in Segal types. That was the bit that Mike and I always assumed would be annoying.

Were you proposing to host those formalizations here or keep them in a separate linked repository?

I would also be interested in comparing these two proofs for the same reason.

Regarding your question, yes, that would be my proposition. Given that this is a repository hosting comparative formalizations of Yoneda's lemma, I figured it would perhaps be fitting to have this hosted here as well. If you agree, I can take some time in August to round up the relevant formalizations I have into a pull request. In the meanwhile, I suggest keeping this issue open.

Also, I wonder if it would make sense to have formalisations in 2+ languages available for easy comparison using Content tabs feature for code blocks. At least for the simplicial HoTT part.

The Rzk and Agda formalizations are not going to correspond 1 to 1, so I'm unsure how well this will work.

fredrik-bakke commented 1 year ago

Just as an update, I am currently working on this, and you'll hear from me when I have something worthwhile to share.