I wonder if the interesting uses of impredicative set would be satisfied by having just

```
Inductive Forall (A:Type) (B:A -> Set) : Set :=
mkForall : (forall x, B x) -> Forall A B.
Definition apply {A B} (f:Forall A B) (x:A) : B x :=
match f with mkForall f => f x end.
```

where `Forall`

does NOT have large elimination (but apply s well defined because `B x`

is small)

ie impredicative set enables 2 behaviours: the product typing rule when codomain : Set, and defining inductives in Set without large elimination whose constructors may have large arguments

perhaps just the second behaviour is enough, and it has a much more local effect so less impact on implementation

You lose η-laws on functions with that, but I don't know if people rely on that.

That said I don't consider that impredicative set is a huge burden on the implementation.

Most probably, I suspect it just doesn't work in practice.

isn't the gain here that one would be able to combine code with predicative set and impredicative under one roof? (no separate option)

We only have a handful of tests and AFAIK no CI dev relying on it.

@Karl Palmskog maybe I'm misunderstanding what you mean, but that's precisely what you don't want. Otherwise you lose code reuse.

otherwise it's very easy to add a dedicated sort `ISet`

that stands for impredicative set (and deactivate it by default)

OK, so this would just change semantics with `-impredicative-set`

I guess

re @Gaëtan Gilbert actually you can recover η-laws by using a primitive record instead

(the fact we can even do this looks like a glaring inconsistency to me but YMMV)

Pierre-Marie Pédrot said:

otherwise it's very easy to add a dedicated sort

`ISet`

that stands for impredicative set (and deactivate it by default)

I don't believe that this is true

Pierre-Marie Pédrot said:

re Gaëtan Gilbert actually you can recover η-laws by using a primitive record instead

no you can't

no large elimination without the type of product rule

right right

we could implement it with type-in-type though, and provide -impredicative-set as a library

(i.e. it would only activate fancy typing rules for inductive types)

Last updated: Sep 15 2024 at 12:01 UTC