arXiv 0803.43492008-03math.LOmath.CT

The identity type weak factorisation system

Nicola Gambino, Richard Garner

备注：: 25 pages; accepted for publication in Theoretical Computer Science
发表信息：: Theoretical Computer Science 409 (2008), no. 1, 94--109
DOI：: 10.1016/j.tcs.2008.08.030

英文摘要：

We show that the classifying category C(T) of a dependent type theory T with axioms for identity types admits a non-trivial weak factorisation system. We provide an explicit characterisation of the elements of both the left class and the right class of the weak factorisation system. This characterisation is applied to relate identity types and the homotopy theory of groupoids.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

Models of Martin-Löf type theory from algebraic weak factorisation systems

We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-Löf type theory. This is done by showing that the comprehension category associated to a type-theoretic algebraic weak factorisation system satisfies the assumptions necessary to apply a right adjoint method for splitting comprehension categories. We then provide methods for constructing several examples of type-theoretic algebraic weak factorisation systems, encompassing the existing groupoid model and cubical sets models, as well as some models based on normal f…

2021-04-23math.CTmath.LO

代数弱分解系统的 Frobenius 等价与 Beck-Chevalley 条件

The Frobenius equivalence and Beck-Chevalley condition for Algebraic Weak Factorisation Systems

本文针对代数弱分解系统证明 Frobenius 等价与 Beck-Chevalley 条件的类比命题，指出其结构包含分解与提升，并基于类型论范畴语义动机，以群胚的分裂纤维化为例说明其应用。

2024-04-23math.CTmath.LO

Topological and simplicial models of identity types

In this paper we construct new categorical models for the identity types of Martin-Löf type theory, in the categories Top of topological spaces and SSet of simplicial sets. We do so building on earlier work of Awodey and Warren, which has suggested that a suitable environment for the interpretation of identity types should be a category equipped with a weak factorisation system in the sense of Bousfield--Quillen. It turns out that this is not quite enough for a sound model, due to some subtle coherence issues concerned with stability under substitution; and so our first task is to introduce a …

2011-10-14math.CTmath.LO

An Algebraic Weak Factorisation System on 01-Substitution Sets: A Constructive Proof

We will construct an algebraic weak factorisation system on the category of 01 substitution sets such that the R-algebras are precisely the Kan fibrations together with a choice of Kan filling operation. The proof is based on Garner's small object argument for algebraic weak factorization systems. In order to ensure the proof is valid constructively, rather than applying the general small object argument, we give a direct proof based on the same ideas. We use this us to give an explanation why the J computation rule is absent from the original cubical set model and suggest a way to fix this.

2016-05-17math.LO

双范畴小对象论证的构造性方法

A constructive approach to the double-categorical small object argument

本文提出了一种双范畴小对象论证的构造性方法，通过链的极限构造显式因子分解，从而在构造性设置中证明有效Kan纤维作为代数弱因子系统的右类。

2025-12-12math.CTmath.LO

A category-theoretic version of the identity type weak factorization system

Gambino and Garner proved that the syntactic category of a dependent type theory with identity types can be endowed with a weak factorization system structure, called identity type weak factorization system. In this paper we consider an enrichment of Joyal's notion of tribe, which we call a tribe with weakly stable path objects, and prove a purely category-theoretic version of the identity type weak factorization system, thus generalizing Gambino and Garner's result. We conclude showing that this structure subsumes also the weak factorization systems coming from the topological and simplicial …

2018-04-23math.CTmath.LO

更多相关论文收起更多论文

Weak omega-categories from intensional type theory

We show that for any type in Martin-Löf Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. Precisely, we construct a contractible globular operad of definable composition laws, and give an action of this operad on the terms of any type and its identity types.

2010-09-17math.CTmath.LO

Path categories and propositional identity types

Connections between homotopy theory and type theory have recently attracted a lot of attention, with Voevodsky's univalent foundations and the interpretation of Martin-Lof's identity types in Quillen model categories as some of the highlights. In this paper we establish a connection between a natural weakening of Martin-Lof's rules for the identity types which has been considered by Cohen, Coquand, Huber and Mortberg in their work on a constructive interpretation of the univalence axiom on the one hand, and the notion of a path category, a slight variation on the classic notion of a category o…

2016-09-20math.CTmath.LO

Identity Types in Algebraic Model Structures and Cubical Sets

We give a general technique for constructing a functorial choice of very good paths objects, which can be used to implement identity types in models of type theories in direct manner with little reliance on general coherence results. We give a simple proof that applies in algebraic model structures that possess a notion of structured weak equivalence, in a sense that we define here. We then give a more direct proof that applies both to the original BCH cubical set model and more recent variants. We give an explanation how this construction relates to the one used in the CCHM cubical set model …

2018-08-02math.CTmath.LO

Types are weak omega-groupoids

We define a notion of weak omega-category internal to a model of Martin-Löf type theory, and prove that each type bears a canonical weak omega-category structure obtained from the tower of iterated identity types over that type. We show that the omega-categories arising in this way are in fact omega-groupoids.

2011-10-14math.CTmath.LO

Solid weak BCC-algebras

We characterize weak BCC-algebras in which the identity $(xy)z=(xz)y$ is satisfied only in the case when elements $x,y$ belong to the same branch.

2012-04-29math.LO

From Identity to Difference: A Quantitative Interpretation of the Identity Type

We explore a quantitative interpretation of 2-dimensional intuitionistic type theory (ITT) in which the identity type is interpreted as a "type of differences". We show that a fragment of ITT, that we call difference type theory (dTT), yields a general logical framework to talk about quantitative properties of programs like approximate equivalence and metric preservation. To demonstrate this fact, we show that dTT can be used to capture compositional reasoning in presence of errors, since any program can be associated with a "derivative" relating errors in input with errors in output. Moreover…

2021-07-13cs.LOmath.LO