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:
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
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: Jun 04 2023 at 19:30 UTC