extract computation rule for first-path-Sigma and eq-pair

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.

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

46 stars 12 forks source link

extract computation rule for first-path-Sigma and eq-pair #61

Closed TashiWalde closed 1 year ago

emilyriehl commented 1 year ago

Hey @TashiWalde could you explain what's going on here?

It looks like you've proved (non-judgmentally) that first-path-Σ (eq-pair p q) = p. Does this work for your purposes or would you prefer to try to redefine something to get a judgmental computation?