型論理とかカン拡張とか