nLab axiom of cohesion


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



topology (point-set topology, point-free topology)

see also differential topology, algebraic topology, functional analysis and topological homotopy theory


Basic concepts

Universal constructions

Extra stuff, structure, properties


Basic statements


Analysis Theorems

topological homotopy theory



Axioms of cohesion are certain axioms added to any spatial type theory in order to define the shape modality for cohesive homotopy type theory. In particular, the axiom of real cohesion plays a role in defining real-cohesive homotopy type theory (the setting for classical homotopy theory and algebraic topology), and the axiom of affine cohesion plays a role in defining 𝔸 1 \mathbb{A}^1 -cohesive homotopy type theory (the setting for 𝔸 1 \mathbb{A}^1 -homotopy theory), where the affine line 𝔸 1\mathbb{A}^1 plays the role that \mathbb{R} does in real-cohesive homotopy type theory. Affine cohesion could hypothetically also be used in defining a cohesive version of Mitchell Riley‘s bunched linear homotopy type theory (the setting for stable homotopy theory) for the purposes of doing motivic homotopy theory.


We assume the presentation of spatial type theory using crisp term judgments a::Aa::A in addition to the usual (cohesive) type and term judgments AtypeA \; \mathrm{type} and a:Aa:A, as well as context judgments Ξ|Γctx\Xi \vert \Gamma \; \mathrm{ctx} where Ξ\Xi is a list of crisp term judgments, and Γ\Gamma is a list of cohesive term judgments. A crisp type is a type in the context Ξ|()\Xi \vert (), where ()() is the empty list of cohesive term judgments. We also assume identity types, the sharp modality, and the flat modality.

Given a type AA, let us define const A,R:A(RA)\mathrm{const}_{A, R}:A \to (R \to A) to be the type of all constant functions in RR:

δ const A,R(a,r):const A,R(a)(r)= Aa\delta_{\mathrm{const}_{A, R}}(a, r):\mathrm{const}_{A, R}(a)(r) =_A a

There is an equivalence const A,1:A(1A)\mathrm{const}_{A, 1}:A \simeq (1 \to A) between the type AA and the type of functions from the unit type 11 to AA. Given types BB and CC and a function F:(BA)(CA)F:(B \to A) \to (C \to A), type AA is FF-local if the function F:(BA)(CA)F:(B \to A) \to (C \to A) is an equivalence of types.

A crisp type Ξ|()A\Xi \vert () \vdash A is discrete if the function () :AA(-)_\flat:\flat A \to A is an equivalence of types.

The axiom of cohesion for type RR states that there is a crisp type Ξ|()Rtype\Xi \vert () \vdash R \; \mathrm{type} such that given any crisp type Ξ|()Atype\Xi \vert () \vdash A \; \mathrm{type}, AA is discrete if and only if AA is (const A,1 1const A,R)(\mathrm{const}_{A, 1}^{-1} \circ \mathrm{const}_{A, R})-local, or equivalently, if const A,R\mathrm{const}_{A, R} is an equivalence of types.

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

This allows us to define discreteness for non-crisp types: a type AA is discrete if AA is (const A,1 1const A,R)(\mathrm{const}_{A, 1}^{-1} \circ \mathrm{const}_{A, R})-local, or equivalently, if const A,R\mathrm{const}_{A, R} is an equivalence of types.

Another consequence is that the shape of RR is contractible.


Assuming a type RR and the axiom of RR-cohesion, the shape of RR is contractible.


The type RR is inhabited by κ R(σ R)\kappa_R(\sigma_R), so it remains to show that for all x:ʃRx:\esh R, x= ʃRκ R(σ R)x =_{\esh R} \kappa_R(\sigma_R). Since ʃR\esh R is discrete, so is the identity type x= ʃRκ R(σ R)x =_{\esh R} \kappa_R(\sigma_R), which means by ʃ\esh-induction, it suffices to prove σ R(x)= ʃRκ R(σ R)\sigma_R(x) =_{\esh R} \kappa_R(\sigma_R) for all x:ʃRx:\esh R. But this is true from the third introduction rule for ʃR\esh R.

In addition, if the type of booleans 𝟚\mathbb{2} is discrete, then RR is compact connected:


Assuming a type RR, a type of all propositions Ω\Omega with type reflector TT, and the axiom of RR-cohesion, if the function const 2,R\mathrm{const}_{2, R} is an equivalence of types, then for all functions P:RΩP:R \to \Omega, if for all x:Rx:R, T(P(x))¬T(P(x))T(P(x)) \vee \neg T(P(x)) is contractible, then either for all x:Rx:R, T(P(x))T(P(x)) is contractible, or for all x:Rx:R, ¬T(P(x))\neg T(P(x)) is contractible.


If P:RΩP:R \to \Omega is such that for all x:Rx:R, T(P(x))¬T(P(x))T(P(x)) \vee \neg T(P(x)) is contractible, then there is a function P:R𝟚P':R \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)). But if 𝟚\mathbb{2} is discrete, then by RR-cohesion PP' is constant, which implies that either for all x:Rx:R, T(P(x))T(P(x)) is contractible, or for all x:Rx:R, ¬T(P(x))\neg T(P(x)) is contractible. Thus, RR is compact connected if 𝟚\mathbb{2} is discrete.


There are a number of axioms which in general could be called an axiom of cohesion for type RR. The most general such axiom of cohesion is called stable local connectedness or axiom C0, which imposes no other restrictions on RR. If we additionally assume that the type RR is pointed with point 0:R0:R, then the axiom becomes punctual local connectedness or axiom C1, and if we additionally assume that the type RR is a non-trivial bi-pointed set, with points 0:R0:R, 1:R1:R, and witnesses τ 0:isSet(R)\tau_0:\mathrm{isSet}(R) and nontriv:(0= R1)\mathrm{nontriv}:(0 =_{R} 1) \to \emptyset, then the axiom becomes contractible codiscreteness or axiom C2. If we additionally assume that the type RR is a Dedekind complete Archimedean ordered lattice field (and usually written as \mathbb{R}), then the axiom becomes real cohesion or axiom \mathbb{R}-flat.

number/symbolnameassociated shape modalityadditional requirements
C 0C_0cohesion/stable local connectednesslocalization at a type RR
C 1C_1punctual cohesion/punctual local connectednesslocalization at a pointed type RR
C 2C_2contractible codiscretenesslocalization at a non-trivial bi-pointed h-set RR
discrete cohesionlocalization at a contractible type RR
affine cohesion/algebraic cohesion/𝔸 1\mathbb{A}^1-cohesionlocalization at an affine line 𝔸 1\mathbb{A}^1
compact connectednesslocalization at a type RRthe type of booleans 𝟚\mathbb{2} is discrete
continuum cohesionlocalization at a Hausdorff space RR𝟚\mathbb{2} is discrete.
metric continuum cohesionlocalization at a metric space RR𝟚\mathbb{2} is discrete.
\mathbb{R} \flatreal cohesionlocalization at the impredicative Dedekind real numbers or generalized Cauchy real numbers \mathbb{R}A type of all propositions Ω\Omega
U\mathbb{R}_{U} \flatlocally UU-small real cohesionlocalization at the UU-Dedekind real numbers or UU-generalized Cauchy real numbers U\mathbb{R}_UA Tarski universe (U,T)(U, T)
U loc\mathbb{R}_{U}^\mathrm{loc} \flatlocally UU-small localic real cohesionlocalization at the UU-localic real numbers U loc\mathbb{R}_{U}^\mathrm{loc}A Tarski universe (U,T)(U, T).
unit interval cohesionlocalization at the unit interval [0,1][0, 1]a higher coinductive type representing the homotopy terminal dyadic interval coalgebra.
UU-small unit interval cohesionlocalization at the UU-small unit interval [0,1] 𝕌[0, 1]_\mathbb{U}A Tarski universe (U,T)(U, T).
smooth cohesionlocalization at a local Artin \mathbb{R} -algebraA local Artin \mathbb{R} -algebra RR
S 1S^1 \flatcircle type cohesionlocalization at the circle typeThe circle type S 1S^1

See also


Last revised on January 25, 2023 at 16:30:38. See the history of this page for a list of all contributions to it.