nLab underlying type of free infinity-group

Idea

In dependent type theory with uniqueness of identity proofs, the free group on a type $A$ is the (higher) inductive type generated by an element $\mathrm{unit}:\mathrm{FreeGroup}(A)$ and a function $\mathrm{gen}:A \to (\mathrm{FreeGroup}(A) \simeq \mathrm{FreeGroup}(A))$. However, in dependent type theory without uniqueness of identity proofs, the resulting type is no longer a free group, because the resulting type is no longer 0-truncated. Instead, it is the underlying type of the free $\infty$-group on a type $A$, and denoted as $\mathrm{UTFIG}(A)$. Nonetheless, the underlying type of the free infinity group on a set $A$ is a group.

This is the invertible version of the type of lists $\mathrm{List}(A)$ on a type $A$, which in the context of uniqueness of identity proofs is the free monoid on a type $A$, but without uniqueness of identity proofs is the underlying type of the free $A_\infty$-space on a type $A$; i.e. a free monoid in a monoidal (infinity,1)-category, and $\infty$-groups are the invertible versions of $A_\infty$-spaces.

Definitions

Assuming that identification types, equivalence types and dependent product types exist in the type theory, the underlying type of the free infinity-group on a type $A$ of generators is the (higher) inductive type $\mathrm{UTFIG}(A)$ generated by an element $\mathrm{unit}:\mathrm{UTFIG}(A)$ and a function $\mathrm{gen}:A \to (\mathrm{UTFIG}(A) \simeq \mathrm{UTFIG}(A))$:

Formation rules for the underlying type of the free infinity-group:

$$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{UTFIG} \; \mathrm{type}}$$

Introduction rules for the underlying type of the free infinity-group:

$$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{unit}:\mathrm{UTFIG}(A)} \qquad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{gen}:A \to (\mathrm{UTFIG}(A) \simeq \mathrm{UTFIG}(A))}$$

Elimination rules for the underlying type of the free infinity-group:

$$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:\mathrm{UTFIG}(A) \vdash C(x) \; \mathrm{type} \\ \Gamma \vdash c_\mathrm{unit}:C(\mathrm{unit}) \quad \Gamma \vdash c_\mathrm{gen}:\prod_{a:A} \prod_{x:\mathrm{UTFIG}(A)} C(x) \simeq C(\mathrm{gen}(a)(x)) \\ \Gamma \vdash g:\mathrm{UTFIG}(A)) \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{UTFIG}(A)}^C(c_\mathrm{unit}, c_\mathrm{gen}, g):C(g)}$$

Computation rules for the underlying type of the free infinity-group:

• Judgmental computation rules

$$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:\mathrm{UTFIG}(A) \vdash C(x) \; \mathrm{type} \\ \Gamma \vdash c_\mathrm{unit}:C(\mathrm{unit}) \quad \Gamma \vdash c_\mathrm{gen}:\prod_{a:A} \prod_{x:\mathrm{UTFIG}(A))} C(x) \simeq C(\mathrm{gen}(a)(x)) \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{UTFIG}(A)}^C(c_\mathrm{unit}, c_\mathrm{gen}, 0) \equiv c_\mathrm{unit}:C(\mathrm{unit})}$$

$$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:\mathrm{UTFIG}(A) \vdash C(x) \; \mathrm{type} \\ \Gamma \vdash c_\mathrm{unit}:C(\mathrm{unit}) \quad \Gamma \vdash c_\mathrm{gen}:\prod_{a:A} \prod_{x:\mathrm{UTFIG}(A))} C(x) \simeq C(\mathrm{gen}(a)(x)) \\ \Gamma \vdash b:A \quad \Gamma \vdash g:\mathrm{UTFIG}(A)) \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{UTFIG}(A)}^C(c_\mathrm{unit}, c_\mathrm{gen}, \mathrm{gen}(b)(g)) \equiv c_\mathrm{gen}(b)(g)(\mathrm{ind}_{\mathrm{UTFIG}(A)}^C(c_\mathrm{unit}, c_\mathrm{gen}, g)):C(\mathrm{gen}(b)(g))}$$

• Typal computation rules

$$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:\mathrm{UTFIG}(A) \vdash C(x) \; \mathrm{type} \\ \Gamma \vdash c_\mathrm{unit}:C(\mathrm{unit}) \quad \Gamma \vdash c_\mathrm{gen}:\prod_{a:A} \prod_{x:\mathrm{UTFIG}(A))} C(x) \simeq C(\mathrm{gen}(a)(x)) \end{array} }{\Gamma \vdash \beta_{\mathrm{UTFIG}(A)}^\mathrm{unit}(c_\mathrm{unit}, c_\mathrm{gen}):\mathrm{Id}_{C(\mathrm{unit})}(\mathrm{ind}_{\mathrm{UTFIG}(A)}^C(c_\mathrm{unit}, c_\mathrm{gen}, 0), c_\mathrm{unit})}$$

$$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:\mathrm{UTFIG}(A) \vdash C(x) \; \mathrm{type} \\ \Gamma \vdash c_\mathrm{unit}:C(\mathrm{unit}) \quad \Gamma \vdash c_\mathrm{gen}:\prod_{a:A} \prod_{x:\mathrm{UTFIG}(A))} C(x) \simeq C(\mathrm{gen}(a)(x)) \\ \Gamma \vdash b:A \quad \Gamma \vdash g:\mathrm{UTFIG}(A)) \end{array} }{\Gamma \vdash \beta_{\mathrm{UTFIG}(A)}^\mathrm{gen}(c_\mathrm{unit}, c_\mathrm{gen}, b, g):\mathrm{Id}_{C(\mathrm{gen}(b)(g))}(\mathrm{ind}_{\mathrm{UTFIG}(A)}^C(c_\mathrm{unit}, c_\mathrm{gen}, \mathrm{gen}(b)(g)), c_\mathrm{gen}(b)(g)(\mathrm{ind}_{\mathrm{UTFIG}(A)}^C(c_\mathrm{unit}, c_\mathrm{gen}, g)))}$$

Uniqueness rules for the underlying type of the free infinity-group:

• Judgmental uniqueness rules

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:\mathrm{UTFIG}(A) \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c:\prod_{x:\mathrm{UTFIG}(A)} C(x) \quad \Gamma \vdash g:\mathrm{UTFIG}(A)}{\Gamma \vdash \mathrm{ind}_{\mathrm{UTFIG}(A)}^C(c(\mathrm{unit}), \lambda a:A.\lambda x:\mathrm{UTFIG}(A).c(\mathrm{gen}(a)(x)), g) \equiv c(g):C(g)}$$

• Typal uniqueness rules

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:\mathrm{UTFIG}(A) \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c:\prod_{x:\mathrm{UTFIG}(A)} C(x) \quad \Gamma \vdash g:\mathrm{UTFIG}(A)}{\Gamma \vdash \eta_{\mathrm{UTFIG}(A)}(c, n):\mathrm{Id}_{C(g)}(\mathrm{ind}_{\mathrm{UTFIG}(A)}^C(c(\mathrm{unit}), \lambda a:A.\lambda x:\mathrm{UTFIG}(A).c(\mathrm{gen}(a)(x)), g), c(g))}$$

The elimination, typal computation, and typal uniqueness rules for the underlying type of the free infinity-group state that the underlying type of the free infinity-group satisfy the dependent universal property of the underlying type of the free infinity-group. If the dependent type theory also has dependent sum types and product types, allowing one to define the uniqueness quantifier, the dependent universal property of the underlying type of the free infinity-group could be simplified to the following rule:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:\mathrm{UTFIG}(A) \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_\mathrm{unit}:C(\mathrm{unit}) \quad \Gamma \vdash c_\mathrm{gen}:\prod_{a:A} \prod_{x:\mathrm{UTFIG}(A))} C(x) \simeq C(\mathrm{gen}(a)(x))}{\Gamma \vdash \mathrm{up}_\mathbb{Z}^C(c_\mathrm{unit}, c_\mathrm{gen}):\exists!c:\prod_{x:\mathrm{UTFIG}(A))} C(x).\mathrm{Id}_{C(\mathrm{unit})}(c(\mathrm{unit}), c_\mathrm{unit}) \times \prod_{a:A} \prod_{x:\mathrm{UTFIG}(A)} \mathrm{Id}_{C(\mathrm{gen}(a)(x))}(c(\mathrm{gen}(a)(x)), c_\mathrm{gen}(a)(c(x)))}$$

Properties

H-space structure on the underlying type of the free infinity-group

Definition

The binary operation $\mu$ on the underlying type of the free infinity-group is defined by induction on the underlying type of the free infinity-group

Introduction rules for $\mu$:

$$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:\mathrm{UTFIG}(A) \vdash \mu(x):\mathrm{UTFIG}(A) \simeq \mathrm{UTFIG}(A)}$$

By uncurrying the equivalence of types one gets the binary operation

$$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:\mathrm{UTFIG}(A), y:\mathrm{UTFIG}(A) \vdash \mu(x, y):\mathrm{UTFIG}(A)}$$

Computation rules for $\mu$:

$$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, g:\mathrm{UTFIG}(A) \vdash \beta_{\mathrm{UTFIG}(A)}^{\mu, \mathrm{unit}}(g):\mu(\mathrm{unit})(g) =_{\mathrm{UTFIG}(A)} g}$$

$$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, x:\mathrm{UTFIG}(A), g:\mathrm{UTFIG}(A) \vdash \beta_\mathbb{Z}^{\mu, \mathrm{gen}}(a, x, g):\mu(\mathrm{gen}(a)(x))(g) =_\mathbb{Z} \mathrm{gen}(a)(\mu(x, g))}$$

Theorem

The underlying type of the free infinity-group of $A$ is a non-coherent H-space with respect to the unit $\mathrm{unit}:\mathrm{UTFIG}(A)$ found in the introduction rule of the underlying type of the free-infinity group and the binary operation $x:\mathrm{UTFIG}(A), y:\mathrm{UTFIG}(A) \vdash \mu(x)(y):\mathrm{UTFIG}(A)$ defined above.

Proof

The left homotopy comes from the computation laws for the operation $\mu$ expressed above.

$$\lambda x:\mathrm{UTFIG}(A).\beta_{\mathrm{UTFIG}(A)}^{\mu, \mathrm{unit}}(x):\prod_{x:\mathrm{UTFIG}(A)} \mu(\mathrm{unit})(x) =_{\mathrm{UTFIG}(x)} g$$

It remains to construct the right homotopy

See also

• free group

• infinity-group

• list (non-invertible version)

• A-infinity space

• integers type (underlying type of the free infinity-group on the unit type