Formalise multivariable covariance (Section 8.5 of RS17 paper) - Githubissues

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.

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

44 stars 12 forks source link

Formalise multivariable covariance (Section 8.5 of RS17 paper) #16

Open fizruk opened 1 year ago

fizruk commented 1 year ago

[ ] Proposition 8.21
[ ] Theorem 8.26
[ ] Proposition 8.27

nimarasekh commented 1 year ago

I will try 8.21, in case anybody wants to discuss it.