The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Saturday, September 24, 2011 11:12:27 AM Vladimir Voevodsky wrote:
> PS Note that if one drops Prop then one also drops inductive definitions
> with values in Prop and then, for example, the definition of subgroup
> generated by a subset which Daniel writes about won't work. To replace it
> with another definition - the intersection of all the subgroups which
> contain the given subset, one needs a "resizing rule" since otherwise the
> subgroup generated by a subset will be typed to the larger universe than
> the subset itself.

I'm not sure what you mean by this.  If you replace Ensemble G in my 
definition 
with (G->Type), then essentially what you get is the set of abstract terms in 
the language of groups, with each atom coming from S (although indexed by the 
evaluation in G of the abstract term).  That construction shouldn't require 
passing to a larger universe than the universe G is in.
-- 
Daniel