皆様
来週木曜日に、京都大学にて上村太一さん(University of Amsterdam)のご講演があります。 詳細は以下のとおりです。どうぞお気軽にご参加ください。
京都大学数理解析研究所 照井一成
========== Time: 11:00-12:00, 26 July, 2018 Place: Rm 478, Research Building 2, Main Campus, Kyoto University 京都大学 本部構内 総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34)
Speaker: Taichi Uemura (University of Amsterdam)
Title: Cubical Assemblies and the Independence of the Propositional Resizing Axiom
Abstract: Cubical type theory gives a constructive justification of the univalence axiom. A model of this type theory in cubical sets is build, informally, in constructive metatheory, so this construction should work internally in suitable categories other than Set. Orton and Pitts have given a sufficient condition for modeling cubical type theory in an elementary topos. Based on their work, I build the cubical set model internally in the category of assemblies. A feature of this new model is that it has a universe which is impredicative as well as univalent, but this model does not satisfy the propositional resizing axiom.