Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing

Autor: Uemura, T., Dybjer, P., Espírito Santo, J., Pinto, L.

Publikováno v: 24th International Conference on Types for Proofs and Programs: TYPES 2018, June 18-21, 2018, Braga, Portugal
24th International Conference on Types for Proofs and Programs

We construct a model of cubical type theory with a univalent and impredicative universe in a category of cubical assemblies. We show that this impredicative universe in the cubical assembly model does not satisfy a form of propositional resizing.

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3fc7deae2ced1277a23dbd9ad0ce0f6c
https://doi.org/10.4230/LIPIcs.TYPES.2018.7

Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.

Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.

Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.

Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.