Redirected from "weak negative copy".
Contents
Idea
In dependent type theory, given a type , one could define a type called a copy of , which is equivalent to .
Definitions
There are two ways to define the copy of a type , 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 is the inductive type generated by a function from to :
Formation rules for copies:
Introduction rules for copies:
Elimination rules for copies:
Computation rules for copies:
Uniqueness rules for copies:
The elimination, computation, and uniqueness rules for the copy of state that the copy of and satisfy the dependent universal property of the copy of and . 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 could be simplified to the following rule:
Proof
Suppose one takes the type family in the elimination, computation, and uniqueness rules of the copy of to be the type family . Then the elimination rule states that has an element for all elements , the computation rule states that given all elements the type is contractible, and the uniqueness rule states that if the type is contractible for all elements , then the type is contractible for all elements . Thus, is an equivalence of types, since the type is contractible for all elements .
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:
Introduction rules for copies:
Elimination rules for copies:
Computation rules for copies:
Uniqueness rules for copies:
Proof
Unary products with judgmental conversion rules turn into a definitional isomorphism. Unary products with only typal conversion rules turn and into quasi-inverse functions of each other. One could then define a function which takes the quasi-inverse function to a witness that has contractible fibers and is thus an equivalence of types.
Extensionality principle for copies
The extensionality princple for copies says that for each element and the function application to identities for the copy function is an equivalence of types
In Mike Shulman‘s model of higher observational type theory, this would be promoted to a judgmental equality:
Relation to equivalences
Given types and and , is an equivalence of types if satisfies the universal property of a positive copy type of with copy function .
Indeed, one could define the isEquiv type family by very similar rules to the rules for positive copy types:
Formation rules for isEquiv:
Introduction rules for isEquiv:
Elimination rules for isEquiv:
Computation rules for isEquiv:
Uniqueness rules for isEquiv:
Similarly, one could define the type of equivalences between and by very similar rules to the rules for positive copy types and isEquiv types:
Formation rules for equivalence types:
Introduction rules for equivalence types:
Elimination rules for equivalence types:
Computation rules for equivalence types:
Uniqueness rules for equivalence types:
See also
References
The above notion of “copy of a type” is considered in §2.12.8 of: