conditionally constant functions

I'm proposing the name "conditionally constant" for a function that factors through the propositional truncation of its domain, to be distinguished from "weakly constant functions" which map all pairs of inputs to equal outputs and "constant functions" which factor through `Unit`.  This commit formalizes some basic facts about when weakly constant functions are conditionally constant, from the paper of Kraus, Escardo, Coquand, and Altenkirch.
I think the original implication of `Is` was that it denotes an hprop; I think that's how Voevodsky used it in his library.  I've already violated that convention with `IsIdempotent` and friends, though; in that case it was because I needed to distinguish the predicate `IsIdempotent` on functions from the type `Idempotent X` of idempotents on a type `X`.  (Note that `IsEquiv` and `IsTrunc` also need to be distinguished from the type `Equiv` of equivalences and the operation `Trunc` of truncation, respectively.)  But here that didn't seem to be a problem, so I reverted back to the original convention without really thinking about it.  Do you (or anyone else) have opinions?  Should we demand a consistent meaning of `Is`, and if so what should it be?