[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
A set theorist, an ordinary mathematician and an intensional type
theorist are discussing the booleans.
The set theorist says:
"I define bool to be the set {{},{{}}}, calling {} false and
{{}} true."
The mathematician replies:
"Why be so specific? bool can be any set with a specified
isomorphism to {{},{{}}}. That's why I reject your theorem that the
empty set is an element of the union-set of bool."
The intensional type theorist says to the mathematician:
"Why be so specific? bool can be any omega-groupoid with a
specified equivalence to {{},{{}}}. That's why I reject your theorems
that
x : bool, y : id(x,true), z: if x then bool else nat |-
z : bool
x : bool, y : id(x,true) |- y : id(if x then true else
false, true) (a consequence of judgemental eta). "
Having overheard this conversation, I ask the type theorist:
"But why do you reject the judgements
x : bool, y : if x then 1 else 0 |- if x then true else
7 : bool
x : 0 |- 7 : bool (a consequence of judgemental eta)
? After all, these are semantically valid no matter which omega-
groupoid and specified equivalence to {{},{{}}} you use to interpret
bool."
The type theorist replies:
"Because either of these judgements would make typing
undecidable."
I ask:
"Then you agree with my position that decidable typing is
woefully incomplete typing?"
The type theorist replies:
"Yes, but (like all intensional type theorists) I am ambiguous
about whether I am doing type theory or logic. With my logician hat
on I care only about completeness of inhabitation, not about
completeness of typing."
A final question for the type theorist and anyone still reading: is it
the case that any closed type of ITT + function extensionality that's
inhabited in ETT is also inhabited in ITT + function extensionality?
Or at least in homotopy type theory?
Paul
--
Paul Blain Levy
School of Computer Science, University of Birmingham
+44 121 414 4792
http://www.cs.bham.ac.uk/~pbl
