Hi, Thomas Streicher writes: Date: Thu, 5 Jun 2003 13:08:14 +0200 (CEST) Subject: categories: Re: topos logic arising nicely But I would be surprised if HOL has subtype formation as from a logical point of view subtypes are neither necessary nor convenient. Adding subtypes is only necessary for getting a topos out of a model of HOL. I don't know, if I miss the point here. However, PVS has a HOL system with predicate subtypes. And it is _very very_ convenient (because of the predicate subtypes). I don't know if it is a necessity, but the absence of subtypes in Isabelle/HOL leads to a representation of partial functions, that allows you to prove unexpected results. Despite what the Isabelle tutorial says at page 187, you _can_ prove hd [] = last [] (saying that the head of the empy list equals its last element) Bye, Hendrik