nLab copy

 Idea

In dependent type theory, given a type $A$, one could define a type $\mathrm{Copy}(A)$ called a copy of $A$, which is equivalent to $A$.

Definitions

There are two ways to define the copy $\mathrm{Copy}(A)$ of a type $A$, as a positive type or as a negative type

Copies as a positive type

Copies as positive types are also called unary sum types or positive unary product types.

Assuming that identification types, function types and dependent product types exist in the type theory, the copy of type $A$ is the inductive type generated by a function from $A$ to $\mathrm{Copy}(A)$:

Formation rules for copies:

$$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{Copy}(A) \; \mathrm{type}}$$

Introduction rules for copies:

$$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{copy}_A:A \to \mathrm{Copy}(A)}$$

Elimination rules for copies:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:\mathrm{Copy}(A) \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_{\mathrm{copy}_A}:\prod_{x:A} C(\mathrm{copy}_A(x)) \quad \Gamma \vdash y:\mathrm{Copy}(A)}{\Gamma \vdash \mathrm{ind}_{\mathrm{Copy}(A)}^C(c_{\mathrm{copy}_A}, y):C(y)}$$

Computation rules for copies:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:\mathrm{Copy}(A) \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_{\mathrm{copy}_A}:\prod_{x:A} C(\mathrm{copy}_A(x)) \quad \Gamma \vdash x:A}{\Gamma \vdash \beta_{\mathrm{Copy}(A)}^{\mathrm{copy}_A}(c_{\mathrm{copy}_A}, x):\mathrm{Id}_{C(\mathrm{copy}_A(x))}(\mathrm{ind}_{\mathrm{Copy}(A)}^C(c_{\mathrm{copy}_A}, \mathrm{copy}_A(x)), c(x))}$$

Uniqueness rules for copies:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:\mathrm{Copy}(A) \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c:\prod_{x:\mathrm{Copy}(A)} C(x) \quad \Gamma \vdash y:\mathrm{Copy}(A)}{\Gamma \vdash \eta_{\mathrm{Copy}(A)}(c, y):\mathrm{Id}_{C(y)}(\mathrm{ind}_{\mathrm{Copy}(A)}^C(c_{\mathrm{copy}_A}, y), c(y))}$$

The elimination, computation, and uniqueness rules for the copy of $A$ state that the copy of $A$ and $B$ satisfy the dependent universal property of the copy of $A$ and $B$. If the dependent type theory also has dependent sum types, allowing one to define the uniqueness quantifier, the dependent universal property of the copy of $A$ could be simplified to the following rule:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:\mathrm{Copy}(A) \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_{\mathrm{copy}_A}:\prod_{x:A} C(\mathrm{copy}_A(x))}{\Gamma \vdash \mathrm{up}_{\mathrm{Copy}(A)}^C(c_{\mathrm{copy}_A}):\exists!c:\prod_{x:\mathrm{Copy}(A)} C(x).\prod_{x:A} \mathrm{Id}_{C(\mathrm{copy}_A(x))}(c(\mathrm{copy}_A(x)), c_{\mathrm{copy}_A}(x))}$$

Theorem

$\mathrm{copy}_A$ is an equivalence of types between $A$ and $\mathrm{Copy}(A)$.

Proof

Suppose one takes the type family $C$ in the elimination, computation, and uniqueness rules of the copy of $A$ to be the type family $\sum_{x:A} \mathrm{Id}_{\mathrm{Copy}(A)}(\mathrm{copy}_A(x), -)$. Then the elimination rule states that $\sum_{x:A} \mathrm{Id}_{\mathrm{Copy}(A)}(\mathrm{copy}(x), b)$ has an element for all elements $b:\mathrm{Copy}(A)$, the computation rule states that given all elements $a:A$ the type $\sum_{x:A} \mathrm{Id}_{\mathrm{Copy}(A)}(\mathrm{copy}(x), \mathrm{copy}(a))$ is contractible, and the uniqueness rule states that if the type $\sum_{x:A} \mathrm{Id}_{\mathrm{Copy}(A)}(\mathrm{copy}(x), \mathrm{copy}(a))$ is contractible for all elements $a:A$, then the type $\sum_{x:A} \mathrm{Id}_{\mathrm{Copy}(A)}(\mathrm{copy}(x), b)$ is contractible for all elements $b:B$. Thus, $\mathrm{copy}$ is an equivalence of types, since the type $\sum_{x:A} \mathrm{Id}_{\mathrm{Copy}(A)}(\mathrm{copy}(x), b)$ is contractible for all elements $b:\mathrm{Copy}(A)$.

Copies as a negative type

Copies as negative types are also called negative unary product types

The rules for negative copies are given as follows:

Formation rules for copies:

$$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{Copy}(A) \; \mathrm{type}}$$

Introduction rules for copies:

$$\frac{\Gamma \vdash a:A}{\Gamma \vdash \mathrm{copy}(a):\mathrm{Copy}(A)}$$

Elimination rules for copies:

$$\frac{\Gamma \vdash b:\mathrm{Copy}(A)}{\Gamma \vdash \mathrm{original}(b):A}$$

Computation rules for copies:

$$\frac{\Gamma \vdash a:A}{\Gamma \vdash \mathrm{original}(\mathrm{copy}(a)) \equiv a:A} \qquad \frac{\Gamma \vdash a:A}{\Gamma \vdash \mathrm{original}(\mathrm{copy}(a)) \equiv_A a \; \mathrm{true}} \qquad \frac{\Gamma \vdash a:A}{\Gamma \vdash \beta_{\mathrm{Copy}(A)}(a):\mathrm{original}(\mathrm{copy}(a)) =_A a}$$

Uniqueness rules for copies:

$$\frac{\Gamma \vdash b:\mathrm{Copy}(A)}{\Gamma \vdash b \equiv \mathrm{copy}(\mathrm{original}(b)):\mathrm{Copy}(A)} \qquad \frac{\Gamma \vdash b:\mathrm{Copy}(A)}{\Gamma \vdash b \equiv_{\mathrm{Copy}(A)} \mathrm{copy}(\mathrm{original}(b)) \; \mathrm{true}} \qquad \frac{\Gamma \vdash b:\mathrm{Copy}(A)}{\Gamma \vdash \eta_{\mathrm{Copy}(A)}(b):b =_{\mathrm{Copy}(A)} \mathrm{copy}(\mathrm{original}(b))}$$

Theorem

$\mathrm{copy}$ is an equivalence of types between $A$ and $\mathrm{Copy}(A)$.

Proof

Unary products with judgmental or propositional conversion rules turn $\mathrm{copy}$ into a judgmentally strict equivalence and a propositionally strict equivalence respectively. Unary products with only typal conversion rules turn $\mathrm{copy}$ and $\mathrm{original}$ into quasi-inverse functions of each other. One could then define a function $f:\mathrm{QInv}(\mathrm{copy}) \to \mathrm{isEquiv}(\mathrm{copy})$ which takes the quasi-inverse function $(\mathrm{original}, \beta_{\mathrm{Copy}(A)}, \eta_{\mathrm{Copy}(A)})$ to a witness that $\mathrm{copy}$ has contractible fibers and is thus an equivalence of types.

Extensionality principle for copies

The extensionality princple for copies says that for each element $x:A$ and $y:A$ the function application to identities for the copy function $\mathrm{copy}$ is an equivalence of types

$$x:A, y:A \vdash \mathrm{copyext}(x, y):\mathrm{isEquiv}(\mathrm{ap}_{\mathrm{copy}}(x, y))$$

In Mike Shulman‘s model of higher observational type theory, this would be promoted to a judgmental equality:

$$x:A, y:A \vdash (x =_A y) \equiv (\mathrm{copy}(x) =_{\mathrm{Copy}(A)} \mathrm{copy}(y))$$

Relation to equivalences

Given types $A$ and $B$ and $f:A \to B$, $f$ is an equivalence of types if $B$ satisfies the universal property of a positive copy type of $A$ with copy function $f:A \to B$.

Indeed, one could define the isEquiv type family $f:A \to B \vdash \mathrm{isEquiv}(f)$ by very similar rules to the rules for positive copy types:

Formation rules for isEquiv:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B}{\Gamma \vdash \mathrm{isEquiv}(f) \; \mathrm{type}}$$

Introduction rules for isEquiv:

$$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B \quad \Gamma \vdash g:B \to A \\ \Gamma \vdash G:\prod_{y:B} f(g(y)) =_B y \quad \Gamma \vdash H:\prod_{x:A} (g(f(x)) =_A x) \end{array} }{\Gamma \vdash \mathrm{witn}(f, g, G, H):\mathrm{isEquiv}(f)}$$

Elimination rules for isEquiv:

$$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B \quad \Gamma \vdash p:\mathrm{isEquiv}(f) \\ \Gamma, y:B \vdash C(y) \; \mathrm{type} \quad \Gamma \vdash c_f:\prod_{x:A} C(f(x)) \quad \Gamma \vdash b:B \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{isEquiv}(f)}^C(f, p, c_f, b):C(b)}$$

Computation rules for isEquiv:

$$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B \quad \Gamma \vdash p:\mathrm{isEquiv}(f) \\ \Gamma, y:B \vdash C(y) \; \mathrm{type} \quad \Gamma \vdash c_f:\prod_{x:A} C(f(x)) \quad \Gamma \vdash a:A \end{array} }{\Gamma \vdash \beta_{\mathrm{isEquiv}(f)}(f, p, c_f, a):\mathrm{ind}_{\mathrm{isEquiv}(f)}^C(f, p, c_f, f(a)) =_{C(f(a))} c_f(a)}$$

Uniqueness rules for isEquiv:

$$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B \quad \Gamma \vdash p:\mathrm{isEquiv}(f) \\ \Gamma, y:B \vdash C(y) \; \mathrm{type} \quad \Gamma \vdash c:\prod_{y:B} C(y) \quad \Gamma \vdash b:B \end{array} }{\Gamma \vdash \eta_{\mathrm{isEquiv}(f)}(f, p, c, b):c(b) =_{C(b)} \mathrm{ind}_{\mathrm{isEquiv}(f)}^C(f, p, c, b)}$$

Similarly, one could define the type of equivalences between $A$ and $B$ by very similar rules to the rules for positive copy types and isEquiv types:

Formation rules for equivalence types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \simeq B \; \mathrm{type}}$$

Introduction rules for equivalence types:

$$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B \quad \Gamma \vdash g:B \to A \\ \Gamma \vdash G:\prod_{y:B} f(g(y)) =_B y \quad \Gamma \vdash H:\prod_{x:A} (g(f(x)) =_A x) \end{array} }{\Gamma \vdash \mathrm{equiv}(f, g, G, H):A \simeq B}$$

Elimination rules for equivalence types:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, R:A \simeq B}{\Gamma, x:A \vdash f_R(x):B}$$

$$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, R:A \simeq B \\ \Gamma, y:B \vdash C(y) \; \mathrm{type} \quad \Gamma \vdash c_R:\prod_{x:A} C(f_R(x)) \quad \Gamma \vdash b:B \end{array} }{\Gamma \vdash \mathrm{ind}_{A \simeq B}^C(R, c_R, b):C(b)}$$

Computation rules for equivalence types:

$$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash R:A \simeq B \\ \Gamma, y:B \vdash C(y) \; \mathrm{type} \quad \Gamma \vdash c_R:\prod_{x:A} C(f_R(x)) \quad \Gamma \vdash a:A \end{array} }{\Gamma \vdash \beta_{A \simeq B}(R, c_R, a):\mathrm{ind}_{A \simeq B}^C(R, c_R, f_R(a)) =_{C(f_R(a))} c_R(a)}$$

Uniqueness rules for equivalence types:

$$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash R:A \simeq B \\ \Gamma, y:B \vdash C(y) \; \mathrm{type} \quad \Gamma \vdash c:\prod_{y:B} C(y) \quad \Gamma \vdash b:B \end{array} }{\Gamma \vdash \eta_{A \simeq B}(R, c, b):c(b) =_{C(b)} \mathrm{ind}_{A \simeq B}^C(R, c, b)}$$

 See also

• equivalence in type theory
• unit type
• dependent sum type
• sum type
• definition

 References

The above notion of “copy of a type” is considered in §2.12.8 of:

• Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, Daniel R. Grayson, Symmetry (2021) $[$pdf$]$