nLab axiom K (type theory)

Contents

Context

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
propositionsetobjecttype
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

semantics

This entry is about the axiom K in type theory. For axiom K of modal logic, see axiom K (modal logic).

Contents

Idea

In type theory, the axiom K is an axiom that when added to intensional type theory turns it into extensional type theory — or more precisely, what is called here “propositionally extensional type theory”. In the language of homotopy type theory, this means that all types are h-sets, accordingly axiom K is incompatible with the univalence axiom.

Heuristically, the axiom asserts that each term of each identity type Id A(x,x)Id_A(x,x) (of equivalences of a term x:Ax \colon A) is propositionally equal to the canonical reflexivity equality proof refl x:Id A(x,x)refl_x \colon Id_A(x,x).

See also at set-level type theory.

Axiom K can also be called loop induction or self-identification induction in parallel to path induction.

Statement

K:A:Typex:AP:Id A(x,x)Type(P(refl Ax)h:Id A(x,x)P(h)) K \colon \underset{A \colon Type}{\prod} \underset{x \colon A}{\prod} \underset{P \colon Id_A(x,x) \to Type}{\prod} \left( P(refl_A x) \to \underset{h \colon Id_A(x,x)}{\prod} P(h) \right)

If one doesn’t have type universes in the type theory, then axiom K has to be expressed as an inference rule, and thus is called the K-rule:

ΓAtypeΓ,x:A,p:Id A(x,x)P(x,p)typeΓK A: x:AP(x,refl A(x)) h:Id A(x,x)P(x,h)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A, p:\mathrm{Id}_A(x,x) \vdash P(x, p) \; \mathrm{type}}{\Gamma \vdash K_A:\prod_{x:A} P(x, \mathrm{refl}_A(x)) \to \prod_{h:\mathrm{Id}_A(x,x)} P(x, h)}

Using the circle type

One can, instead of using elements x:Ax:A and self identifications p:Id A(x,x)p:\mathrm{Id}_A(x,x), use a function p:S 1Ap:S^1 \to A from the circle type S 1S^1 to express axiom K:

K :A:Typex:AP:(S 1A)Type(P(λi:S 1.x)p:S 1AP(p)) K^{\prime} \colon \underset{A \colon Type}{\prod} \underset{x \colon A}{\prod} \underset{P \colon (S^1 \to A) \to Type}{\prod} \left( P(\lambda i:S^1.x) \to \underset{p:S^1 \to A}{\prod} P(p) \right)

This states that the function type S 1AS^1 \to A is a positive copy of AA, and is equivalent to the other formulation of axiom K through the recursion principle of the circle type.

If one doesn’t have type universes in the type theory, then axiom K has to be expressed as an inference rule:

ΓAtypeΓ,p:S 1AP(p)typeΓK A : x:AP(λi:S 1.x) p:S 1AP(p)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, p:S^1 \to A \vdash P(p) \; \mathrm{type}}{\Gamma \vdash K_A^{\prime}:\prod_{x:A} P(\lambda i:S^1.x) \to \prod_{p:S^1 \to A} P(p)}

Properties

Relation to S 1S^1-localization

The negative analogue of axiom K is the axiom of S 1 S^1 -localization, which states that

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)

is an equivalence of types or a definitional isomorphism.

Theorem

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

Then S 1AS^1 \to A is a positive copy of AA: 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).

Proof

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)

Theorem

Suppose that for all types AA, S 1AS^1 \to A is a positive copy of AA through the 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)

Then Streicher’s axiom K is true: given a type AA and given a type family C(x,P)C(x, P) indexed by x:Ax:A and p:x= AXp:x =_A X, and a dependent function t: x:AC(x,refl A(x))t:\prod_{x:A} C(x, \mathrm{refl}_A(x)), one can construct a dependent function

K A(t): x:A p:x= AXC(x,p)K_A(t):\prod_{x:A} \prod_{p:x =_A X} C(x, p)

such that for all x:Ax:A,

K A(t,x,refl A(x))t(x)K_A(t, x, \mathrm{refl}_A(x)) \equiv t(x)

Proof

By the induction principle of positive copies on the type family C(f(base),ap f(loop))C(f(\mathrm{base}), \mathrm{ap}_f(\mathrm{loop})) indexed by f:S 1Af:S^1 \to A, we can construct a dependent function

K A (t): f:𝕀AC(f(base),ap f(loop))K_A^{\prime}(t):\prod_{f:\mathbb{I} \to A} C(f(\mathrm{base}), \mathrm{ap}_f(\mathrm{loop}))

such that for all x:Ax:A,

K A (t,λi:S 1.x)t(x):C(x,refl A(x))K_A^{\prime}(t, \lambda i:S^1.x) \equiv t(x):C(x, \mathrm{refl}_A(x))

since by definition of constant function and reflexivity, one has

(λi:𝕀.x)(base)xap λi:𝕀.x(loop)refl A(x)(\lambda i:\mathbb{I}.x)(\mathrm{base}) \equiv x \quad \mathrm{ap}_{\lambda i:\mathbb{I}.x}(\mathrm{loop}) \equiv \mathrm{refl}_A(x)

We define

K A(t,x,p)K A (t,rec S 1 A(x,p))K_A(t, x, p) \equiv K_A^{\prime}(t, \mathrm{rec}_{S^1}^A(x, p))

since by circle recursion one has a path rec S 1 A(x,p):S 1A\mathrm{rec}_{S^1}^A(x, p):S^1 \to A such that

rec S 1 A(x,p)(base)xap rec S 1 A(x,p)(base,base,loop)p\mathrm{rec}_{S^1}^{A}(x, p)(\mathrm{base}) \equiv x \quad \mathrm{ap}_{\mathrm{rec}_{S^1}^{A}(x, p)}(\mathrm{base}, \mathrm{base}, \mathrm{loop}) \equiv p

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

Computational behavior

Unlike its logical equivalent axiom UIP, axiom K can be endowed with computational behavior: K(A,x,P,d,refl Ax)K(A,x,P,d,refl_A x) computes to dd. This gives a way to specify a computational propositionally extensional type theory.

This sort of computational axiom K can also be implemented with, and is sufficient to imply, a general scheme of function definition by pattern-matching. This is implemented in the proof assistant Agda. (The flag --without-K alters Agda’s pattern-matching scheme to a weaker version appropriate for intensional type theory, including homotopy type theory.)

References

The axiom K was introduced in

  • Thomas Streicher, Investigations into intensional type theory Habilitation thesis (1993) (pdf)

For a review and discussion of the implementation in Coq, see

  • Pierre Corbineau, The K axiom in Coq (almost) for free (pdf)

Discussion in the context of homotopy type theory is in

around theorem 7.2.1

Last revised on February 20, 2024 at 05:48:20. See the history of this page for a list of all contributions to it.