search

rzk-lang / sHoTT

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

Update 06-contractible.rzk.md #143

Closed thchatzidiamantis closed 4 months ago

thchatzidiamantis commented 4 months ago

Added proof that a Σ-type with contractible base is equivalent to the dependent type valued at the center of contraction.

nimarasekh commented 4 months ago

@emilyriehl I think this is the thing that you suggested. @thchatzidiamantis tried to follow the recommended guidelines but of course it might need adjustments, cause I am also not an expert on this.

emilyriehl commented 4 months ago

@thchatzidiamantis overall this looks great. I left a few minor comments. Come find me in person if you have any questions.

fizruk commented 4 months ago

@thchatzidiamantis The CI is complaining about a minor thing regarding the formatting of the Markdown file (not Rzk code, the text bits). To fix, please install and use Prettier in VS Code to format Markdown files automatically.

nimarasekh commented 4 months ago

@thchatzidiamantis The CI is complaining about a minor thing regarding the formatting of the Markdown file (not Rzk code, the text bits). To fix, please install and use Prettier in VS Code to format Markdown files automatically.

Is this true for all Rzk formalizations henceforth? If so maybe this should be communicated broader (on GitHub or Zulip or ...)? (maybe it was and I missed it)

fizruk commented 4 months ago

Is this true for all Rzk formalizations henceforth? If so maybe this should be communicated broader (on GitHub or Zulip or ...)? (maybe it was and I missed it)

No, this is specifically turned on for this project (sHoTT) in our GitHub Action, this is not mandatory for Rzk formalizations in general: https://github.com/rzk-lang/sHoTT/blob/33b8fc5a0d45d2d786a4ed196826407b045aa32d/.github/workflows/format.yml#L18-L22

nimarasekh commented 4 months ago

Is this true for all Rzk formalizations henceforth? If so maybe this should be communicated broader (on GitHub or Zulip or ...)? (maybe it was and I missed it)

No, this is specifically turned on for this project (sHoTT) in our GitHub Action, this is not mandatory for Rzk formalizations in general:

https://github.com/rzk-lang/sHoTT/blob/33b8fc5a0d45d2d786a4ed196826407b045aa32d/.github/workflows/format.yml#L18-L22

I see, this makes sense. So it could at least be included on https://github.com/rzk-lang/sHoTT ? (also my guess is that most current Rzk formalization is probably intended for the sHoTT project, so it might actually not really be different from a global requirement)

fizruk commented 4 months ago

So it could at least be included on https://github.com/rzk-lang/sHoTT ?

Technically, it is included in the styleguide: https://github.com/rzk-lang/sHoTT/blob/33b8fc5a0d45d2d786a4ed196826407b045aa32d/src/STYLEGUIDE.md?plain=1#L504-L508

But I guess few people read that far... A pull request with a pointer about Prettier in the README is welcome! :)

thchatzidiamantis commented 4 months ago

@thchatzidiamantis The CI is complaining about a minor thing regarding the formatting of the Markdown file (not Rzk code, the text bits). To fix, please install and use Prettier in VS Code to format Markdown files automatically.

I already have prettier installed as a vscode extension, should I do some kind of setup for it to work?

nimarasekh commented 4 months ago

So it could at least be included on https://github.com/rzk-lang/sHoTT ?

Technically, it is included in the styleguide:

https://github.com/rzk-lang/sHoTT/blob/33b8fc5a0d45d2d786a4ed196826407b045aa32d/src/STYLEGUIDE.md?plain=1#L504-L508

But I guess few people read that far... A pull request with a pointer about Prettier in the README is welcome! :)

Okay you got me with the ultimate "read the terms and conditions"!