nLab axiom of cohesion

Redirected from "axiom C0".

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

Topology

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

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

Introduction

Basic concepts

Universal constructions

Extra stuff, structure, properties

Examples

Basic statements

Theorems

Analysis Theorems

topological homotopy theory

Contents

 Idea

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).

 Definition

Given a type II, the axiom of II-cohesion or axiom C0 such that every crisp type TT is discrete if and only if every function from II into Disc(T)\mathrm{Disc}(T) is a constant function. Disc\mathrm{Disc} is a modality which takes types in the crisp mode to its corresponding discrete type in the cohesive mode, and a discrete type AA in the cohesive mode is one for which the canonical function ():AA\flat(-):A \to \flat A is an equivalence of types.

The axiom of II-cohesion allows us to define discreteness for non-crisp types. Given a type AA, let us define const A,I:A(IA)\mathrm{const}_{A, I}:A \to (I \to A) to be the type of all constant functions in II:

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

Type AA is II-null if the function const A,I\mathrm{const}_{A, I} is an equivalence of types.

Definition

Assuming the axiom of II-cohesion, type AA is discrete if AA is II-null.

Another consequence is that the shape of II is contractible, i.e. the axiom of strong connectedness

Theorem

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

Proof

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

Shulman 2018 showed that axiom C0 implies that every function from II into a discrete type AA is a constant function; conversely, if every function from II to a discrete type AA is constant, then it holds for the discrete types which are in the image of the Disc\mathrm{Disc} modality. Finally, Aberlé 2024 proved that the axiom of strong connectedness holds if and only if every function from II into a discrete type AA is a constant function

Properties

Theorem

The boolean domain 𝟚\mathbb{2} is discrete.

Proof

Theorem 6.19 of Shulman 18 says that the unit type is crisply discrete, and theorem 6.21 of Shulman 18 says that the sum type of two crisply discrete types is itself crisply discrete. Since the boolean domain is the sum type of two copies of the unit type, the boolean domain is crisply discrete, thus discrete.

Since the boolean domain is discrete, then the type RR is compact connected:

Theorem

Assuming the axiom of RR-cohesion, if the function const 𝟚,R\mathrm{const}_{\mathbb{2}, R} is an equivalence of types, then for all RR-indexed families of mere propositions x:RP(x)x:R \vdash P(x), if for all x:Rx:R, P(x)¬P(x)P(x) \vee \neg P(x) is contractible, then either for all x:Rx:R, P(x)P(x) is contractible, or for all x:Rx:R, ¬P(x)\neg P(x) is contractible.

Proof

If the family of mere propositions x:RP(x)x:R \vdash P(x) is such that for all x:Rx:R, P(x)¬P(x)P(x) \vee \neg P(x) is contractible, then there is a function P:R𝟚P':R \to \mathbb{2} into the boolean domain 𝟚\mathbb{2} with δ P 1 2(x):(P(x)=1 2))P(x)\delta_{P'}^{1_2}(x):(P'(x) = 1_2)) \simeq P(x) and δ P 0 2(x):(P(x)=0 2))¬P(x)\delta_{P'}^{0_2}(x):(P'(x) = 0_2)) \simeq \neg P(x). But since 𝟚\mathbb{2} is discrete, then by RR-cohesion PP' is constant, which implies that either for all x:Rx:R, P(x)=1 2P'(x) = 1_2 and thus P(x)P(x) is contractible, or for all x:Rx:R, P(x)=0 2P'(x) = 0_2 and thus ¬P(x)\neg P(x) is contractible. Thus, RR is compact connected.

Examples

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
\mathbb{R} \flatreal cohesionlocalization at the real numbers \mathbb{R}A higher coinductive type representing the homotopy terminal Archimedean ordered field \mathbb{R}
\mathbb{R} \flatreal cohesion (impredicative)localization 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)
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).
S 1S^1 \flatcircle type cohesionlocalization at the circle typeThe circle type S 1S^1

See also

 References

Last revised on August 27, 2024 at 08:28:45. See the history of this page for a list of all contributions to it.