[logic-ml] Talk by Taichi Uemura (26 July, 11.00-, at Kyoto University)

[Kazushige TERUI]

皆様

来週木曜日に、京都大学にて上村太一さん(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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.fos.kuis.kyoto-u.ac.jp/pipermail/logic-ml/attachments/20180719/48eb9bae/attachment.html>