[kisoron-ml] intuitionistic type theory and inaccessible cardinals

[logic]

上記に関するproof-theoreticalな研究というと、

https://zbmath.org/?q=an%3A0953.03065
https://zbmath.org/?q=an%3A0990.03048

あたりに集約されますが、これをcategory-theoretical
ないしhomotopy-theoreticalな観点から補完する
研究をreviewしたので、ご案内しておきます。


https://zbmath.org/?q=an%3A07323980

にしむら
https://www.researchgate.net/profile/Hirokazu-Nishimura
https://www.youtube.com/watch?v=7vBit1MVfc8