暫定版。 あんまりわからないのでわかった点だけ箇条書きする。 これまでに導入した型はすべて有限の型である。何故なら型構築演算の反復（iteration）は有限回しかできないから。言語の表現力を上げるには宇宙（universe）を導入して超限の型（transfinite …