nLab copy

Redirected from "unary sum".

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

 Idea

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

Definitions

There are two ways to define the copy Copy(A)\mathrm{Copy}(A) of a type AA, 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 AA is the inductive type generated by a function from AA to Copy(A)\mathrm{Copy}(A):

Formation rules for copies:

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

Introduction rules for copies:

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

Elimination rules for copies:

ΓAtypeΓ,x:Copy(A)C(x)typeΓc copy A: x:AC(copy A(x))Γy:Copy(A)Γind Copy(A) C(c copy A,y):C(y)\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:

ΓAtypeΓ,x:Copy(A)C(x)typeΓc copy A: x:AC(copy A(x))Γx:AΓβ Copy(A) copy A(c copy A,x):Id C(copy A(x))(ind Copy(A) C(c copy A,copy A(x)),c(x))\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:

ΓAtypeΓ,x:Copy(A)C(x)typeΓc: x:Copy(A)C(x)Γy:Copy(A)Γη Copy(A)(c,y):Id C(y)(ind Copy(A) C(c copy A,y),c(y))\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 AA state that the copy of AA and BB satisfy the dependent universal property of the copy of AA and BB. 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 AA could be simplified to the following rule:

ΓAtypeΓ,x:Copy(A)C(x)typeΓc copy A: x:AC(copy A(x))Γup Copy(A) C(c copy A):!c: x:Copy(A)C(x). x:AId C(copy A(x))(c(copy A(x)),c copy A(x))\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

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

Proof

Suppose one takes the type family CC in the elimination, computation, and uniqueness rules of the copy of AA to be the type family x:AId Copy(A)(copy A(x),)\sum_{x:A} \mathrm{Id}_{\mathrm{Copy}(A)}(\mathrm{copy}_A(x), -). Then the elimination rule states that x:AId Copy(A)(copy(x),b)\sum_{x:A} \mathrm{Id}_{\mathrm{Copy}(A)}(\mathrm{copy}(x), b) has an element for all elements b:Copy(A)b:\mathrm{Copy}(A), the computation rule states that given all elements a:Aa:A the type x:AId Copy(A)(copy(x),copy(a))\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 x:AId Copy(A)(copy(x),copy(a))\sum_{x:A} \mathrm{Id}_{\mathrm{Copy}(A)}(\mathrm{copy}(x), \mathrm{copy}(a)) is contractible for all elements a:Aa:A, then the type x:AId Copy(A)(copy(x),b)\sum_{x:A} \mathrm{Id}_{\mathrm{Copy}(A)}(\mathrm{copy}(x), b) is contractible for all elements b:Bb:B. Thus, copy\mathrm{copy} is an equivalence of types, since the type x:AId Copy(A)(copy(x),b)\sum_{x:A} \mathrm{Id}_{\mathrm{Copy}(A)}(\mathrm{copy}(x), b) is contractible for all elements b:Copy(A)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:

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

Introduction rules for copies:

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

Elimination rules for copies:

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

Computation rules for copies:

Γa:AΓoriginal(copy(a))a:AΓa:AΓoriginal(copy(a)) AatrueΓa:AΓβ Copy(A)(a):original(copy(a))= Aa\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:

Γb:Copy(A)Γbcopy(original(b)):Copy(A)Γb:Copy(A)Γb Copy(A)copy(original(b))trueΓb:Copy(A)Γη Copy(A)(b):b= Copy(A)copy(original(b))\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

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

Proof

Unary products with judgmental conversion rules turn copy\mathrm{copy} into a definitional isomorphism. Unary products with only typal conversion rules turn copy\mathrm{copy} and original\mathrm{original} into quasi-inverse functions of each other. One could then define a function f:QInv(copy)isEquiv(copy)f:\mathrm{QInv}(\mathrm{copy}) \to \mathrm{isEquiv}(\mathrm{copy}) which takes the quasi-inverse function (original,β Copy(A),η Copy(A))(\mathrm{original}, \beta_{\mathrm{Copy}(A)}, \eta_{\mathrm{Copy}(A)}) to a witness that copy\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:Ax:A and y:Ay:A the function application to identities for the copy function copy\mathrm{copy} is an equivalence of types

x:A,y:Acopyext(x,y):isEquiv(ap copy(x,y))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(x= Ay)(copy(x)= Copy(A)copy(y))x:A, y:A \vdash (x =_A y) \equiv (\mathrm{copy}(x) =_{\mathrm{Copy}(A)} \mathrm{copy}(y))

Relation to equivalences

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

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

Formation rules for isEquiv:

ΓAtypeΓBtypeΓf:ABΓisEquiv(f)type\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:

ΓAtypeΓBtypeΓf:ABΓg:BA ΓG: y:Bf(g(y))= ByΓH: x:A(g(f(x))= Ax)Γwitn(f,g,G,H):isEquiv(f)\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:

ΓAtypeΓBtypeΓf:ABΓp:isEquiv(f) Γ,y:BC(y)typeΓc f: x:AC(f(x))Γb:BΓind isEquiv(f) C(f,p,c f,b):C(b)\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:

ΓAtypeΓBtypeΓf:ABΓp:isEquiv(f) Γ,y:BC(y)typeΓc f: x:AC(f(x))Γa:AΓβ isEquiv(f)(f,p,c f,a):ind isEquiv(f) C(f,p,c f,f(a))= C(f(a))c f(a)\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:

ΓAtypeΓBtypeΓf:ABΓp:isEquiv(f) Γ,y:BC(y)typeΓc: y:BC(y)Γb:BΓη isEquiv(f)(f,p,c,b):c(b)= C(b)ind isEquiv(f) C(f,p,c,b)\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 AA and BB by very similar rules to the rules for positive copy types and isEquiv types:

Formation rules for equivalence types:

ΓAtypeΓBtypeΓABtype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \simeq B \; \mathrm{type}}

Introduction rules for equivalence types:

ΓAtypeΓBtypeΓf:ABΓg:BA ΓG: y:Bf(g(y))= ByΓH: x:A(g(f(x))= Ax)Γequiv(f,g,G,H):AB\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:

ΓAtypeΓBtypeΓ,R:ABΓ,x:Af R(x):B\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}
ΓAtypeΓBtypeΓ,R:AB Γ,y:BC(y)typeΓc R: x:AC(f R(x))Γb:BΓind AB C(R,c R,b):C(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:

ΓAtypeΓBtypeΓR:AB Γ,y:BC(y)typeΓc R: x:AC(f R(x))Γa:AΓβ AB(R,c R,a):ind AB C(R,c R,f R(a))= C(f R(a))c R(a)\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:

ΓAtypeΓBtypeΓR:AB Γ,y:BC(y)typeΓc: y:BC(y)Γb:BΓη AB(R,c,b):c(b)= C(b)ind AB C(R,c,b)\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

 References

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

Last revised on May 17, 2024 at 12:35:25. See the history of this page for a list of all contributions to it.