Reputation
15,738
Top tag
Next privilege 20,000 Rep.
Access 'trusted user' tools
Badges
39 83
Newest
 Nice Answer
Impact
~145k people reached

Apr
27
comment What is a canonical term of $\text{Id}_A(x,y)$ if $x$ is not jugdmentally identical to $y$?
Type theory is never as strong as my meta-logic. That would make my meta-logic too weak to study type theory.
Apr
27
comment What is a canonical term of $\text{Id}_A(x,y)$ if $x$ is not jugdmentally identical to $y$?
Also, the OP is usig the word "judgementally" so it may be better to use the same word instead of "definitionally" (which is not as good as "judgmentally" in my opinion).
Apr
27
comment What is a canonical term of $\text{Id}_A(x,y)$ if $x$ is not jugdmentally identical to $y$?
Let me put on my provably crusade hat: "provably the case" as opposed to "unprovably the case"?
Apr
27
awarded  Nice Answer
Apr
19
comment Real computers have only a finite number of states, so what is the relevance of Turing machines to real computers?
Because sometimes $\infty$ is a better approximation to $10000000000000000000000000000000$ than $10000000000000000000000000000000$.
Apr
16
revised Composition in explicit substitutions
added 50 characters in body
Apr
16
comment Composition in explicit substitutions
The reference is in my answer.
Apr
16
answered Composition in explicit substitutions
Apr
12
comment Is there a good notion of non-termination and halting proofs in type theory?
Are you looking for the delay monad?
Apr
10
comment Implementing “Internal” Languages
For the Type theory + Prop, you just stare at every rule and see that if you interpret Prop as the subobject classifier, it's all valid in a topos.
Apr
10
comment Implementing “Internal” Languages
For step-indexing in particular it would make sense to extend the topos logic with a modal operator. This will in general be a feature of any situation in which you care about a subtopos, or you have a (co)monad that you want to study, etc.
Apr
9
answered Implementing “Internal” Languages
Apr
8
comment Minimal specification of Martin-Löf type theory
You could get $0$ that way, but note that $1 =_U 2$ refers to a universe $U$. And the $0$ so defined lives, awkwardly, in the next universe.
Apr
2
comment Can we say that Church encoding is a form of Gödelization?
Well, in that case this question should be asked at cs.stackexchange.com. There's nothing research-level about it.
Apr
2
comment Can we say that Church encoding is a form of Gödelization?
Is there a scientific question here? It seems awfully vague to ask this question. For instance, why would "Yes we can" be an insufficient answer?
Mar
22
comment Zero of a multivariate cubic equation
But if the coefficients of the polynomial are arbitrary reals and so are the endpoints of the intervals, how do you apply Tarski's theory? Are you assuming that the coffecients and the endpoints are algebraic numbers? I think it would just help if you were a bit more precise about the exact assumptions you're placing on the problem.
Mar
22
comment Zero of a multivariate cubic equation
It's co-semidecidable, unless you are assuming that testing reals for zero is decidable or some such. What model are you working in? BSS?
Mar
7
awarded  Enlightened
Mar
7
awarded  Nice Answer
Feb
7
comment `f_equal` isn't doing anything
The type valid m_value = true and valid n_value = true are propositionally equal, which means that the type (valid m_value = true) = (valid n_value = true) is inhabited by some p. But they are not judgmentally equal, an so from x : valid m_value = true we cannot conclude x : valid n_value = true. Instead we get to conclude that the transport of x along p has type valid n_value = true. Have you looked at homotopy type theory? There these things are explained carefully (and also why things are done this way).