New answers tagged lo.logic
5
I have reached out to the authors of papers [1] and [2], and it seems that the claims were both in error, leaving this an open question.
0
It matters once you have higher inductive types. Consider the following example (Agda):
data S¹ : Set where
base : S¹
loop : base ≡ base
Changing the order will make loop impossible to see base.
EDIT: there is an interesting conversation in the comments below, which defines how 'does not matter' the order is.
Top 50 recent answers are included