Modeling Martin-Löf type theory in categories
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