Re: [mizar] structures

[Andrzej Trybulec <trybulec@cs.shinshu-u.ac.jp>]

Not at all. You have to be certain that the fixed set is theta. If we chose the
empty set for the fixed set, as Grzegorz proposed, then the non empty set must be
something different, mustn't it?

Andrzej

Josef Urban wrote:

> On Tue, 8 Oct 2002, Andrzej Trybulec wrote:
>
> > Grzegorz (Bancerek) propose that we should adopt an additional rule, that
> >     'the fixed set' should be the empty set
> > I agree, but it looks as a requirement. Moreover, he proposed that if the
> > empty set has the type theta, then 'the fixed theta' equals to the empty set.
> > It may be generalized: if the mother type of theta is theta_1 and
> >       the theta is theta_1
> > then
> >      the theta = the theta_1
>
> If I understand this correctly, recursion (ending at the top of the type
> hierarchy, i.e. "set") gives for all types "the theta" = "the fixed set".
>
> Josef