~~> \fz.f(f((\fz.f((\hfz.f(hhfz)) (\hfz.f(hhfz))))fz))
~~> \fz.f(f(f((\hfz.f(hhfz)) (\hfz.f(hhfz)))))
-So 2 + (HH) <~~> (HH). This is what we expect from arithmetic infinity.
-You can check to see if 2 * (HH) <~~> (HH).
+So `2 + (HH) <~~> (HH)`. This is what we expect from arithmetic infinity.
+You can check to see if `2 * (HH) <~~> (HH)`.
So our fixed point recipe has delivere a reasonable candidate for
arithmetic infinity.