Formalise Propositions 3.6 and 3.7 from RS17 paper

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.

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

44 stars 12 forks source link

Closed fizruk closed 1 year ago

fizruk commented 1 year ago

Should be straightforward, no HoTT preliminaries required.

dvmcarpena commented 1 year ago

I'm trying to solve this one, nearly there.