[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 THEORY : https://cstheory.stackexchange.com/questions/30896/ramification-of-an-impredicative-type-theory, https://plato.stanford.edu/entries/type-theory/#3, https://homepages.inf.ed.ac.uk/wadler/papers/gr/gr-TACS-FINAL.pdf
- normalization, strong normalization : https://davewripley.rocks/papers/snctt.pdf, https://www.pls-lab.org/en/Normalization
- Decidability : https://www.math.unipd.it/~silvio/papers/TypeTheory/Decidability.pdf
- canonicity : https://cs.stackexchange.com/questions/112893/what-does-canonicity-property-mean-in-type-theory, https://arxiv.org/abs/1810.09367, https://www.cs.cmu.edu/~rwh/papers/2dtt-can/paper.pdf
- subject reduction : https://en.wikipedia.org/wiki/Subject_reduction, https://www.cs.cmu.edu/~fp/courses/15814-f19/lectures/05-subred.pdf, https://www.cs.cmu.edu/~fp/courses/15814-f19/lectures/
- Bounded quantification ： https://en.wikipedia.org/wiki/Bounded_quantification
