パラメトリシティが排中律と矛盾するという話、面白い。 https://lists.chalmers.se/pipermail/agda/2012/003916.html