finegeometer
finegeometer
Thank you! I've followed most of your advice. The exceptions are as follows: > I'm not sure how I feel about defining bisimulation by hand like this. It does look...
Responding to your comment about the lex order: **Theorem:** If the strict order `(x₁ , x₂) < (y₁ , y₂) ⇔ x₂ < y₂ ∨ (x₂ ≤ y₂ ∧ x₁...
Wow, that's much cleaner! Let me see if I can summarize what you did: The argument is: - We have a path between categories. - Over this path, we have...