>>672 を参考にしつつ……質問というか確認というか。

何度か出ている Hydra と Hardy が同じというのは

Hydra : List -> N^N
Hardy' : Ord -> N^N
なんか変換 : List -> Ord

で作られる三角形が可換だという理解でいいんでしょうか。