nLab inductive cover

Context

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

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

Contents

 Idea

Traditionally, in mathematics and in formal topology the cover is a relation between elements of a poset SS and subtypes of SS. However, that definition is impredicative, since it requires quantifiying over subtypes. There is another definition of a cover as a relation between elements of SS and dependent pairs (I,)(I, \mathcal{F}) consisting of an UU-small index type I:UI:U and an embedding of types :IS\mathcal{F}:I \hookrightarrow S from II into SS. However, this definition requires an existing type universe UU in the type theory, and not all foundations of mathematics have type universes. Nonetheless, one could annotate the cover relation using the index type II of the family :IS\mathcal{F}:I \hookrightarrow S, in the same way that one annotates the identity types of a type with the index type AA in the absence of type universes. This results in a type family z Iz \lhd_I \mathcal{F} between elements z:Sz:S and embeddings :IS\mathcal{F}:I \hookrightarrow S for every single type II, and is akin to using the stack semantics of the type theory.

 Definition

For arbitrary formal topologies

Ayberk Tosun in Tosun 2020 defined a formal topology as a poset (A,)(A, \leq) with families of types x:AB(x)x:A \vdash B(x), x:A,y:B(x)C(x,y)x:A, y:B(x) \vdash C(x, y) and a dependent function

d: x:A y:B(x)C(x,y)Ad:\prod_{x:A} \prod_{y:B(x)} C(x, y) \to A

such that

  • for all x:Ax:A, y:B(x)y:B(x), and z:C(x,y)z:C(x, y), d(x,y,z)xd(x, y, z) \leq x
x:A y:B(x) z:C(x,y)d(x,y,z)x\prod_{x:A} \prod_{y:B(x)} \prod_{z:C(x, y)} d(x, y, z) \leq x
  • for all x:Ax:A and x:Ax':A, xxx' \leq x implies that for all y:B(x)y:B(x) one can construct y:B(x)y':B(x') such that for all z:C(x,y)z:C(x, y), one can construct z:C(x,y)z':C(x', y') such that d(x,y,z)d(x,y,z)d(x', y', z') \leq d(x, y, z).
x:A x:A(aa) y:B(x) y:B(x) z:C(x,y) z:C(x,y)d(x,y,z)d(x,y,z)\prod_{x:A} \prod_{x:A'} (a \leq a') \to \prod_{y:B(x)}\sum_{y':B(x')} \prod_{z:C(x, y)} \sum_{z':C(x', y')} d(x', y', z') \leq d(x, y, z)

If one has a type universe UU, then the locally UU-small inductive cover relation is given by

Γa:AΓI:UΓe:IAΓp:x:I.e(x)= AaΓdir U(a,I,e,p):a U(I,e)\frac{\Gamma \vdash a:A \quad \Gamma \vdash I:U \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash p:\exists x:I.e(x) =_A a}{\Gamma \vdash \mathrm{dir}_U(a, I, e, p):a \lhd_U (I, e)}
Γa:AΓI:UΓe:IAΓb:B(a)Γf: c:C(a,b)d(a,b,c) U(I,e)Γbranch U(a,I,e,b,f):a U(I,e)\frac{\Gamma \vdash a:A \quad \Gamma \vdash I:U \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash b:B(a) \quad \Gamma \vdash f:\prod_{c:C(a, b)} d(a, b, c) \lhd_U (I, e)}{\Gamma \vdash \mathrm{branch}_U(a, I, e, b, f):a \lhd_U (I, e)}
Γa:AΓI:UΓe:IAΓp:a U(I,e)Γq:a U(I,e)Γsquash U(a,I,e,p,q):p= a U(I,e)q\frac{\Gamma \vdash a:A \quad \Gamma \vdash I:U \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash p:a \lhd_U (I, e) \quad \Gamma \vdash q:a \lhd_U (I, e)}{\Gamma \vdash \mathrm{squash}_U(a, I, e, p, q):p =_{a \lhd_U (I, e)} q}

If one doesn’t have type universes, then given a type II, the inductive cover relation for II is a higher inductive type family a Iea \lhd_I e between elements a:Aa:A and embeddings of types e:IAe:I \hookrightarrow A generated by the constructors

Γa:AΓItypeΓe:IAΓp:x:I.e(x)= AaΓdir I(a,e,p):a Ie\frac{\Gamma \vdash a:A \quad \Gamma \vdash I \; \mathrm{type} \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash p:\exists x:I.e(x) =_A a}{\Gamma \vdash \mathrm{dir}_I(a, e, p):a \lhd_I e}
Γa:AΓItypeΓe:IAΓb:B(a)Γf: c:C(a,b)d(a,b,c) IeΓbranch I(a,e,b,f):a Ie\frac{\Gamma \vdash a:A \quad \Gamma \vdash I \; \mathrm{type} \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash b:B(a) \quad \Gamma \vdash f:\prod_{c:C(a, b)} d(a, b, c) \lhd_I e}{\Gamma \vdash \mathrm{branch}_I(a, e, b, f):a \lhd_I e}
Γa:AΓItypeΓe:IAΓp:a IeΓq:a IeΓsquash I(a,e,p,q):p= a Ieq\frac{\Gamma \vdash a:A \quad \Gamma \vdash I \; \mathrm{type} \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash p:a \lhd_I e \quad \Gamma \vdash q:a \lhd_I e}{\Gamma \vdash \mathrm{squash}_I(a, e, p, q):p =_{a \lhd_I e} q}

Families of types x:AB(x)x:A \vdash B(x) are equivalently functions BAB \to A, so one can express the above definition in terms of single types. A formal topology is a poset (A,)(A, \leq) with a set BB, a function f:BAf:B \to A, a set CC with a function g:CBg:C \to B and a function d:CAd:C \to A, such that

  • for all z:Cz:C, d(z)g(f(z))d(z) \leq g(f(z))
z:Cd(z)g(f(z))\prod_{z:C} d(z) \leq g(f(z))
  • for all x:Ax:A and x:Ax':A, if xxx \leq x', then for all y:By:B, f(y)= Axf(y) =_A x implies that one can construct a y:By':B such that f(y)= Axf(y') =_A x' implies that for all z:Cz:C, g(z)= Byg(z) =_B y implies that one can construct a z:Cz':C such that g(z)= Byg(z') =_B y' implies d(z)d(z)d(z') \leq d(z).
x:A x:A(aa) y:B(f(y)= Ax) y:B(f(y)= Ax) z:C(g(z)= By) z:C(g(z)= By)(d(z)d(z))\prod_{x:A} \prod_{x:A'} (a \leq a') \to \prod_{y:B} (f(y) =_A x) \to \sum_{y':B} (f(y') =_A x') \to \prod_{z:C} (g(z) =_B y) \to \sum_{z':C} (g(z') =_B y') \to (d(z') \leq d(z))

If one has a type universe UU, then the locally UU-small inductive cover relation is given by

Γa:AΓI:UΓe:IAΓp:x:I.e(x)= AaΓdir U(a,I,e,p):a U(I,e)\frac{\Gamma \vdash a:A \quad \Gamma \vdash I:U \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash p:\exists x:I.e(x) =_A a}{\Gamma \vdash \mathrm{dir}_U(a, I, e, p):a \lhd_U (I, e)}
Γa:AΓI:UΓe:IAΓb:BΓp:f(b)= AaΓh: c:C(g(c)= Bb)(d(c) U(I,e))Γbranch U(a,I,e,b,p,h):a U(I,e)\frac{\Gamma \vdash a:A \quad \Gamma \vdash I:U \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash b:B \quad \Gamma \vdash p:f(b) =_A a \quad \Gamma \vdash h:\prod_{c:C} (g(c) =_B b) \to (d(c) \lhd_U (I, e))}{\Gamma \vdash \mathrm{branch}_U(a, I, e, b, p, h):a \lhd_U (I, e)}
Γa:AΓI:UΓe:IAΓp:a U(I,e)Γq:a U(I,e)Γsquash U(a,I,e,p,q):p= a U(I,e)q\frac{\Gamma \vdash a:A \quad \Gamma \vdash I:U \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash p:a \lhd_U (I, e) \quad \Gamma \vdash q:a \lhd_U (I, e)}{\Gamma \vdash \mathrm{squash}_U(a, I, e, p, q):p =_{a \lhd_U (I, e)} q}

If one doesn’t have type universes, then given given a type II, the cover relation for II is a higher inductive type family a Iea \lhd_I e between elements a:Aa:A and embeddings of types e:IAe:I \hookrightarrow A generated by the constructors

Γa:AΓItypeΓe:IAΓp:x:I.e(x)= AaΓdir I(a,e,p):a Ie\frac{\Gamma \vdash a:A \quad \Gamma \vdash I \; \mathrm{type} \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash p:\exists x:I.e(x) =_A a}{\Gamma \vdash \mathrm{dir}_I(a, e, p):a \lhd_I e}
Γa:AΓItypeΓe:IAΓb:BΓp:f(b)= AaΓh: c:C(g(c)= Bb)(d(c) Ie)Γbranch I(a,e,b,p,h):a Ie\frac{\Gamma \vdash a:A \quad \Gamma \vdash I \; \mathrm{type} \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash b:B \quad \Gamma \vdash p:f(b) =_A a \quad \Gamma \vdash h:\prod_{c:C} (g(c) =_B b) \to (d(c) \lhd_I e)}{\Gamma \vdash \mathrm{branch}_I(a, e, b, p, h):a \lhd_I e}
Γa:AΓItypeΓe:IAΓp:a IeΓq:a IeΓsquash I(a,e,p,q):p= a Ieq\frac{\Gamma \vdash a:A \quad \Gamma \vdash I \; \mathrm{type} \quad \Gamma \vdash e:I \hookrightarrow A \quad \Gamma \vdash p:a \lhd_I e \quad \Gamma \vdash q:a \lhd_I e}{\Gamma \vdash \mathrm{squash}_I(a, e, p, q):p =_{a \lhd_I e} q}

For the real numbers

For covers over the real numbers, one can use a generalized defintion and simply work with pairs of ratonal numbers numbers (q,r):×(q, r):\mathbb{Q} \times \mathbb{Q} and arbitrary functions :I×\mathcal{F}:I \to \mathbb{Q} \times \mathbb{Q} instead of embeddings.

We first define the following relations and operations on pairs of rational numbers:

q:,r:,s:,t:(q,r)(s,t)(q<r)((sq)×(rt))q:\mathbb{Q}, r:\mathbb{Q}, s:\mathbb{Q}, t:\mathbb{Q} \vdash (q, r) \subseteq (s, t) \coloneqq (q \lt r) \to ((s \leq q) \times (r \leq t))
q:,r:,s:,t:(q,r)(s,t)(q<r)((s<q)×(r<t))q:\mathbb{Q}, r:\mathbb{Q}, s:\mathbb{Q}, t:\mathbb{Q} \vdash (q, r) \Subset (s, t) \coloneqq (q \lt r) \to ((s \lt q) \times (r \lt t))
q:,r:,s:,t:(q,r)(s,t)(min(q,s),max(r,t)):×q:\mathbb{Q}, r:\mathbb{Q}, s:\mathbb{Q}, t:\mathbb{Q} \vdash (q, r) \cap (s, t) \coloneqq (\min(q, s), \max(r, t)):\mathbb{Q} \times \mathbb{Q}

The inductive covers are generated by the following inference rules:

Formation rules for inductive covers:

ΓItypeΓz:×Γ:I×Γz Itype\frac{\Gamma \vdash I \; \mathrm{type} \quad \Gamma \vdash z:\mathbb{Q} \times \mathbb{Q} \quad \Gamma \vdash \mathcal{F}:I \to \mathbb{Q} \times \mathbb{Q}}{\Gamma \vdash z \lhd_I \mathcal{F} \; \mathrm{type}}

Introduction rules for inductive covers:

ΓItypeΓ:I×Γz:×Γ,p:z I,q:z Iproptrunc(,z,p,q):p= z Iq\frac{\Gamma \vdash I \; \mathrm{type} \quad \Gamma \vdash \mathcal{F}:I \to \mathbb{Q} \times \mathbb{Q} \quad \Gamma \vdash z:\mathbb{Q} \times \mathbb{Q}}{\Gamma, p:z \lhd_I \mathcal{F}, q:z \lhd_I \mathcal{F} \vdash \mathrm{proptrunc}(\mathcal{F}, z, p, q):p =_{z \lhd_I \mathcal{F}} q}
ΓItypeΓ:I×Γi:IΓrefl I(,i):(i) I\frac{\Gamma \vdash I \; \mathrm{type} \quad \Gamma \vdash \mathcal{F}:I \to \mathbb{Q} \times \mathbb{Q} \quad \Gamma \vdash i:I}{\Gamma \vdash \mathrm{refl}_I(\mathcal{F}, i):\mathcal{F}(i) \lhd_I \mathcal{F}}
ΓItypeΓJtypeΓ:I×Γ𝒢:I×z:×Γtrans I,J(z,,𝒢):( i:I(i) J𝒢)(z I)(z J𝒢)\frac{\Gamma \vdash I \; \mathrm{type} \quad \Gamma \vdash J \; \mathrm{type} \quad \Gamma \vdash \mathcal{F}:I \to \mathbb{Q} \times \mathbb{Q} \quad \Gamma \vdash \mathcal{G}:I \to \mathbb{Q} \times \mathbb{Q} \quad z:\mathbb{Q} \times \mathbb{Q}}{\Gamma \vdash \mathrm{trans}_{I, J}(z, \mathcal{F}, \mathcal{G}):\left(\prod_{i:I} \mathcal{F}(i) \lhd_J \mathcal{G}\right) \to (z \lhd_I \mathcal{F}) \to (z \lhd_J \mathcal{G})}
ΓItypeΓ:I×Γz:×Γw:×Γmono I(,z,w):(zw)(w I)(z I)\frac{\Gamma \vdash I \; \mathrm{type} \quad \Gamma \vdash \mathcal{F}:I \to \mathbb{Q} \times \mathbb{Q} \quad \Gamma \vdash z:\mathbb{Q} \times \mathbb{Q} \quad \Gamma \vdash w:\mathbb{Q} \times \mathbb{Q}}{\Gamma \vdash \mathrm{mono}_I(\mathcal{F}, z, w):(z \subseteq w) \to (w \lhd_I \mathcal{F}) \to (z \lhd_I \mathcal{F})}
ΓItypeΓ:I×Γz:×Γw:×Γlocal I(,z,w):(z I)(zw) I(λi:I.(i)w)\frac{\Gamma \vdash I \; \mathrm{type} \quad \Gamma \vdash \mathcal{F}:I \to \mathbb{Q} \times \mathbb{Q} \quad \Gamma \vdash z:\mathbb{Q} \times \mathbb{Q} \quad \Gamma \vdash w:\mathbb{Q} \times \mathbb{Q}}{\Gamma \vdash \mathrm{local}_I(\mathcal{F}, z, w):(z \lhd_I \mathcal{F}) \to (z \cap w) \lhd_I (\lambda i:I.\mathcal{F}(i) \cap w)}
Γq:Γr:Γs:Γt:Γoverlap(q,r,s,t):((s,t)(q,r))(q,r) 𝟚rec 𝟚 ×((q,t),(s,r))\frac{\Gamma \vdash q:\mathbb{Q} \quad \Gamma \vdash r:\mathbb{Q} \quad \Gamma \vdash s:\mathbb{Q} \quad \Gamma \vdash t:\mathbb{Q}}{\Gamma \vdash \mathrm{overlap}(q, r, s, t):((s, t) \Subset (q, r)) \to (q, r) \lhd_\mathbb{2} \mathrm{rec}_\mathbb{2}^{\mathbb{Q} \times \mathbb{Q}}((q, t), (s, r))}
Γz:×Γwithin(z):z w:×wzλu.u\frac{\Gamma \vdash z:\mathbb{Q} \times \mathbb{Q}}{\Gamma \vdash \mathrm{within}(z):z \lhd_{\sum_{w:\mathbb{Q} \times \mathbb{Q}} w \Subset z} \lambda u.u}

Elimination rules for inductive covers:

Computation rules for inductive covers:

Properties

The Heine-Borel theorem holds for inductive covers.

Every inductive cover on the real numbers is a pointwise cover on the real numbers. Assuming excluded middle, every pointwise cover is an inductive cover.

 See also

 References

Last revised on June 25, 2024 at 21:21:22. See the history of this page for a list of all contributions to it.