Rowan Evans via agora-business [2025-04-09 11:48]:
> It seems to me that:
>
> 1. Switches are created on a "type" of entity by bullet 1 in R2162.
>
> 2. R2606, which creates Class switches, attempts to limit it to "Proposals
> created since the enactment of this rule".
>
> 3. This would have had the effect of creating a switch on a set of entities
> rather than a type of entity
…what? That *is* a type of entity, in any conception of the term,
as far as I understand it. Even if you mean it formally, a reasonable
type theory would account for that:
Σ (p : Proposal) (creation_time p > rule_creation_time)
Sets and types are constructs from different theories used to formalized
mathematics. To be picky about their meanings, we need some theory
that could be reasonably said to include both. And, to my mind, that
is probably some form of structural set theory, such as Lawvere's ETCS,
in which sets *are* types [1], and subsets are subobjects of those types.
[1]: Well, objects in a category, which correspond to types in a
reasonable internal language for that category.
I think this should answer the first three CFJs you called. I leave the
fourth, a matter of law, to the judges.
> I CFJ each of the following four statements:
> 1. "Proposals created since the enactment of this rule" is not a valid
> entity type for the purpose of creating a switch by R2162.
> 2. If a lower-powered rule than R2162 (for example but not limited to
> R2606) attempts to create a switch on entities of a type, but attempts to
> attach some extra condition that will always be met (and is impossible not
> to meet) for entities of that type, then the rule has validly constructed
> that switch under R2162.
> 3. If a lower-powered rule than R2162 (for example but not limited to
> R2606) attempts to create a switch on entities of a type, but attempts to
> attach some extra condition, the rule is interpreted as though the extra
> condition was not included.
> 4. Some proposals have a Class switch
--
juan
Coincidentally, a type theory researcher
