Formalise propositions about extension extensionality (Section 4.4 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

[x] Axiom 4.6
[x] Construction 4.7 (ext-htpy-eq)
[x] Proposition 4.8
- [x] (i)
- [x] (ii) (ExtExt is defined but is not connected to the definition of Axiom 4.6)
[x] Proposition 4.10
[x] Proposition 4.11
[ ] Proposition 4.12 (currently only instances of the proposition for specific n can be stated in Rzk)

May require extra definitions in the HoTT part.

jonalfcam commented 1 year ago

I'm going to start work on this.