# [TYPES] boolean conversation

Paul Levy P.B.Levy at cs.bham.ac.uk
Mon Aug 25 12:17:38 EDT 2014

```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."

"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
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

```