(-1)-categories and (-2)-categories

[baez@newmath.UCR.EDU]

Steve Vickers asked by email whether in constructive mathematics a 
(-1)-category should be allowed to be an arbitrary "subsingleton", 
i.e. a set with at most one element.  I think that yes, these should
be allowed - but maybe other things too!

Indeed, a space has homotopy dimension -1 iff 

1) given 2 points in the space there exists a path joining them, 

and 

2) given 2 paths joining them, there exists a path of paths joining *them*

and

3) given 2 paths of paths joining *them*, there exists a path of paths 
  of paths joining THEM, 

and so on ad infinitum.   As a nonconstructivist, I would say that
either the space is empty in which case clause 1) is vacuous, or
it's nonempty in which case we go on and read the resulting infinite
list of clauses.  But a constructive mathematician would have to proceed
differently here, not being allowed to use the excluded middle.  

Do the remaining clauses provide any extra challenges for the constructivist?

Then there's the bit where, having gotten a space that's either empty
or contains one arc-component with vanishing homotopy groups, I conclude
that if it's *nice* (e.g. a CW complex) it's homotopy equivalent to a
space that's either empty or one point.  I don't know how this reasoning
(which uses the Whitehead theorem) gets affected by constructivism.  

Steve's idea sounds interesting, for this reason.  If you plow
through the detailed exchange between James Dolan and Toby Bartels, 
you'll see that (-1)-categories secretly represent TRUTH VALUES.  
In any approach to math where "truth values" are more interesting
than merely 0 or 1, (-1)-categories will be correspondingly more 
interesting than merely sets with 0 or 1 elements.  

I guess this is familiar from topos theory.  But I don't know if 
there's an extra twist due to all the "higher-dimensional" stuff 
going on in my reasoning above.  Are truth values for an
omega-categorical constructivist still more interesting than for
an ordinary constructivist?  The ordinary constructivist may not
know whether two things are equal.  The omega-categorical constructivist
may not know whether all morphisms between two things are related by
a 2-morphism, or whether all such 2-morphisms are related a 3-morphism,
and so on....