Return to Question

What's the extension of definitional identity in HoTT (homotopy type theory)?

The Martin-Löf intensional dependent type theory with identity types is called (definitionally) extensional if the definitional (intensional) equality coincides with the propositional equality, i.e, $$ \frac{p:Id_A(x,y)}{x\equiv y} $$ For the name "extensional" makes sense, the definitional equality must be determined by the extension of the terms.

So what's the extension of $x \equiv y$? By the definition, it just seems that the extension are the proofs (hence $Id_A (x, y)$ is the extension of $x \equiv_A y$) and, in this case, it would not match with the extension of the relational symbol "equality" used in the internal language of categories where a relational symbol (or predicate) $\varphi$ would be a subobject of a type $A$ $$[\varphi] \hookrightarrow A$$ composed by the collection (not set, there's no set theory here) of terms such that the predicate is true $\{x : A; \varphi(x) \ \text{true} \}$ .

So, more generally, what's the extension of a predicate in Martin-Löf type theory?

What's the extension of judgmental identity in HoTT (homotopy type theory)?

The Martin-Löf intensional dependent type theory with identity types is called (definitionally) extensional if the judgmental (intensional) equality coincides with the propositional equality, i.e, $$ \frac{p:Id_A(x,y)}{x\equiv y} $$ For the name "extensional" makes sense, the judgmental equality must be determined by the extension of the terms.

So what's the extension of $x \equiv y$? By the definition, it just seems that the extension are the proofs (hence $Id_A (x, y)$ is the extension of $x \equiv_A y$) and, in this case, it would not match with the extension of the relational symbol "equality" used in the internal language of categories where a relational symbol (or predicate) $\varphi$ would be a subobject of a type $A$ $$[\varphi] \hookrightarrow A$$ composed by the collection (not set, there's no set theory here) of terms such that the predicate is true $\{x : A; \varphi(x) \ \text{true} \}$ .

So, more generally, what's the extension of a predicate in Martin-Löf type theory?

What's the extension of definitional identity in HoTT (homotopy type theory)?

The Martin-Löf intensional dependent type theory with identity types is called (definitionally) extensional if the definitional (intensional) equality coincides with the propositional equality, i.e, $$ \frac{p:Id_A(x,y)}{x\equiv y} $$ For the name "extensional" makes sense, the definitional equality must be determined by the extension of the terms. So what's the extension of $x \equiv y$? By the definition, it just seems that the extension are the proofs and, in this case, it would not match with the extension of the relational symbol "equality" used in the internal language of categories where a relational symbol would be a subobject of a type $A$ composed by the terms such that the predicate is true.

So, more generally, what's the extension of a predicate in type theory?

What's the extension of definitional identity in HoTT (homotopy type theory)?

The Martin-Löf intensional dependent type theory with identity types is called (definitionally) extensional if the definitional (intensional) equality coincides with the propositional equality, i.e, $$ \frac{p:Id_A(x,y)}{x\equiv y} $$ For the name "extensional" makes sense, the definitional equality must be determined by the extension of the terms. 

So what's the extension of $x \equiv y$? By the definition, it just seems that the extension are the proofs (hence $Id_A (x, y)$ is the extension of $x \equiv_A y$) and, in this case, it would not match with the extension of the relational symbol "equality" used in the internal language of categories where a relational symbol (or predicate) $\varphi$ would be a subobject of a type $A$ $$[\varphi] \hookrightarrow A$$ composed by the collection (not set, there's no set theory here) of terms such that the predicate is true $\{x : A; \varphi(x) \ \text{true} \}$ .

So, more generally, what's the extension of a predicate in Martin-Löf type theory?