[CTRL]+クリック UIP ： https://ncatlab.org/nlab/show/uniqueness+of+identity+proofs 哲学的Impredicativity : https://en.wikipedia.org/wiki/Impredicativity IMPREDICATIVE TYPE THEORY : https://arxiv.org/pdf/1911.08174.pdf PREDICATIVE TYPE THEO…