How to make cyclic terms (Was: A miraculous match?)

See here:
A Modality for Recursion
Hiroshi Nakano - 2000 - Zitiert von: 237
https://www602.math.ryukoku.ac.jp/~nakano/papers/modality-lics00.pdf
Even if you disband cyclic terms in your
model, like if you adhere to a strict Herband model.
If the Herband model has an equality which is a
congruence relation ≌. Nakano's paper contains
an inference rule for a congruence relation ≌.
When you have such a congruence relation, you can
of course derive things like for example for a certain
exotic recursive type C, that the following holds:
C ≌ C -> A
You can then produce the Curry Paradox in simple
types with congruence. And then ultimately derive:
|- (λx.x x)(λx.x x): A
As in Proposition 2 of Nakano's paper.
Julio Di Egidio schrieb:

(But I still wouldn't know how to create a cyclic term proper in Coq or in fact in any total functional language, despite the mechanism underlying conversion/definitional equality is logical unification, and we can even somewhat access it in Coq, via the definition of `eq`/reflexivity.)