With -indices-matter eq has the same type but cannot generate rec and rect. How exactly does -indices-matter get in the way of the eliminator?

I only remember this comment from @Gaëtan Gilbert but I don't really understand what is going on. https://github.com/coq/coq/pull/15260#discussion_r759329432

eq with indices matter looks like: `eq : forall [A : Type], A -> A -> Prop`

eq without indices matter looks like `eq : forall [A : Type], A -> A -> Prop`

Where is the magic happening?

the difference is not the type nor the constructor, it's what is allowed in the eliminator

inductives can be defined in Prop either if they are small enough (then they get _rect) or by squashing

indices-matter forces squashing for eq

The "small enough" part being the singleton business?

Are the small ones the same ones picked out by SProp? Acc etc.?

rules for non squashed Prop:

- all constructor arguments in Prop or SProp
- at most 1 constructor
- if indices matter, all indices in Prop or SProp

Acc is still Prop with indices matter (it has no indices thanks to non recursively uniform parameters)

if indices matter, all indices in Prop or SProp

Is it known that this causes problems when dropped?

it's the definition of indices matter

I was always under the impression that -indices-matter was really talking about universe levels not comparing between prop and other sorts.

I don't know what that's supposed to mean so I can't tell if it's correct

The reason we don't allow an indexed inductive to live in a universe lower than its indices is because we can get Russel style problems no?

My point is that prop is not an ordinary universe level

universe rules for inductives in general, let U be the sort of the inductive

- all constructor arguments <= U (where the order is SProp <= Prop <= Set <= Type...)
- if indices matter, all indices <= U (same order)
- if U=SProp, 0 constructors OR (definitional UIP on and 1 constructor and no constructor arguments)
- if U=Prop, 0 or 1 constructors

OR U impredicative and the inductive is squashed

strictly speaking indices-matter is designed for HoTT (where `@paths A x y`

must be in same or higher universe as A)

since HoTT isn't supposed to use Prop indices-matter could do anything on Prop and it doesn't matter since nobody knows what it means

Exactly, so the second condition might be a bit too strict. I wonder if it is consistent to relax it so that we don't compare between SProp,Prop and Set,Type.

too strict for what? it's consistent without axioms since no-indices-matter is consistent

so that we don't compare between SProp,Prop and Set,Type.

WDYM?

Not enabling -indices-matter is not exactly allowing any size for the indices however. For example, the following doesn't work (with uni poly):

```
Inductive Box (A : Type) : Set :=
| a : A -> Box A.
```

sorry more correctly:

```
Inductive Box : forall (A : Type), Set :=
| a {A : Type} : A -> Box A.
```

I guess here the constructor size check is what is stopping this.

because of the constructor argument

univ poly does nothing on this

Gaëtan Gilbert said:

too strict for what? it's consistent without axioms since no-indices-matter is consistent

I'm looking at it from the perspective of enabling -indices-matter everywhere. But I always get confused since all the issues are Prop related which -indices-matter wasn't even designed for.

there is a transformation from inductives with indices to inductives with non recursively uniform parameters + a special equality type

if the special equality type is in the same universe as its type argument you get indices-matter

if it's in Prop you get no-indices-matter with uip off

if it's in sprop you get no-indices-matter with uip on

so you can't have indices-matter with unsquashed eq in prop

(I should have remembered that instead of saying stuff about how hott doesn't care what we do with prop)

Is that transformation detailed anywhere?

it's pretty trivial, if you have

```
Inductive Ind params : indices -> U := C : forall args, Ind params (f args)
```

you transform to

```
Inductive Ind params indices : U := C : forall args, f args = indices -> Ind params indices.
```

(where params, indices, args and f are telescopes for full generality)

Right, I've seen this before actually

But I saw it in a different dress. Its the translation between indexed W-types and W-types?

In fact, I even ported Jasper's formalization of it to the HoTT library: https://github.com/HoTT/HoTT/blob/master/theories/Types/IWType.v

There is no UIP involved in this translation however

mine doesn't use uip either

it's probably basically the same thing

However these IW-types inherit their "indices mattering" from the definition of the IW-type

Which is just

```
Inductive IW
(I : Type) (** The indexing type *)
(A : Type) (** The type of labels / constructors / data *)
(B : A -> Type) (** The the type of arities / arguments / children *)
(i : A -> I) (** The index map (for labels) *)
(j : forall x, B x -> I) (** The index map for arguments *)
: I -> Type :=
| iw_sup (x : A)
: (forall (y : B x), IW I A B i j (j x y)) -> IW I A B i j (i x).
```

I played around with similar stuff a while back but never submitted anywhere

https://github.com/SkySkimmer/HoTTClasses/blob/f9affefaa088d02ca7e6e901580ae6f9ff13ca40/theories/inductives/inductives.v#L79-L121

So all of this doesn't really have to do with inductive types I suppose. It really is a property of whatever equality you have.

InductiveS is a description of an inductive (with only recursive parameters)

indT implements it with indices

indT' with nonrec params

Ali Caglayan said:

So all of this doesn't really have to do with inductive types I suppose. It really is a property of whatever equality you have.

I guess it depends on if you see equality as more primitive or as just a specific inductive

Your formalization is very cool.

Thank you very much for the interesting discussion.

I seem to recall an example of -indices-matter breaking things in the test-suite for non-prop related things.

```
Variables (A B : Type) (x : A) (f : A -> B) (b : bool) (vT vF : A).
Variant if_spec (not_b : Prop) : bool -> A -> Set :=
| IfSpecTrue of b : if_spec not_b true vT
| IfSpecFalse of not_b : if_spec not_b false vF.
```

From ssrbool.v

Not in the test-suite actually

So A can be in a big universe but if_spec lands in Set

what about it?

Last updated: Dec 05 2023 at 05:01 UTC