search

rzk-lang / sHoTT

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

Formalise dependent composition (Remark 8.11 of RS17 paper) #13

Open fizruk opened 1 year ago

fizruk commented 1 year ago

Should be straightforward.

jonweinb commented 1 year ago

I recently wrote a version for (iso)inner families in the Yoneda repo. I can work on integrating this into sHoTT if anyone needs it (to apply it in this case, we would need a formalization of Theorem 8.8 (issue)).