Modeling Martin-Löf type theory in categories

Journal of Applied Logic - Tập 12 - Trang 28-44 - 2014
François Lamarche1
1INRIA Saclay – Ile de France, Equipe-Projet Parsifal, France

Tài liệu tham khảo

Awodey, 2009, Homotopy-theoretic models of identity types, Math. Proc. Camb. Philos. Soc., 146, 45, 10.1017/S0305004108001783 Berg, 2011, Types are weak ω-groupoids, Proc. Lond. Math. Soc., 102, 370, 10.1112/plms/pdq026 Cartmell, 1986, Categorical models of dependent type theory, Ann. Pure Appl. Log., 32, 209, 10.1016/0168-0072(86)90053-9 Gambino, 2008, The identity type weak factorisation system, Theor. Comput. Sci., 409, 94, 10.1016/j.tcs.2008.08.030 Garner, 2012, Topological and simplicial models of identity types, ACM Trans. Comput. Log., 13, 3:1 Hofmann, 1995, On the interpretation of type theory in locally cartesian closed categories, vol. 933, 427 Hofmann, 1998, The groupoid interpretation of type theory, vol. 36, 83 Jacobs, 1999, Categorical Logic and Type Theory, vol. 141 Lamarche, 1989 Lamarche Lambek, 1994, Bilinear logic in algebra and linguistics, vol. 222, 43 Lawvere, 1973, Metric spaces, generalized logic and closed categories, Rend. Semin. Mat. Fis. Milano, XLIII, 135, 10.1007/BF02924844 Lumsdaine, 2009, Weak ω-categories obtained from weak factorization systems, vol. 5608 Pitts, 2000, Categorical logic, 39 Streicher Streicher, 2014, A model of type theory in simplicial sets: A brief introduction to Voevodskyʼs homotopy type theory, J. Appl. Log., 12, 45, 10.1016/j.jal.2013.04.001 Taylor, 1987 Voevodsky Warren, 2008