PaperlayerView exact revision on arXiv

Source-linked AI summary

The identity type weak factorisation system

Nicola Gambino, Richard Garner

arXiv:0803.4349v2math.LOmath.CT

TL;DR

Identity types have a complex categorical structure, and familiar locally cartesian closed semantics validates reflection rules that trivialize them. The paper constructs a non-trivial weak factorisation system on the classifying category using display maps, then characterises its classes and relates them to groupoids. The characterisation identifies the classes with type-theoretic injective equivalences and normal isofibrations, while the groupoid functor sends them to injective equivalences and Grothendieck fibrations.

  • Problem

    Identity types have a complex iterated structure, while locally cartesian closed semantics validates reflection rules that make them essentially trivial.

    Source: §1 · p. 1

  • Method

    The paper defines a weak factorisation system using display maps, uses identity-type axioms to verify it, characterises its classes, and relates it to groupoids by a functor from C(T).

    Source: §1 · p. 2, §4 · p. 13

  • Results

    The classifying category C(T) admits a non-trivial weak factorisation system whose left and right classes are respectively type-theoretic injective equivalences and type-theoretic normal isofibrations.

    Source: §4 · p. 13, §5 · p. 17

  • Takeaways & Limitations

    Under the functor to groupoids, left-class maps become equivalences injective on objects and right-class maps become Grothendieck fibrations.

    Source: §5 · p. 21

    C(T) does not have arbitrary pullbacks, though it admits pullbacks along dependent projections, which are right-class maps.

    Source: §5 · p. 19

Abstract

from arXiv · show

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.

1. Introduction

Identity types encode proofs of equality, but their iterated structure complicates categorical semantics; locally cartesian closed semantics also validates reflection rules that trivialize them. The paper constructs a non-trivial weak factorisation system on the classifying category and uses it to connect identity types with groupoids.

1. Introduction

  • Identity types encode proofs that two elements are equal, yet iterating them produces equality proofs between proofs and further layers of structure.Locally cartesian closed semantics validates reflection rules that make identity types essentially trivial.Source: §1 · p. 1
  • The classifying category C(T) of a dependent type theory with identity types admits a non-trivial weak factorisation system, called the identity type weak factorisation system.The paper presents this as evidence of a close connection between identity-type axioms and weak factorisation systems.Source: §1 · p. 1
  • The result also contributes to the development of functorial semantics for dependent type theories.The introduction frames the main result as analogous to the cartesian closed structure on the classifying category of simply-typed λ-calculus [19, 29].Source: §1 · pp. 1–2
  • The system is defined using display maps rather than identity types; identity-type axioms are used to verify its weak factorisation system axioms.The paper explicitly characterises both map classes and applies the characterisation to stability and groupoids.Source: §1 · p. 2
  • The paper extends the groupoid construction from individual types to contexts, then defines a functor F : C(T) → Gpd.It shows that F maps the identity type weak factorisation system into the system determined by injective equivalences and Grothendieck fibrations in Gpd.Source: §1 · p. 2

2. Identity types

This section sets up the classifying-category language and identity-type rules used to build identity contexts. It distinguishes propositional from definitional equality and explains why the paper uses generalized identity rules without assuming Π-types.

2. Identity types

  • The classifying category C(T) has contexts as objects and context morphisms as maps, with composition given by substitution; display maps project away one variable.Dependent projections are composites of display maps.Source: §2 · p. 3
  • Identity-type formation makes IdA(a,b) a type, and its elements witness propositional equality, distinct from definitional equality.The rules also include reflexivity, elimination, and computation.Source: §2 · pp. 2, 4, 5
  • The generalized elimination and computation rules allow a dependent context Θ(x,y,u), rather than only an empty context.These generalized rules suffice for the Leibniz rule without Π-types; with Π-types, they follow from the standard identity rules.Source: §2 · pp. 5–6
  • The theory does not assume reflection rules, which would collapse propositional and definitional equality and destroy type-checking decidability.The text states that reflection rules are generally avoided for this reason.Source: §2 · p. 6
  • Identity contexts IdΦ(a,b) are constructed from identity types and inherit formation, introduction, elimination, and computation rules.The construction proceeds by induction on context length; the rules are derived from the identity-type axioms.Source: §2 · p. 7
  • In extending a context by one variable, the construction uses the Leibniz rule for contexts to transport the new component across an identity.The paper omits details of the remaining inductive rule definitions, referring readers to.Source: §2 · pp. 7, 9

3. The fundamental groupoid of a context

Identity types let contexts be viewed as spaces whose points are connected by paths, with homotopies identifying paths. The section constructs a fundamental groupoid for each context and extends the construction to a functor from C(T) to groupoids.

3. The fundamental groupoid of a context

  • Identity types supply paths between points and homotopies between paths, making homotopy equivalence the relation used to form the groupoid's maps.Homotopy of paths is reflexive, symmetric, and transitive.Source: §3 · pp. 9–10
  • A context's points become objects, and homotopy classes of paths between them become the maps of its fundamental groupoid.Path composition, identities, and inverses are induced by the corresponding operations on paths.Source: §3 · p. 11
  • The construction sends each context morphism to a functor between its fundamental groupoids, yielding F : C(T) → Gpd.A morphism sends a point a to f(a) and a path class [p] to [f(p)].Source: §3 · p. 11

4. The identity type weak factorisation system

For a dependent type theory with identity types, the classifying category has a weak factorisation system defined using display maps. Identity-type rules support the factorisations, while the resulting system is not functorial.

4. The identity type weak factorisation system

  • A = ⋔D and B = A⋔ form a weak factorisation system on C(T), where D is the class of display maps.The classes are defined without identity types, which are used to verify the weak factorisation system axioms.Source: §4 · p. 13
  • Every map factors as f = pi, with i in A and p a dependent projection.Theorem 10 follows from this factorisation result and the weak orthogonality axiom.Source: §4 · pp. 13, 15
  • Identity elimination supplies diagonal fillers for the factorisation maps, using identity contexts and their computation rule.The constructed filler uses the identity elimination rule; its top triangle commutes by the computation rule.Source: §4 · pp. 12, 14, 15, 16
  • The identity type weak factorisation system is not functorial: the composite of the induced identity-context maps need not equal the map induced by the composite.That equality holds only pointwise up to propositional equality.Source: §4 · p. 16

5. Characterisation and applications

The section characterizes the two classes of the identity type weak factorisation system and applies that characterization to homotopy and groupoids. It relates maps in the classifying category to familiar groupoid maps and compares the factorisations in both categories.

Characterisation and applications

  • The identity type weak factorisation system does not seem to be functorial, although the authors establish the characterisation of its classes.The argument follows the approach used for characterising maps of a functorial weak factorisation system.Source: §5 · p. 17
  • The left class consists exactly of type-theoretic injective equivalences, and the right class exactly of type-theoretic normal isofibrations.These characterizations apply to the identity type weak factorisation system.Source: §5 · p. 17
  • Maps in C(T) are homotopic exactly when their values are pointwise propositionally equal; closure of the left class under pullback along dependent projections ensures transitivity.C(T) need not have arbitrary pullbacks, but it admits pullbacks along dependent projections.Source: §5 · pp. 18–19
  • Under F, maps in the left class become equivalences injective on objects, while maps in the right class become Grothendieck fibrations.The comparison is between the fundamental groupoids of the source and target contexts.Source: §5 · p. 21
  • For each context morphism f, F(Id(f)) is equivalent, surjectively on objects, to Path(F(f)).The objects of F(Id(f)) are triples (a, b, p) with p ∈ Id(f(a), b), which map to (a, b, [p]) in Path(F(f)).Source: §5 · p. 22
  • For every context Φ, a special case gives a surjective equivalence involving the groupoid of isomorphisms in F(x ∈ Φ).The supplied passage identifies the groupoid as F(x ∈ Φ)J but does not include the other endpoint of the equivalence.Source: §5 · p. 22

Axiom, weakening and substitution.

The rule described here requires that x not occur freely in Γ or Δ.

Axiom, weakening and substitution

Loading 0803.4349v2…