search

rzk-lang / sHoTT

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

Formalise Lemmas 10.7 and 10.8 from RS17 #44

Closed dvmcarpena closed 1 year ago

dvmcarpena commented 1 year ago

Partial solution to issue #24. I'm trying also to do the other two propositions to close the issue, but seem a little more involved.

fizruk commented 1 year ago

Looks good to me thus far! Let us know if you want this merged and complete the other propositions in a separate PR :)

emilyriehl commented 1 year ago

Let's merge this now and you can submit a new pull request with the new results whenever they're ready. @dvmcarpena you've done a great job with the style guide. But I renamed both of your terms. There are a few similar results in the covariant families file that @fredrik-bakke suggested we name "compute-thing-we're-computing-list-of-hypotheses". So I've attempted to follow that convention.

Please feel free to suggest alternate names with your next pull request also. I don't have a strong sense yet of how things should go!