New answers tagged


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.


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