nLab inductive cover

 Idea

Traditionally, in mathematics and in formal topology the cover is a relation between elements of a poset $S$ and subtypes of $S$. However, that definition is impredicative, since it requires quantifiying over subtypes. There is another definition of a cover as a relation between elements of $S$ and dependent pairs $(I, \mathcal{F})$ consisting of an $U$-small index type $I:U$ and an embedding of types $\mathcal{F}:I \hookrightarrow S$ from $I$ into $S$. However, this definition requires an existing type universe $U$ in the type theory, and not all foundations of mathematics have type universes. Nonetheless, one could annotate the cover relation using the index type $I$ of the family $\mathcal{F}:I \hookrightarrow S$, in the same way that one annotates the identity types of a type with the index type $A$ in the absence of type universes. This results in a type family $z \lhd_I \mathcal{F}$ between elements $z:S$ and embeddings $\mathcal{F}:I \hookrightarrow S$ for every single type $I$, 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, \leq)$ with families of types $x:A \vdash B(x)$, $x:A, y:B(x) \vdash C(x, y)$ and a dependent function

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

such that

• for all $x:A$, $y:B(x)$, and $z:C(x, y)$, $d(x, y, z) \leq x$

$$\prod_{x:A} \prod_{y:B(x)} \prod_{z:C(x, y)} d(x, y, z) \leq x$$

• for all $x:A$ and $x':A$, $x' \leq x$ implies that for all $y:B(x)$ one can construct $y':B(x')$ such that for all $z:C(x, y)$, one can construct $z':C(x', y')$ such that $d(x', y', z') \leq 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 $U$, then the locally $U$-small inductive cover relation is given by

$$\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)}$$

$$\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)}$$

$$\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 $I$, the inductive cover relation for $I$ is a higher inductive type family $a \lhd_I e$ between elements $a:A$ and embeddings of types $e:I \hookrightarrow A$ generated by the constructors

$$\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}$$

$$\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}$$

$$\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:A \vdash B(x)$ are equivalently functions $B \to A$, so one can express the above definition in terms of single types. A formal topology is a poset $(A, \leq)$ with a set $B$, a function $f:B \to A$, a set $C$ with a function $g:C \to B$ and a function $d:C \to A$, such that

• for all $z:C$, $d(z) \leq g(f(z))$

$$\prod_{z:C} d(z) \leq g(f(z))$$

• for all $x:A$ and $x':A$, if $x \leq x'$, then for all $y:B$, $f(y) =_A x$ implies that one can construct a $y':B$ such that $f(y') =_A x'$ implies that for all $z:C$, $g(z) =_B y$ implies that one can construct a $z':C$ such that $g(z') =_B y'$ implies $d(z') \leq 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 $U$, then the locally $U$-small inductive cover relation is given by

$$\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)}$$

$$\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)}$$

$$\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 $I$, the cover relation for $I$ is a higher inductive type family $a \lhd_I e$ between elements $a:A$ and embeddings of types $e:I \hookrightarrow A$ generated by the constructors

$$\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}$$

$$\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}$$

$$\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):\mathbb{Q} \times \mathbb{Q}$ and arbitrary functions $\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:\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:\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:\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:

$$\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:

$$\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}$$

$$\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}}$$

$$\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})}$$

$$\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})}$$

$$\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)}$$

$$\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))}$$

$$\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

• cover

• inductive family

• formal topology

 References

• Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Project, Institute for Advanced Study, 2013. (web, pdf)

• Ayberk Tosun, Formal Topology in Univalent Foundations, (pdf, slides)