{"id":{"repo_id":"cambridge","oai_identifier":"oai:www.repository.cam.ac.uk:1810/265152"},"canonical_url":"https://search.dev.ndltd.org/etd/cambridge/oai:www.repository.cam.ac.uk:1810/265152","repository":{"repo_id":"cambridge","name":"Cambridge University","base_url":"https://api.repository.cam.ac.uk/server/oai/request"},"display":{"title":"Type theoretic weak factorization systems","abstract":"This thesis presents a characterization of those categories with weak factorization systems that can interpret the theory of intensional dependent type theory with Σ, Π, and identity types. We use display map categories to serve as models of intensional dependent type theory. If a display map category (C, D) models Σ and identity types, then this structure generates a weak factorization system (L, R). Moreover, we show that if the underlying category C is Cauchy complete, then (C, R) is also a display map category modeling Σ and identity types (as well as Π types if (C, D) models Π types). Thus, our main result is to characterize display map categories (C, R) which model Σ and identity types and where R is part of a weak factorization system (L, R) on the category C. We offer three such characterizations and show that they are all equivalent when C has all finite limits. The first is that the weak factorization system (L, R) has the properties that L is stable under pullback along R and 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 what we call an Id-presentation: it can be built from certain categorical structure in the same way that a model of Σ and identity types generates a weak factorization system. The third is that the weak factorization system (L, R) is generated by a Moore relation system. This is a technical tool used to establish the equivalence between the first and second characterizations described. To conclude the thesis, we describe a certain class of convenient categories of topological spaces (a generalization of compactly generated weak Hausdorff spaces). We then construct a Moore relation system within these categories (and also within the topological topos) and thus show that these form display map categories with Σ and identity types (as well as Π types in the topological topos).","abstract_html":"This thesis presents a characterization of those categories with weak factorization systems that can interpret the theory of intensional dependent type theory with Σ, Π, and identity types. We use display map categories to serve as models of intensional dependent type theory. If a display map category (C, D) models Σ and identity types, then this structure generates a weak factorization system (L, R). Moreover, we show that if the underlying category C is Cauchy complete, then (C, R) is also a display map category modeling Σ and identity types (as well as Π types if (C, D) models Π types). Thus, our main result is to characterize display map categories (C, R) which model Σ and identity types and where R is part of a weak factorization system (L, R) on the category C. We offer three such characterizations and show that they are all equivalent when C has all finite limits. The first is that the weak factorization system (L, R) has the properties that L is stable under pullback along R and 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 what we call an Id-presentation: it can be built from certain categorical structure in the same way that a model of Σ and identity types generates a weak factorization system. The third is that the weak factorization system (L, R) is generated by a Moore relation system. This is a technical tool used to establish the equivalence between the first and second characterizations described. To conclude the thesis, we describe a certain class of convenient categories of topological spaces (a generalization of compactly generated weak Hausdorff spaces). We then construct a Moore relation system within these categories (and also within the topological topos) and thus show that these form display map categories with Σ and identity types (as well as Π types in the topological topos).","abstract_has_math":false,"creators":["North, Paige Randall"],"institution":"University of Cambridge","degree_name":"Doctor of Philosophy (PhD)","degree_level":"Doctoral","degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":["Hyland, Martin"],"committee_chairs":[],"committee_members":[],"year":2017,"date_issued":"2017-06-01","date_published":"2017-06-01","updated_at":"2026-07-22T22:24:13Z","subjects":["homotopy type theory","weak factorization systems","category theory"],"languages":["en"],"rights":[],"rights_urls":["https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/8bd56ca1-cd31-4731-a33b-b26be8c8c21f/download","https://www.rioxx.net/licenses/all-rights-reserved/"],"identifier_entries":[{"key":"dc:creator.authoridentifier","label":"Author Identifier","values":["0000000178760956"],"render_values":[{"text":"0000-0001-7876-0956","href":"https://orcid.org/0000-0001-7876-0956","code":true}]}]},"links":{"outbound_url":"https://doi.org/10.17863/CAM.11207","outbound_label":"DOI","outbound_source":"dc:identifier.doi"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Hyland, Martin"]},{"key":"dc:creator","label":"Author","values":["North, Paige Randall"]},{"key":"dc:creator.authoridentifier","label":"Author Identifier","values":["0000000178760956"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.issued","label":"Date","values":["2017-06-01"]},{"key":"dc:publisher.institution","label":"Dc Publisher Institution","values":["University of Cambridge"]},{"key":"dc:relation.isreferencedby.uri","label":"Dc Relation Isreferencedby URI","values":["https://www.repository.cam.ac.uk/handle/1810/265152"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"dc:type.qualificationlevel","label":"Dc Type Qualificationlevel","values":["Doctoral"]},{"key":"dc:type.qualificationname","label":"Dc Type Qualificationname","values":["Doctor of Philosophy (PhD)"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["homotopy type theory","weak factorization systems","category theory"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/8bd56ca1-cd31-4731-a33b-b26be8c8c21f/download","https://www.rioxx.net/licenses/all-rights-reserved/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.doi","label":"DOI","values":["10.17863/CAM.11207"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/09bcbec2-95ad-4779-adc8-59971bc32323/download"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["This thesis presents a characterization of those categories with weak factorization systems that can interpret the theory of intensional dependent type theory with Σ, Π, and identity types. We use display map categories to serve as models of intensional dependent type theory. If a display map category (C, D) models Σ and identity types, then this structure generates a weak factorization system (L, R). Moreover, we show that if the underlying category C is Cauchy complete, then (C, R) is also a display map category modeling Σ and identity types (as well as Π types if (C, D) models Π types). Thus, our main result is to characterize display map categories (C, R) which model Σ and identity types and where R is part of a weak factorization system (L, R) on the category C. We offer three such characterizations and show that they are all equivalent when C has all finite limits. The first is that the weak factorization system (L, R) has the properties that L is stable under pullback along R and 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 what we call an Id-presentation: it can be built from certain categorical structure in the same way that a model of Σ and identity types generates a weak factorization system. The third is that the weak factorization system (L, R) is generated by a Moore relation system. This is a technical tool used to establish the equivalence between the first and second characterizations described. To conclude the thesis, we describe a certain class of convenient categories of topological spaces (a generalization of compactly generated weak Hausdorff spaces). We then construct a Moore relation system within these categories (and also within the topological topos) and thus show that these form display map categories with Σ and identity types (as well as Π types in the topological topos)."]},{"key":"dc:format.checksum.md5","label":"Dc Format Checksum Md5","values":["87eda9de84448d1f82354d60eee3eb5f","9aca61265adeabd3de47291a908341fa"]},{"key":"dc:title","label":"Title","values":["Type theoretic weak factorization systems"]}]}],"canonical_facts":{"dc:contributor.advisor":["Hyland, Martin"],"dc:creator":["North, Paige Randall"],"dc:creator.authoridentifier":["0000000178760956"],"dc:date.issued":["2017-06-01"],"dc:description.abstract":["This thesis presents a characterization of those categories with weak factorization systems that can interpret the theory of intensional dependent type theory with Σ, Π, and identity types. We use display map categories to serve as models of intensional dependent type theory. If a display map category (C, D) models Σ and identity types, then this structure generates a weak factorization system (L, R). Moreover, we show that if the underlying category C is Cauchy complete, then (C, R) is also a display map category modeling Σ and identity types (as well as Π types if (C, D) models Π types). Thus, our main result is to characterize display map categories (C, R) which model Σ and identity types and where R is part of a weak factorization system (L, R) on the category C. We offer three such characterizations and show that they are all equivalent when C has all finite limits. The first is that the weak factorization system (L, R) has the properties that L is stable under pullback along R and 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 what we call an Id-presentation: it can be built from certain categorical structure in the same way that a model of Σ and identity types generates a weak factorization system. The third is that the weak factorization system (L, R) is generated by a Moore relation system. This is a technical tool used to establish the equivalence between the first and second characterizations described. To conclude the thesis, we describe a certain class of convenient categories of topological spaces (a generalization of compactly generated weak Hausdorff spaces). We then construct a Moore relation system within these categories (and also within the topological topos) and thus show that these form display map categories with Σ and identity types (as well as Π types in the topological topos)."],"dc:format.checksum.md5":["87eda9de84448d1f82354d60eee3eb5f","9aca61265adeabd3de47291a908341fa"],"dc:identifier.doi":["10.17863/CAM.11207"],"dc:identifier.uri":["https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/09bcbec2-95ad-4779-adc8-59971bc32323/download"],"dc:language":["en"],"dc:publisher.institution":["University of Cambridge"],"dc:relation.isreferencedby.uri":["https://www.repository.cam.ac.uk/handle/1810/265152"],"dc:rights":["https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/8bd56ca1-cd31-4731-a33b-b26be8c8c21f/download","https://www.rioxx.net/licenses/all-rights-reserved/"],"dc:subject":["homotopy type theory","weak factorization systems","category theory"],"dc:title":["Type theoretic weak factorization systems"],"dc:type":["Thesis"],"dc:type.qualificationlevel":["Doctoral"],"dc:type.qualificationname":["Doctor of Philosophy (PhD)"]},"updated_at":"2026-07-22T22:24:13Z"}