Definitions for Simplicial principal bundles in parametrized spaces

QAlgorithms.Papers.Independent.Intakethird100.P73.EquivariantCylinderMap

Let $B$ be a compactly generated topological space, $G$ a parametrized group over $B$, and $X,Y$ right $G$-spaces over $B$. Explicitly, the total spaces are compactly generated; their projections are continuous; $G$ has a continuous unit section and inverse and fiberwise group multiplication; and $X,Y$ have projection-preserving right actions satisfying the unit and associativity laws. Multiplication and actions are continuous on the kifications of their same-fiber pair spaces. For any space $T$, write $K(T)$ for its underlying set with the topology in which $U$ is open exactly when every continuous map from a compact Hausdorff space into $T$ has open inverse image of $U$. An equivariant cylinder map from $X$ to $Y$ consists of a continuous function

$$H:K(X\times[0,1])\longrightarrow Y$$

such that, for every $x\in X$ and $t\in[0,1]$, $p_Y(H(x,t))=p_X(x)$, and, for every $g\in E_G$ with $p_X(x)=p_G(g)$,

$$H(x\cdot g,t)=H(x,t)\cdot g.$$

No endpoint values are prescribed. Empty spaces and empty fibers are permitted.

QAlgorithms.Papers.Independent.Intakethird100.P73.EquivariantMap

Let $B$ be a compactly generated topological space, and let $G$ be a parametrized group over $B$: its compactly generated total space $E_G$ has a projection $p_G:E_G\to B$, a continuous unit section, a continuous inverse preserving the projection, and multiplication on pairs in the same fiber, continuous on the kification of that fiber product, satisfying the group laws in every fiber. Here kification keeps the underlying set and declares a subset open exactly when its inverse image under every continuous map from a compact Hausdorff space into the original space is open. Let $X$ and $Y$ be compactly generated spaces with continuous projections $p_X,p_Y$ to $B$ and right $G$-actions preserving these projections, continuous on the kified fiber products, and satisfying the unit and action associativity laws. An equivariant map from $X$ to $Y$ consists of a continuous function $f:X\to Y$ such that $p_Y(f(x))=p_X(x)$ for every $x$, together with the requirement

$$f(x\cdot g)=f(x)\cdot g \qquad \text{for every }x\in X,\ g\in E_G \text{ with }p_X(x)=p_G(g).$$

The spaces and their fibers need not be nonempty; conditions quantified over empty domains are vacuous.

QAlgorithms.Papers.Independent.Intakethird100.P73.EquivariantSpace

For any compactly generated topological space $B$, fix a parametrized group $G$ consisting of a compactly generated space $E$ with continuous projection $\pi_E:E\to B$, a continuous section $e:B\to E$, a continuous multiplication $m:\kappa(E\times_B E)\to E$ preserving the common projection, and a continuous inverse map $\iota:E\to E$ preserving projection, with $m(e(\pi_E(g)),g)=m(g,e(\pi_E(g)))=g$, $m(\iota(g),g)=m(g,\iota(g))=e(\pi_E(g))$ for every $g\in E$, and $m(m(g,h),k)=m(g,m(h,k))$ whenever $\pi_E(g)=\pi_E(h)=\pi_E(k)$; here $\pi_E(e(b))=b$ for every $b\in B$. For this fixed $G$, the structure consists of a compactly generated topological space $X$ with a continuous projection $\pi_X:X\to B$ and a continuous action $\alpha:\kappa(X\times_B E)\to X$ satisfying $\pi_X(\alpha(x,g))=\pi_X(x)$ for every pair with $\pi_X(x)=\pi_E(g)$, together with the identities

$$\alpha(x,e(\pi_X(x)))=x$$

for every $x\in X$, and

$$\alpha(\alpha(x,g),h)=\alpha(x,m(g,h))$$

for every $x\in X$ and $g,h\in E$ with $\pi_X(x)=\pi_E(g)$ and $\pi_E(g)=\pi_E(h)$. In this description, $E\times_B E=\{(g,h):\pi_E(g)=\pi_E(h)\}$ and $X\times_B E=\{(x,g):\pi_X(x)=\pi_E(g)\}$, initially with their ordinary product subspace topologies; for either such space $T$, $\kappa T$ has the same underlying set with $U\subseteq T$ open exactly when $s^{-1}(U)$ is open for every compact Hausdorff space $S$ in the fixed universe and every originally continuous map $s:S\to T$. Each multiplication or action is evaluated on a pair together with the required equality of projections. The space $X$ may be empty, in which case its action identities are vacuous.

QAlgorithms.Papers.Independent.Intakethird100.P73.EquivariantlyHomotopic

Let $B$ be a compactly generated topological space, $G$ a parametrized group over $B$, and $X,Y$ compactly generated right $G$-spaces over $B$. This means that $G$ has continuous projection, unit section and inverse and fiberwise group laws, while $X,Y$ have continuous projections and projection-preserving, unital, associative right actions; multiplication and actions are continuous on their kified fiber products. Write $K(T)$ for the same set as $T$, with a subset open exactly when its inverse image under every continuous compact Hausdorff probe into $T$ is open. For any continuous projection-preserving, action-preserving maps $f,g:X\to Y$, the assertion that they are equivariantly homotopic means that there exists a continuous

$$H:K(X\times[0,1])\longrightarrow Y$$

such that, for every $x\in X$ and $t\in[0,1]$,

$$H(x,0)=f(x),\qquad H(x,1)=g(x),\qquad p_Y(H(x,t))=p_X(x),$$

and $H(x\cdot a,t)=H(x,t)\cdot a$ for every $a\in E_G$ with $p_X(x)=p_G(a)$. No nonemptiness is assumed; if $X$ is empty, all the pointwise conditions are vacuous and the empty function supplies such a homotopy.

QAlgorithms.Papers.Independent.Intakethird100.P73.FiberProductSet

For any compactly generated topological space $B$ and any compactly generated topological spaces $X,Y$ equipped with continuous projections $\pi_X:X\to B$ and $\pi_Y:Y\to B$, this abbreviation denotes the subtype

$$\{(x,y)\in X\times Y:\pi_X(x)=\pi_Y(y)\}.$$

An element consists of a pair together with evidence that its two coordinates have equal projections. This subtype may be empty.

QAlgorithms.Papers.Independent.Intakethird100.P73.FiberwiseHomotopic

For any compactly generated topological space $B$, compactly generated topological spaces $X,Y$ with continuous projections $\pi_X:X\to B$, $\pi_Y:Y\to B$, and continuous maps $f,g:X\to Y$ satisfying $\pi_Y\circ f=\pi_X=\pi_Y\circ g$, this predicate means that there exists a continuous map $H:\kappa(X\times I)\to Y$, where $I=[0,1]$ has its usual topology and $\kappa(X\times I)$ has the same underlying set as the ordinary product, with a subset $U$ open exactly when $s^{-1}(U)$ is open for every compact Hausdorff space $S$ in the fixed universe and every continuous map $s:S\to X\times I$ for the ordinary product topology, such that

$$H(x,0)=f(x),\qquad H(x,1)=g(x),\qquad \pi_Y(H(x,t))=\pi_X(x)$$

for every $x\in X$ and every $t\in I$. There is no nonemptiness assumption on $X$; if $X$ is empty, the conditions are satisfied by the empty map.

QAlgorithms.Papers.Independent.Intakethird100.P73.GroupMapOver

Let $B$ be a compactly generated topological space and let $G,H$ be parametrized groups over $B$. Thus their compactly generated total spaces $E_G,E_H$ have continuous projections $p_G,p_H$, continuous unit sections $e_G,e_H$ satisfying $p_G(e_G(b))=p_H(e_H(b))=b$, continuous inverses preserving the projections, and multiplications defined on same-fiber pairs and satisfying the group laws in every fiber. These multiplications are continuous on the kifications of the fiber products, where kification declares a subset open exactly when its inverse image under every continuous map from a compact Hausdorff space into the original space is open. A group map over $B$ from $G$ to $H$ consists of a continuous $f:E_G\to E_H$ such that, for every $g\in E_G$, $p_H(f(g))=p_G(g)$, and such that

$$f(e_G(b))=e_H(b)\quad(b\in B),\qquad f(gh)=f(g)f(h)\quad \bigl(g,h\in E_G,\ p_G(g)=p_G(h)\bigr).$$

Preservation of inverses is not a separate field of the structure. The base may be empty; if it is nonempty, each group fiber contains its specified unit.

QAlgorithms.Papers.Independent.Intakethird100.P73.IsEquivariantFEquivalence

Let $B$ be a compactly generated topological space and $G$ a parametrized group over $B$: its compactly generated total space has continuous projection, unit section and inverse, with group multiplication in each fiber continuous on the kified fiber product. Let $X,Y$ be compactly generated spaces over $B$ carrying projection-preserving right $G$-actions, continuous on the kified fiber products and satisfying the unit and associativity laws. For a space $T$, let $K(T)$ have the same underlying set, with subsets open precisely when all continuous maps from compact Hausdorff spaces into $T$ have open inverse images. A continuous projection-preserving, action-preserving map $f:X\to Y$ is an equivariant $F$-equivalence exactly when there exist a continuous projection-preserving, action-preserving map $g:Y\to X$ and continuous maps

$$H_X:K(X\times[0,1])\to X,\qquad H_Y:K(Y\times[0,1])\to Y$$

with

$$H_X(x,0)=g(f(x)),\quad H_X(x,1)=x,\qquad H_Y(y,0)=f(g(y)),\quad H_Y(y,1)=y.$$

For all points and all $t\in[0,1]$, these maps preserve the base point and satisfy $H_X(x\cdot a,t)=H_X(x,t)\cdot a$ and $H_Y(y\cdot a,t)=H_Y(y,t)\cdot a$ whenever the indicated point and group element lie over the same base point. Neither uniqueness nor nonemptiness is required.

QAlgorithms.Papers.Independent.Intakethird100.P73.IsEquivariantFFibration

Let $B$ be a compactly generated topological space, $G$ a parametrized group over $B$, and $p:X\to Y$ a continuous projection-preserving, action-preserving map between compactly generated right $G$-spaces over $B$. Here the group has continuous projection, unit section and inverse and fiberwise group laws, the actions preserve projections and satisfy the unit and associativity laws, and multiplication and actions are continuous on the kified same-fiber pair spaces. Write $K(T)$ for the topology on the underlying set of $T$ whose open subsets are those having open inverse image under every continuous compact Hausdorff probe into $T$. The assertion that $p$ is an equivariant $F$-fibration means the following: for every such right $G$-space $Z$, every continuous projection-preserving, action-preserving map $a:Z\to X$, and every continuous map $H:K(Z\times[0,1])\to Y$ satisfying

$$p_Y(H(z,t))=p_Z(z),\qquad H(z\cdot g,t)=H(z,t)\cdot g,\qquad H(z,0)=p(a(z)),$$

where the action identity is required for all $z,g$ over the same base point and all $t\in[0,1]$, there exists a continuous $L:K(Z\times[0,1])\to X$ satisfying, for all $z,t$,

$$p_X(L(z,t))=p_Z(z),\qquad L(z,0)=a(z),\qquad p(L(z,t))=H(z,t),$$

and $L(z\cdot g,t)=L(z,t)\cdot g$ for all compatible $z,g,t$. Empty test spaces are included; the lift is not required to be unique.

QAlgorithms.Papers.Independent.Intakethird100.P73.IsEquivariantFiberwiseNDR

Let $B$ be a compactly generated topological space, $G$ a parametrized group over $B$, $X$ a compactly generated right $G$-space over $B$, and $A$ any subset of $X$. Explicitly, $G$ has continuous projection, unit section and inverse and fiberwise group multiplication, while $X$ has a continuous projection $p_X$ and a projection-preserving, unital, associative right action; multiplication and action are continuous on the kified fiber products. Let $K(T)$ denote the same set as $T$, with subsets open exactly when their inverse images under every continuous compact Hausdorff probe into $T$ are open. The assertion that $X,A$ satisfy the equivariant fiberwise NDR condition means that there exist a continuous function $u:X\to[0,1]$ and a continuous map $H:K(X\times[0,1])\to X$ such that $p_X(H(x,t))=p_X(x)$ for all $x,t$, and $H(x\cdot g,t)=H(x,t)\cdot g$ for every compatible $x,g$ and every $t$, with

$$x\in A\ \Longleftrightarrow\ u(x)=0,\qquad H(x,0)=x,\qquad H(x,t)=x\ \text{for }x\in A,\qquad u(x)<1\ \Longrightarrow\ H(x,1)\in A,$$

and $u(x\cdot g)=u(x)$ for every $x,g$ over the same base point. The endpoint inclusion is required only where $u(x)<1$. The subset $A$ is not separately assumed closed or invariant, and empty $X$ and empty $A$ are allowed.

QAlgorithms.Papers.Independent.Intakethird100.P73.IsEquivariantStrongFCofibration

Let $B$ be a compactly generated topological space, $G$ a parametrized group over $B$, and $i:A\to X$ a continuous projection-preserving, action-preserving map of compactly generated right $G$-spaces over $B$. The group has continuous projection, unit section and inverse and fiberwise group laws; the right actions preserve projections and satisfy the unit and associativity laws; multiplication and actions are continuous on kified fiber products. Write $K(T)$ for the same set as $T$, with $U$ open exactly when every continuous compact Hausdorff probe into $T$ has open inverse image of $U$. In this paragraph an equivariant map means a continuous map preserving the projection and satisfying $f(x\cdot g)=f(x)\cdot g$ for compatible pairs; an equivariant homotopy from $f$ to $g$ means a continuous $H:K(D\times[0,1])\to E$ preserving the projection and the action at every time, with $H(d,0)=f(d)$ and $H(d,1)=g(d)$. The assertion that $i$ is an equivariant strong $F$-cofibration means that for every pair $U,V$ of these right $G$-spaces and every equivariant $p:U\to V$ having both of the following properties—every equivariant $a_0:Z\to U$ and equivariant homotopy $H:K(Z\times[0,1])\to V$ with $H(z,0)=p(a_0(z))$, for every right $G$-space $Z$, admit an equivariant homotopy $L$ with $L(z,0)=a_0(z)$ and $p(L(z,t))=H(z,t)$; and there exists an equivariant $q:V\to U$ with equivariant homotopies from $q\circ p$ to $\operatorname{id}_U$ and from $p\circ q$ to $\operatorname{id}_V$—every pair of equivariant maps $a:A\to U$, $b:X\to V$ satisfying $p(a(z))=b(i(z))$ for all $z\in A$ admits an equivariant map $\ell:X\to U$ such that

$$\ell(i(z))=a(z)\quad(z\in A),\qquad p(\ell(x))=b(x)\quad(x\in X).$$

Neither injectivity of $i$ nor uniqueness of $\ell$ is part of this definition, and empty spaces are included.

QAlgorithms.Papers.Independent.Intakethird100.P73.IsFEquivalence

For any compactly generated topological space $B$, compactly generated topological spaces $X,Y$ with continuous projections $\pi_X:X\to B$, $\pi_Y:Y\to B$, and continuous map $f:X\to Y$ satisfying $\pi_Y\circ f=\pi_X$, this predicate means that there exist a continuous map $g:Y\to X$ satisfying $\pi_X\circ g=\pi_Y$ and continuous maps $H_X:\kappa(X\times I)\to X$ and $H_Y:\kappa(Y\times I)\to Y$, where $I=[0,1]$, such that

$$\begin{aligned} H_X(x,0)&=g(f(x)),& H_X(x,1)&=x,& \pi_X(H_X(x,t))&=\pi_X(x),\\ H_Y(y,0)&=f(g(y)),& H_Y(y,1)&=y,& \pi_Y(H_Y(y,t))&=\pi_Y(y) \end{aligned}$$

for all $x\in X$, $y\in Y$, and $t\in I$. Here, for either ordinary product $T=X\times I$ or $T=Y\times I$, $\kappa T$ has the same set as $T$, with $U\subseteq T$ open exactly when $s^{-1}(U)$ is open for every compact Hausdorff space $S$ in the fixed universe and every continuous map $s:S\to T$. The inverse and homotopies are required to exist but are not required to be unique; empty spaces are included in the quantification.

QAlgorithms.Papers.Independent.Intakethird100.P73.IsFFibration

For any compactly generated topological space $B$, compactly generated topological spaces $X,Y$ with continuous projections $\pi_X:X\to B$, $\pi_Y:Y\to B$, and continuous map $p:X\to Y$ satisfying $\pi_Y\circ p=\pi_X$, this predicate states the following lifting property. For every compactly generated topological space $Z$ with continuous projection $\pi_Z:Z\to B$, every continuous map $a:Z\to X$ satisfying $\pi_X\circ a=\pi_Z$, and every continuous map $H:\kappa(Z\times I)\to Y$, where $I=[0,1]$, if

$$\pi_Y(H(z,t))=\pi_Z(z)\quad\text{for all }z\in Z,\ t\in I, \qquad H(z,0)=p(a(z))\quad\text{for all }z\in Z,$$

then there exists a continuous map $L:\kappa(Z\times I)\to X$ such that

$$\pi_X(L(z,t))=\pi_Z(z),\qquad L(z,0)=a(z),\qquad p(L(z,t))=H(z,t)$$

for every $z\in Z$ and $t\in I$. Here $\kappa(Z\times I)$ has the ordinary product’s underlying set, with $U$ open exactly when $s^{-1}(U)$ is open for every compact Hausdorff space $S$ in the fixed universe and every continuous map $s:S\to Z\times I$ for the ordinary product topology. The quantification includes empty $Z$, for which the lifting conditions hold for the empty map.

QAlgorithms.Papers.Independent.Intakethird100.P73.IsGoodSimplicialGroup

For a compactly generated space $B$ and a simplicial parametrized group $G$ over $B$, this defines a property of every degeneracy map $s_i:G_n\to G_{n+1}$, for every integer $n\geq0$ and every $i\in\{0,\ldots,n\}$. Here $G$ assigns a parametrized group to each object of the opposite simplex category and a continuous map over $B$ preserving units and multiplication to each morphism, preserving identities and composition pointwise; each degree has a compactly generated total space $E_n\to B$, a continuous unit section, continuous inversion over $B$, and continuous multiplication on the compactly generated replacement of the pairs in the same fiber, satisfying the group laws in each fiber. The map $s_i$ is assigned to the opposite of the order-preserving surjection $[n+1]\to[n]$ that identifies $i$ and $i+1$. Write $I=[0,1]$, and let $k(T)$ retain the underlying set of $T$ with the finest topology making every originally continuous map from a compact Hausdorff space in the same universe continuous. A map over $B$ is continuous and commutes with projections, and a homotopy over $B$ from $f_0:S\to T$ to $f_1:S\to T$ is a continuous $F:k(S\times I)\to T$ with endpoints $f_0,f_1$ and $\pi_T(F(s,t))=\pi_S(s)$. The required property is that, for every $n,i$, every pair of compactly generated spaces $U,V$ over $B$, and every map $p:U\to V$ over $B$ satisfying the following two conditions, every commuting square with left side $s_i$ has a lift. The first condition on $p$ is that, for every compactly generated space $Z$ over $B$, map $c:Z\to U$ over $B$, and continuous $H:k(Z\times I)\to V$ with $\pi_V(H(z,t))=\pi_Z(z)$ and $H(z,0)=p(c(z))$, there is a continuous $L:k(Z\times I)\to U$ with $\pi_U(L(z,t))=\pi_Z(z)$, $L(z,0)=c(z)$, and $p(L(z,t))=H(z,t)$ for all $z,t$. The second condition is that some map $q:V\to U$ over $B$ admits homotopies over $B$ from $q\circ p$ to $\mathrm{id}_U$ and from $p\circ q$ to $\mathrm{id}_V$. Explicitly, every pair of maps $a:E_n\to U$ and $b:E_{n+1}\to V$ over $B$ with $p(a(x))=b(s_i(x))$ for every $x\in E_n$ must admit a map $\ell:E_{n+1}\to U$ over $B$ with $\ell(s_i(x))=a(x)$ for every $x\in E_n$ and $p(\ell(y))=b(y)$ for every $y\in E_{n+1}$. The quantifiers include $n=0$, where $i=0$, and impose no nonemptiness assumptions.

QAlgorithms.Papers.Independent.Intakethird100.P73.IsStrongFCofibration

For any compactly generated topological space $B$, compactly generated topological spaces $A,X$ with continuous projections $\pi_A:A\to B$, $\pi_X:X\to B$, and continuous map $i:A\to X$ satisfying $\pi_X\circ i=\pi_A$, this predicate states that the following holds for every pair of compactly generated topological spaces $U,V$ with continuous projections $\pi_U:U\to B$, $\pi_V:V\to B$, and every continuous map $p:U\to V$ satisfying $\pi_V\circ p=\pi_U$. Suppose, first, that for every compactly generated space $Z$ with continuous projection $\pi_Z:Z\to B$, every continuous $c:Z\to U$ with $\pi_U\circ c=\pi_Z$, and every continuous $H:\kappa(Z\times I)\to V$ satisfying $\pi_V(H(z,t))=\pi_Z(z)$ and $H(z,0)=p(c(z))$, there exists a continuous $L:\kappa(Z\times I)\to U$ satisfying $\pi_U(L(z,t))=\pi_Z(z)$, $L(z,0)=c(z)$, and $p(L(z,t))=H(z,t)$, for all $z\in Z,t\in I$. Suppose, second, that there exist a continuous $q:V\to U$ with $\pi_U\circ q=\pi_V$ and continuous maps $K_U:\kappa(U\times I)\to U$, $K_V:\kappa(V\times I)\to V$ satisfying $K_U(u,0)=q(p(u))$, $K_U(u,1)=u$, $\pi_U(K_U(u,t))=\pi_U(u)$, $K_V(v,0)=p(q(v))$, $K_V(v,1)=v$, and $\pi_V(K_V(v,t))=\pi_V(v)$, for all $u\in U,v\in V,t\in I$. Under these two suppositions, for every continuous $a:A\to U$ and $b:X\to V$ satisfying $\pi_U\circ a=\pi_A$, $\pi_V\circ b=\pi_X$, and $p(a(z))=b(i(z))$ for all $z\in A$, there exists a continuous $l:X\to U$ satisfying

$$\pi_U(l(x))=\pi_X(x),\qquad l(i(z))=a(z),\qquad p(l(x))=b(x)$$

for all $z\in A,x\in X$. Throughout, $I=[0,1]$, and $\kappa(T\times I)$ denotes the ordinary product’s underlying set with $W$ open exactly when $s^{-1}(W)$ is open for every compact Hausdorff space $S$ in the fixed universe and every ordinarily continuous $s:S\to T\times I$. All quantified spaces may be empty, and the requirement on a particular $p$ is conditional on both suppositions holding.

QAlgorithms.Papers.Independent.Intakethird100.P73.IsWeaklyHausdorff

For a KSpace $B$, meaning a type in universe $u$ equipped with a compactly generated topology, this defines the property that, for every compact Hausdorff space $S$ in universe $u$ and every continuous map $f:S\to B$, the image $f(S)=\{f(s)\mid s\in S\}$ is closed in $B$. Empty compact Hausdorff domains are included, in which case the image is empty; the property also permits $B$ itself to be empty.

QAlgorithms.Papers.Independent.Intakethird100.P73.IsWellSectioned

For a compactly generated space $B$ and a parametrized group $G$ over $B$, with compactly generated total space $E$, continuous projection $\pi:E\to B$, continuous unit section $e:B\to E$, continuous fiberwise inversion, and continuous fiberwise multiplication satisfying the group laws, this defines the following property of $e$. Write $I=[0,1]$, and write $k(T)$ for the underlying set of a topological space $T$ equipped with the finest topology making every originally continuous map from a compact Hausdorff space in the same universe continuous; in particular, the multiplication of $G$ is continuous on $k(\{(g,h)\in E\times E:\pi(g)=\pi(h)\})$. A map over $B$ means a continuous map commuting with the specified projections to $B$, and a homotopy over $B$ from $f_0:S\to T$ to $f_1:S\to T$ means a continuous $F:k(S\times I)\to T$ such that $F(s,0)=f_0(s)$, $F(s,1)=f_1(s)$, and $\pi_T(F(s,t))=\pi_S(s)$ for all $s,t$. The property is that, for every pair of compactly generated spaces $U,V$ over $B$ and every map $p:U\to V$ over $B$ satisfying both of the following conditions, every commuting square with left side $e$ has a lift: first, for every compactly generated space $Z$ over $B$, every map $c:Z\to U$ over $B$, and every continuous $H:k(Z\times I)\to V$ with $\pi_V(H(z,t))=\pi_Z(z)$ and $H(z,0)=p(c(z))$, there exists a continuous $L:k(Z\times I)\to U$ with $\pi_U(L(z,t))=\pi_Z(z)$, $L(z,0)=c(z)$, and $p(L(z,t))=H(z,t)$ for all $z,t$; second, there exists a map $q:V\to U$ over $B$ with homotopies over $B$ from $q\circ p$ to $\mathrm{id}_U$ and from $p\circ q$ to $\mathrm{id}_V$. Explicitly, for every map $a:B\to U$ over $B$ and every map $b:E\to V$ over $B$ such that $p(a(s))=b(e(s))$ for every $s\in B$, there must exist a map $\ell:E\to U$ over $B$ such that $\ell(e(s))=a(s)$ for every $s\in B$ and $p(\ell(x))=b(x)$ for every $x\in E$. No nonemptiness assumptions are imposed.

QAlgorithms.Papers.Independent.Intakethird100.P73.KSpace

A KSpace consists of a type $X$ in universe $u$, a topology on $X$, and a proof that $X$ with that topology is compactly generated. The underlying type is allowed to be empty.

QAlgorithms.Papers.Independent.Intakethird100.P73.MapOver

For every base $B$ equipped with a compactly generated topology and every two spaces over it, consisting of compactly generated spaces $E_X,E_Y$ with continuous projections $p_X:E_X\to B$ and $p_Y:E_Y\to B$, a MapOver from the first to the second consists of a continuous map $f:E_X\to E_Y$ and a proof that $p_Y(f(x))=p_X(x)$ for every $x\in E_X$. When $E_X$ is empty, this equality condition is vacuous.

QAlgorithms.Papers.Independent.Intakethird100.P73.ParametrizedGroup

For a compactly generated topological space $B$, this structure consists of a compactly generated topological space $E$ with a continuous projection $\pi:E\to B$; a continuous map $e:B\to E$ satisfying $\pi(e(b))=b$ for every $b\in B$; a continuous multiplication $m:\kappa P\to E$, where $P=\{(g,h)\in E\times E:\pi(g)=\pi(h)\}$, satisfying $\pi(m(g,h))=\pi(g)$ for every $(g,h)\in P$; and a continuous map $\iota:E\to E$ satisfying $\pi(\iota(g))=\pi(g)$ for every $g\in E$. Here $P$ initially carries the product subspace topology, and $\kappa P$ has the same underlying set, with $U\subseteq P$ open exactly when $s^{-1}(U)$ is open for every compact Hausdorff space $S$ in the fixed universe and every continuous map $s:S\to P$ for that subspace topology. These data must satisfy

$$m(e(\pi(g)),g)=g,\qquad m(g,e(\pi(g)))=g,\qquad m(\iota(g),g)=e(\pi(g)),\qquad m(g,\iota(g))=e(\pi(g))$$

for every $g\in E$, and

$$m(m(g,h),k)=m(g,m(h,k))$$

for every $g,h,k\in E$ with $\pi(g)=\pi(h)$ and $\pi(h)=\pi(k)$. Each occurrence of $m$ is applied to the indicated pair together with the equality of its projections. The section $e$ supplies an element in every fiber over a point of $B$; the base $B$ itself is allowed to be empty.

QAlgorithms.Papers.Independent.Intakethird100.P73.SimplicialParametrizedGroup

For a compactly generated topological space $B$, a simplicial parametrized group over $B$ consists of a parametrized group $G_a$ over $B$ for every object $a$ of the opposite simplex category, and a group map over $B$, denoted $G(\alpha):G_a\to G_b$, for every arrow $\alpha:a\to b$ in that category. The simplex category has the nonempty finite ordered sets $[n]=\{0,\ldots,n\}$, for all natural numbers $n$, including $n=0$, and order-preserving maps; taking its opposite reverses the arrows. Each $G_a$ has a compactly generated total space $E_a$, continuous projection $p_a:E_a\to B$, continuous unit section and inverse, and fiberwise group multiplication continuous on the kified fiber product and satisfying the group laws. Here kification gives the original underlying set the topology whose open subsets have open inverse image under every continuous compact Hausdorff probe into the original space. Each $G(\alpha)$ is continuous, preserves the projection to $B$, sends each fiber unit to the corresponding fiber unit, and preserves products of elements lying in the same fiber. The required identity and composition laws are the pointwise equalities

$$G(\operatorname{id}_a)(x)=x \quad(a,\ x\in E_a), \qquad G(\beta\circ\alpha)(x)=G(\beta)(G(\alpha)(x))$$

for every triple of objects $a,b,c$, every $\alpha:a\to b$, every $\beta:b\to c$, and every $x\in E_a$. The base is not required to be nonempty.

QAlgorithms.Papers.Independent.Intakethird100.P73.SpaceOver

For every base $B$ that is a type in universe $u$ equipped with a compactly generated topology, a SpaceOver $B$ consists of another type $E$ in universe $u$ equipped with a compactly generated topology and a continuous map $p:E\to B$. The total space $E$ may be empty; if $B$ is empty, the existence of $p$ forces $E$ to be empty.

QAlgorithms.Papers.Independent.Intakethird100.P73.baseOver

For every compactly generated space $B$, this defines a space over $B$ whose total space is $B$ itself and whose continuous projection to $B$ is the identity $b\mapsto b$. There is no nonemptiness assumption on $B$.

QAlgorithms.Papers.Independent.Intakethird100.P73.composeOver

For any compactly generated topological space $B$, let $X,Y,Z$ be compactly generated topological spaces with continuous projections $\pi_X:X\to B$, $\pi_Y:Y\to B$, and $\pi_Z:Z\to B$. Given continuous maps $f:X\to Y$ and $g:Y\to Z$ satisfying $\pi_Y(f(x))=\pi_X(x)$ for every $x\in X$ and $\pi_Z(g(y))=\pi_Y(y)$ for every $y\in Y$, this definition gives the continuous map $g\circ f:X\to Z$ over $B$, whose value at $x$ is $g(f(x))$ and whose projection satisfies $\pi_Z(g(f(x)))=\pi_X(x)$.

QAlgorithms.Papers.Independent.Intakethird100.P73.constantSimplicialGroup

For any compactly generated space $B$ and parametrized group $G$ over $B$, this defines a constant simplicial parametrized group. Here $G$ consists of a compactly generated total space $E$, a continuous projection $\pi:E\to B$, a continuous unit section $e:B\to E$ with $\pi(e(b))=b$, a continuous inverse over $B$, and a multiplication over $B$ defined on the compactly generated replacement of $\{(g,h)\in E\times E:\pi(g)=\pi(h)\}$, satisfying the unit, inverse, and associativity laws in each fiber. The compactly generated replacement retains the underlying set and uses the finest topology making every originally continuous map from a compact Hausdorff space in the same universe continuous. The constructed simplicial object assigns this same $G$ to every object of the opposite simplex category and assigns the identity map of $E$, over $B$ and preserving units and multiplication, to every morphism. Its identity and composition laws hold pointwise because all these maps are identities.

QAlgorithms.Papers.Independent.Intakethird100.P73.equivariantCompose

Let $B$ be a compactly generated topological space and $G$ a parametrized group over $B$, meaning a compactly generated total space with a continuous projection to $B$, continuous unit section and inverse, and fiberwise group multiplication continuous on the kified fiber product. Let $X,Y,Z$ be compactly generated spaces over $B$ with projection-preserving right $G$-actions satisfying the unit and associativity laws and continuous on the corresponding kified fiber products. Kification gives a space the topology in which a subset is open exactly when its inverse image under every continuous compact Hausdorff probe into the original space is open. For any continuous projection-preserving, action-preserving maps $f:X\to Y$ and $g:Y\to Z$, this defines their equivariant composite $g\circ f:X\to Z$ by

$$(g\circ f)(x)=g(f(x)).$$

It preserves the projection, $p_Z(g(f(x)))=p_X(x)$, and for every $x\in X$ and $a\in E_G$ with $p_X(x)=p_G(a)$, it satisfies $g(f(x\cdot a))=g(f(x))\cdot a$. No nonemptiness assumptions are imposed.

QAlgorithms.Papers.Independent.Intakethird100.P73.equivariantIdentity

For every compactly generated topological space $B$, every parametrized group $G$ over $B$, and every right $G$-space $X$ over $B$, this defines the equivariant identity map $X\to X$ by $x\mapsto x$. Explicitly, $G$ has a compactly generated total space over $B$, a continuous unit section and inverse, and fiberwise group multiplication continuous on the kified fiber product; $X$ is compactly generated with a continuous projection $p_X:X\to B$ and a projection-preserving right action satisfying the unit and associativity laws and continuous on the kified same-fiber pairs. Kification means that a subset is open precisely when every continuous map from a compact Hausdorff space into the original space has open inverse image of that subset. The defined map is continuous, satisfies $p_X(x)=p_X(x)$, and preserves the action because

$$\operatorname{id}_X(x\cdot g)=\operatorname{id}_X(x)\cdot g$$

for every $x,g$ lying over the same point of $B$. This definition also applies when $B$ or $X$ is empty.

QAlgorithms.Papers.Independent.Intakethird100.P73.fiberPair

For any compactly generated topological space $B$, compactly generated topological spaces $X,Y$ with continuous projections $\pi_X:X\to B$, $\pi_Y:Y\to B$, points $x\in X$, $y\in Y$, and evidence $h$ that $\pi_X(x)=\pi_Y(y)$, this definition returns the element represented by $(x,y)$, together with that evidence, in the space whose underlying set is $P=\{(x',y')\in X\times Y:\pi_X(x')=\pi_Y(y')\}$. Its topology is the compactly generated refinement of the ordinary product subspace topology: $U\subseteq P$ is open exactly when $s^{-1}(U)$ is open for every compact Hausdorff space $S$ in the fixed universe and every map $s:S\to P$ continuous for that subspace topology. Its projection to $B$ sends $(x',y')$ to $\pi_X(x')$.

QAlgorithms.Papers.Independent.Intakethird100.P73.fiberProductMap

For any compactly generated topological space $B$, let $A,X,D,Y$ be compactly generated topological spaces with continuous projections $\pi_A,\pi_X,\pi_D,\pi_Y$ to $B$, and let $f:A\to X$ and $g:D\to Y$ be continuous maps satisfying $\pi_X\circ f=\pi_A$ and $\pi_Y\circ g=\pi_D$. Put $P=\{(a,d)\in A\times D:\pi_A(a)=\pi_D(d)\}$ and $Q=\{(x,y)\in X\times Y:\pi_X(x)=\pi_Y(y)\}$, initially with their product subspace topologies. For either such space $T$, write $\kappa T$ for the same set with the topology in which $U\subseteq T$ is open exactly when $s^{-1}(U)$ is open for every compact Hausdorff space $S$ in the fixed universe and every originally continuous map $s:S\to T$. This definition gives the continuous map over $B$

$$\kappa P\longrightarrow\kappa Q,\qquad(a,d)\longmapsto(f(a),g(d)).$$

The projections of these spaces to $B$ are respectively $(a,d)\mapsto\pi_A(a)$ and $(x,y)\mapsto\pi_X(x)$, and preservation of the projection is the equality $\pi_X(f(a))=\pi_A(a)$.

QAlgorithms.Papers.Independent.Intakethird100.P73.fiberProductOver

For any compactly generated topological space $B$ and compactly generated topological spaces $X,Y$ with continuous projections $\pi_X:X\to B$ and $\pi_Y:Y\to B$, form $P=\{(x,y)\in X\times Y:\pi_X(x)=\pi_Y(y)\}$, initially with the subspace topology inherited from the product. This definition gives a space over $B$ whose underlying set is $P$, whose topology is its compactly generated refinement, and whose continuous projection sends $(x,y)$ to $\pi_X(x)$. Explicitly, a subset $U\subseteq P$ is open in this refined topology exactly when $s^{-1}(U)$ is open for every compact Hausdorff space $S$ in the fixed universe and every map $s:S\to P$ continuous for the original subspace topology. The projection is the original first-coordinate projection composed with the continuous identity map from this refined space to the original $P$. The construction also applies when $P$ is empty.

QAlgorithms.Papers.Independent.Intakethird100.P73.fiberProductSetMap

For any compactly generated topological space $B$, let $A,X,D,Y$ be compactly generated topological spaces with continuous projections $\pi_A,\pi_X,\pi_D,\pi_Y$ to $B$. Given continuous maps $f:A\to X$ and $g:D\to Y$ satisfying $\pi_X(f(a))=\pi_A(a)$ for every $a\in A$ and $\pi_Y(g(d))=\pi_D(d)$ for every $d\in D$, this definition gives the continuous map

$$\{(a,d)\in A\times D:\pi_A(a)=\pi_D(d)\} \longrightarrow \{(x,y)\in X\times Y:\pi_X(x)=\pi_Y(y)\}, \qquad (a,d)\longmapsto(f(a),g(d)),$$

where both subtypes carry their ordinary product subspace topologies. Membership of the output follows from $\pi_X(f(a))=\pi_A(a)=\pi_D(d)=\pi_Y(g(d))$.

QAlgorithms.Papers.Independent.Intakethird100.P73.groupUnitSection

For every compactly generated space $B$ and parametrized group $G$ over $B$, this defines a continuous map over $B$ from $B$, equipped with its identity projection, to the total space $E$ of $G$. A parametrized group here has a continuous projection $\pi:E\to B$ from a compactly generated total space, a continuous unit section $e:B\to E$, continuous inversion over $B$, and continuous multiplication over $B$ on the compactly generated replacement of the space of pairs in the same fiber, with the group laws holding in each fiber. That replacement retains the underlying set and uses the finest topology making every originally continuous map from a compact Hausdorff space in the same universe continuous. The defined map is exactly $b\mapsto e(b)$; the condition that it is over $B$ is the given equality $\pi(e(b))=b$ for every $b\in B$.

QAlgorithms.Papers.Independent.Intakethird100.P73.identityOver

For every base $B$ equipped with a compactly generated topology and every space over it, consisting of a compactly generated space $E$ and a continuous projection $p:E\to B$, this defines a map from that space over $B$ to itself whose underlying continuous function is $\operatorname{id}_E$. Its required compatibility with the projection is $p(\operatorname{id}_E(x))=p(x)$ for every $x\in E$; the construction also applies when $E$ is empty.

QAlgorithms.Papers.Independent.Intakethird100.P73.kSpaceCoeSort

This instance allows any KSpace—a type in universe $u$ equipped with a compactly generated topology—to be used as a type, in which case it denotes its underlying carrier type.

QAlgorithms.Papers.Independent.Intakethird100.P73.kSpaceCompactlyGenerated

For every KSpace $X$, consisting of a carrier type equipped with a topology and a proof of compact generation, this instance supplies the fact that the underlying type with its stored topology is compactly generated, using the proof stored in $X$.

QAlgorithms.Papers.Independent.Intakethird100.P73.kSpaceTopology

For every KSpace $X$, consisting of a carrier type, a topology, and a proof that this topology is compactly generated, this instance equips the underlying type of $X$ with exactly the topology stored in $X$.

QAlgorithms.Papers.Independent.Intakethird100.P73.kify

For every type $X$ in universe $u$ equipped with a topology, this defines a KSpace with underlying type $X$ and the following topology: a subset $U\subseteq X$ is open precisely when $f^{-1}(U)$ is open for every compact Hausdorff space $S$ in universe $u$ and every map $f:S\to X$ continuous for the original topology on $X$. Equivalently, this is the final topology of the evaluation map from the disjoint union of all such domains indexed by pairs $(S,f)$, sending the point indexed by $(S,f,s)$ to $f(s)$. The construction includes a proof that this topology is compactly generated and applies also when $X$ is empty.

QAlgorithms.Papers.Independent.Intakethird100.P73.kifyMap

For every pair of types $X,Y$ in universe $u$, each equipped with a topology, and every continuous map $f:X\to Y$, this defines a continuous map with underlying function $f$ after replacing both topologies as follows: for either space $Z$, a subset $U\subseteq Z$ is open in the replacement topology exactly when $g^{-1}(U)$ is open for every compact Hausdorff space $S$ in universe $u$ and every map $g:S\to Z$ continuous for the original topology. The construction includes empty spaces whenever the supplied map $f$ exists.

QAlgorithms.Papers.Independent.Intakethird100.P73.kifyProbe

For every type $X$ in universe $u$ equipped with a topology, every compact Hausdorff space $S$ in universe $u$, and every continuous map $f:S\to X$, this defines a continuous map with the same underlying function $f$ from $S$ to the underlying set $X$ equipped with the topology in which $U\subseteq X$ is open exactly when $g^{-1}(U)$ is open for every compact Hausdorff space $T$ in universe $u$ and every originally continuous map $g:T\to X$. Empty domains are included; if $X$ is empty, the given function $f$ can exist only when $S$ is empty.

QAlgorithms.Papers.Independent.Intakethird100.P73.kifyProjection

For every type $X$ in universe $u$ equipped with a topology $\mathcal T$, this defines a continuous map whose underlying function is the identity on $X$, from $X$ equipped with the topology in which $U$ is open exactly when $f^{-1}(U)$ is open for every compact Hausdorff space $S$ in universe $u$ and every $\mathcal T$-continuous map $f:S\to X$, to $X$ equipped with its original topology $\mathcal T$. No nonemptiness assumption on $X$ is imposed.