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

More refactoring #52

Closed fredrik-bakke closed 1 year ago

fredrik-bakke commented 1 year ago

14

This PR completes most of the refactoring I wanted to do, I think.

fredrik-bakke commented 1 year ago

Sorry for backtracking on a suggestion I made earlier, but I've found that writing is-segal-function-type for the proof that a function type is segal if its codomain is, is a better convention than the previously suggested is-segal-function-type-is-segal.

fredrik-bakke commented 1 year ago

I wanted to also do some work on the style guide today, but alas, that did not happen

fredrik-bakke commented 1 year ago

If there are no further comments, this PR is ready for merging I believe