[TYPES] boolean conversation

[ 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