fix wrong naming - Githubissues

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.

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

46 stars 12 forks source link

fix wrong naming #101

Closed TashiWalde closed 1 year ago

TashiWalde commented 1 year ago

This is a very minor edit because I realized I had misnamed some terms in an earlier PR.

Replaces is-inner-fibration with is-left-fibration for theorems that prove something about left fibrations.
Replace "total space" with "total type".

PS: What is the correct workflow for these sort of really minor edits? Is seems kinda silly creating a PR just for them; but on the other hand I don't want to batch them with something that's completely unrelated.

jonweinb commented 1 year ago

That's okay, someone of the members can approve it.

emilyriehl commented 1 year ago

I feel silly making PRs for this sort of thing too but on the other hand naming changes can mess up someone else's work in progress so it's nice to have a bit of control of the timing of the merge.

fizruk commented 1 year ago

PS: What is the correct workflow for these sort of really minor edits? Is seems kinda silly creating a PR just for them; but on the other hand I don't want to batch them with something that's completely unrelated.

It is absolutely okay to create a small PR with minor fixes :)