Closed choukh closed 1 year ago
The universe level of ∥∥-rec and ∥∥-elim in the new Cubical.Data.Equality.PropositionalTruncation hasn't been sufficiently generalized. It is quite bothersome, so I've made a quick fix.
∥∥-rec
∥∥-elim
Cubical.Data.Equality.PropositionalTruncation
Good, thanks.
felixwellen
commented
1 year ago
The universe level of
∥∥-recand∥∥-elimin the newCubical.Data.Equality.PropositionalTruncationhasn't been sufficiently generalized. It is quite bothersome, so I've made a quick fix.