a related exploit in Coq proof checker: a hostile plugin hidden inside big archive with proofs can subvert "coqchk" and prove anything sympa.inria.fr/sympa/arc/coq-club/2011-05/msg00016.html . developers acknowledge the exploit but do not seem worried.

Nate: the question is whether there is a similar characterisation for supercompacts, as well as a request for references: probably someone noticed that a tree is a sheaf before, and maybe used some category theory...

Dear Joel, you are right, the definition $\kappa$-tree is correct only for $\kappa$ inaccessible, as Nate writes. (Although I must admit that I only meant that a $\kappa$-tree is a sheaf, perhaps with other properties). For an arbitrary cardinal $\kappa$, one has to require size-of-level condition explicitly.

Joel and Nate: I added the assumption of inaccessibility into my definition of weakly compact cardinal. I am not entirely sure it is really necessary but it is best to avoid this point here...

Nate: thank you for your corrections! I corrected the definition of a sheaf corresponding to a tree; really the union is the wrong thing there, one should actually do the inverse limit...I take care of it now, and hope it is correct now.

But here it is important that I am talking about a sheaf of functions. I can also talk about an arbitrary sheaf of sets, and then I do need to require $Lev_\alpha<\kappa$. That is, $\kappa$ has the tree property iff for every sheaf $T:\kappa^{op}\longrightarrow Sets$ of sets on $\kappa$, if for every $\alpha<\kappa$ it holds $0<|T(\alpha)|<\kappa$, then also $T(\kappa)$ is non-empty.

namely, if $Lev_\alpha$ is of size $\kappa$, from level $\alpha$ onwards start "chopping off" a single branch at each level (and similarly for $|Lev_\alpha|>\kappa$. Does this make more sense?

Joel: thank you, right, not every sheaf of functions on $\kappa$ is necessarily a $\kappa$-tree. (I do not claim this explicitly but I do claim this implicitly..sorry.). In set theory terminology, my requirement is that $\alpha$-th level should have size at most $2^\alpha$. Now, my claim about inaccessibility is for such "trees": that is, if every such "tree" of height $\kappa$ necessarily has a $\kappa$-branch, then $\kappa$ is inaccessible. Essentially it is the argument saying that it is boring to consider trees without the condition that $\alpha$'s-level is of size $<\kappa$:

Joel: yes, I misstated the condition on accessibility; see the corrected proof in the post. I also clarified the passage from trees to sheaves, in response to your second question: informally, every limit stage in a tree splits into two steps: first to you pass to all the limits, and then pass to the subset appearing in the tree.