arXiv Open Access 2019

Type-theoretic weak factorization systems

Paige Randall North

Lihat Sumber

Abstrak

This article presents three characterizations of the weak factorization systems on finitely complete categories that interpret intensional dependent type theory with Sigma-, Pi-, and Id-types. The first characterization is that the weak factorization system (L,R) has the properties that L is stable under pullback along R and that all maps to a terminal object are in R. We call such weak factorization systems type-theoretic. The second is that the weak factorization system has an Id-presentation: roughly, it is generated by Id-types in the empty context. The third is that the weak factorization system (L, R) is generated by a Moore relation system, a generalization of the notion of Moore paths.

Topik & Kata Kunci

math.CT cs.LO

Penulis (1)

Paige Randall North

Format Sitasi

APA MLA BibTeX

North, P.R. (2019). Type-theoretic weak factorization systems. https://arxiv.org/abs/1906.00259

Akses Cepat

Lihat di Sumber

Informasi Jurnal

Tahun Terbit: 2019
Bahasa: en
Sumber Database: arXiv
Akses: Open Access ✓