search

rzk-lang / sHoTT

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

Example 8.14 #29

Closed TashiWalde closed 1 year ago

TashiWalde commented 1 year ago

partially address #14

fredrik-bakke commented 1 year ago

partially resolves #14

You have to be careful with words like "fixes" and "resolves" on GitHub. With the way your comment is phrased, GitHub will mark the issue as resolved when this PR is merged, so I suggest a different phrasing like "Addresses item 1 in #14.".

fredrik-bakke commented 1 year ago

How about compute-covariant-transport-of-hom-family-is-segal for this definition? It reads like a computation principle to me, and as always, we append the assumption that A is Segal. Another alternative is eq-comp-covariant-transport-of-hom-family-is-segal, where we prepend the concluding type, using "comp" instead of "composition" to distinguish it from composition witnesses.