>>12
計算論から見たホモトピー型論理とかそっち?。