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