Formalise anodyne maps (Section 5.5 of RS17) - Githubissues

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.

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

46 stars 12 forks source link

Formalise anodyne maps (Section 5.5 of RS17) #8

Open fizruk opened 1 year ago

fizruk commented 1 year ago

[x] Definition 5.19 (inner anodyne)
[x] Proposition 5.20
[ ] Proposition 5.21
[ ] Corollary 5.22

kyoDralliam commented 1 year ago

I started working on these items