Formalise closure properties of covariance (Section 8.7 of RS17 paper)

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.

https://rzk-lang.github.io/sHoTT/

44 stars 12 forks source link

Open fizruk opened 1 year ago

fizruk commented 1 year ago

nimarasekh commented 1 year ago

Made a PR for 8.30. 8.31 is open for now cause I'm trying 8.21 in case somebody wants it in the meantime.