nLab axiom of circle type localization


Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Foundational axiom



In dependent type theory, the 0-truncation modality of a type AA can be defined by localization of a type AA at the circle type S 1S^1. This means that a type AA is 0-truncated, i.e. a set, if it is S 1S^1-local, which means that, in addition to axiom K and uniqueness of identity proofs, there is another way to make the types of a universe into sets: by stipulating that every type is S 1S^1-local, or that the canonical function

const A,S 1λx:A.λi:S 1.x:A(S 1A)\mathrm{const}_{A, S^1} \equiv \lambda x:A.\lambda i:S^1.x:A \to (S^1 \to A)

which takes elements of AA to constant functions in S 1AS^1 \to A, is an equivalence of types. This is (tentatively) called the axiom of circle type localization or the axiom of S 1S^1-localization.

Assuming that one has the function const A,S 1:A(S 1A)\mathrm{const}_{A, S^1}:A \to (S^1 \to A) defined in the dependent type theory, the syntactic rules for the axiom of S 1S^1-localization in a universe 𝒰\mathcal{U} is given by:

ΓA:𝒰Γf:S 1AΓcirclocal A:isEquiv(const A,S 1)\frac{\Gamma \vdash A:\mathcal{U} \quad \Gamma \vdash f:S^1 \to A}{\Gamma \vdash \mathrm{circlocal}_{A}:\mathrm{isEquiv}(\mathrm{const}_{A, S^1})}

There is also a definitional version of S 1S^1-localization which says that const A,S 1\mathrm{const}_{A, S^1} is a definitional isomorphism:

ΓAtypeΓ,p:S 1Aconst A,S 1 1(p):A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, p:S^1 \to A \vdash \mathrm{const}_{A, S^1}^{-1}(p):A}
ΓAtypeΓ,x:Aconst A,S 1 1(λi:S 1.x)x:A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:A \vdash \mathrm{const}_{A, S^1}^{-1}(\lambda i:S^1.x) \equiv x:A}
ΓAtypeΓ,p:S 1Aλi:S 1.const A,S 1 1(p)p:S 1A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, p:S^1 \to A \vdash \lambda i:S^1.\mathrm{const}_{A, S^1}^{-1}(p) \equiv p:S^1 \to A}

Relation to axiom K

One can prove axiom K (positive copy induction rules) from the axiom of circle type localization (negative copy inference rules):


Suppose that every type AA is definitionally S 1S^1-local.

Then definitional axiom K holds: given any type AA, and any type family C(p)C(p) indexed by loops p:S 1Ap:S^1 \to A in AA, and given any dependent function t: x:AC(λi:S 1.x)t:\prod_{x:A} C(\lambda i:S^1.x) which says that for all elements x:Ax:A, there is an element of the type defined by substituting the constant loop of x:Ax:A into CC, C(λi:S 1.x)C(\lambda i:S^1.x), one can construct a dependent function K A(t): z:S 1AC(z)K_A(t):\prod_{z:S^1 \to A} C(z) such that for all x:Ax:A, K A(t,λi:S 1.x)t(x):C(λi:S 1.x)K_A(t, \lambda i:S^1.x) \equiv t(x):C(\lambda i:S^1.x).


K A(t)K_A(t) is defined to be

K A(t)λp:S 1A.t(const A,S 1 1(p))K_A(t) \equiv \lambda p:S^1 \to A.t(\mathrm{const}_{A, S^1}^{-1}(p))

and by the computation rules of loop types as negative copies, one has that for all x:Ax:A,

const A,S 1 1(λi:𝕀.x)x\mathrm{const}_{A, S^1}^{-1}(\lambda i:\mathbb{I}.x) \equiv x

and so by definition of ind S 1A(t)\mathrm{ind}_{S^1 \to A}(t) and the judgmental congruence rules for substitution, one has

K A(t,λi:S 1.x)t(const A,S 1 1(λi:S 1.x))t(x)K_A(t, \lambda i:S^1.x) \equiv t(\mathrm{const}_{A, S^1}^{-1}(\lambda i:S^1.x)) \equiv t(x)

One has the following analogies between localization at a specific type and the type theoretic letter rule that it proves:

localization ruletype theoretic letter rule
𝕀 \mathbb{I} -localizationJ-rule
S 1 S^1 -localizationK-rule


Since the boolean domain 𝟚\mathbb{2} is S 1S^1-local, the axiom of S 1S^1-localization implies that S 1S^1 is compact connected:


Assuming propositional truncation, where Ω\Omega is the type of all 𝒰\mathcal{U}-small propositions with type reflector TT, and the axiom of S 1S^1-localization, if the function const 2,S 1\mathrm{const}_{2, S^1} is an equivalence of types, then for all functions P:S 1ΩP:S^1 \to \Omega, if for all x:S 1x:S^1, T(P(x))¬T(P(x))T(P(x)) \vee \neg T(P(x)) is contractible, then either for all x:S 1x:S^1, T(P(x))T(P(x)) is contractible, or for all x:S 1x:S^1, ¬T(P(x))\neg T(P(x)) is contractible.


If P:S 1ΩP:S^1 \to \Omega is such that for all x:S 1x:S^1, T(P(x))¬T(P(x))T(P(x)) \vee \neg T(P(x)) is contractible, then there is a function P:S 1𝟚P':S^1 \to \mathbb{2} into the booleans type 𝟚\mathbb{2} with δ P 1 2(x):(P(x)=1 2))T(P(x))\delta_{P'}^{1_2}(x):(P'(x) = 1_2)) \simeq T(P(x)) and δ P 0 2(x):(P(x)=0 2))¬T(P(x))\delta_{P'}^{0_2}(x):(P'(x) = 0_2)) \simeq \neg T(P(x)). Since 𝟚\mathbb{2} is S 1S^1-local, then, by the axiom of S 1S^1-localization, PP' is constant, which implies that either for all x:S 1x:S^1, T(P(x))T(P(x)) is contractible, or for all x:S 1x:S^1, ¬T(P(x))\neg T(P(x)) is contractible. Thus, S 1S^1 is compact connected

In spatial type theory

In spatial type theory, a crisp type Ξ|()A\Xi \vert () \vdash A is discrete if the function () :AA(-)_\flat:\flat A \to A is an equivalence of types. There is a variant of the above axiom called the axiom of circle type cohesion or axiom S 1S^1 \flat, which states that given any crisp type Ξ|()Atype\Xi \vert () \vdash A \; \mathrm{type}, AA is discrete if and only if AA is S 1S^1-local, or if const A,S 1\mathrm{const}_{A, S^1} is an equivalence of types.

Ξ|()AtypeΞ|()S 1ax A:isEquiv(λx:A.x )isEquiv(const A,S 1)\frac{\Xi \vert () \vdash A \; \mathrm{type}}{\Xi \vert () \vdash S^1 \flat\mathrm{ax}_A:\mathrm{isEquiv}(\lambda x:\flat A.x_\flat) \simeq \mathrm{isEquiv}(\mathrm{const}_{A, S^1})}

This allows us to define discreteness for non-crisp types: a type AA is discrete if AA is S 1S^1-local, resulting in a flavor of cohesive homotopy type theory where the shape modality is the 0-truncation modality. This rule is equivalent to the axiom of circle type localization if every type is discrete.

See also

Last revised on December 31, 2023 at 17:59:33. See the history of this page for a list of all contributions to it.