Ali Caglayan (Apr 01 2022 at 17:46): Ali Caglayan (Apr 01 2022 at 17:46):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?
Ali Caglayan (Apr 01 2022 at 17:48):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
Ali Caglayan (Apr 01 2022 at 17:49):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
Ali Caglayan (Apr 01 2022 at 17:50):Where is the magic happening?
Pierre-Marie Pédrot (Apr 01 2022 at 17:52):the difference is not the type nor the constructor, it's what is allowed in the eliminator
Gaëtan Gilbert (Apr 01 2022 at 17:52):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
Ali Caglayan (Apr 01 2022 at 17:54):The "small enough" part being the singleton business?
Ali Caglayan (Apr 01 2022 at 17:57):Are the small ones the same ones picked out by SProp? Acc etc.?
Gaëtan Gilbert (Apr 01 2022 at 17:58):rules for non squashed Prop:
Gaëtan Gilbert (Apr 01 2022 at 17:59):Acc is still Prop with indices matter (it has no indices thanks to non recursively uniform parameters)
Ali Caglayan (Apr 01 2022 at 18:02):if indices matter, all indices in Prop or SProp
Is it known that this causes problems when dropped?
Gaëtan Gilbert (Apr 01 2022 at 18:03):it's the definition of indices matter
Ali Caglayan (Apr 01 2022 at 18:03):I was always under the impression that -indices-matter was really talking about universe levels not comparing between prop and other sorts.
Gaëtan Gilbert (Apr 01 2022 at 18:04):I don't know what that's supposed to mean so I can't tell if it's correct
Ali Caglayan (Apr 01 2022 at 18:05):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?
Ali Caglayan (Apr 01 2022 at 18:06):My point is that prop is not an ordinary universe level
Gaëtan Gilbert (Apr 01 2022 at 18:07):universe rules for inductives in general, let U be the sort of the inductive
OR U impredicative and the inductive is squashed
Gaëtan Gilbert (Apr 01 2022 at 18:09):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
Ali Caglayan (Apr 01 2022 at 18:11):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.
Gaëtan Gilbert (Apr 01 2022 at 18:12):too strict for what? it's consistent without axioms since no-indices-matter is consistent
Gaëtan Gilbert (Apr 01 2022 at 18:13):so that we don't compare between SProp,Prop and Set,Type.
WDYM?
Ali Caglayan (Apr 01 2022 at 18:15):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.
Gaëtan Gilbert (Apr 01 2022 at 18:17):because of the constructor argument
univ poly does nothing on this
Ali Caglayan (Apr 01 2022 at 18:18):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.
Gaëtan Gilbert (Apr 01 2022 at 18:20):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
Gaëtan Gilbert (Apr 01 2022 at 18:21):so you can't have indices-matter with unsquashed eq in prop
Gaëtan Gilbert (Apr 01 2022 at 18:23):(I should have remembered that instead of saying stuff about how hott doesn't care what we do with prop)
Ali Caglayan (Apr 01 2022 at 18:25):Is that transformation detailed anywhere?
Gaëtan Gilbert (Apr 01 2022 at 18:27):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)
Ali Caglayan (Apr 01 2022 at 18:28):Right, I've seen this before actually
Ali Caglayan (Apr 01 2022 at 18:29):But I saw it in a different dress. Its the translation between indexed W-types and W-types?
Ali Caglayan (Apr 01 2022 at 18:30):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
Ali Caglayan (Apr 01 2022 at 18:30):There is no UIP involved in this translation however
Gaëtan Gilbert (Apr 01 2022 at 18:31):mine doesn't use uip either
it's probably basically the same thing
Ali Caglayan (Apr 01 2022 at 18:31):However these IW-types inherit their "indices mattering" from the definition of the IW-type
Ali Caglayan (Apr 01 2022 at 18:32):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
Ali Caglayan (Apr 01 2022 at 18:33):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.
Gaëtan Gilbert (Apr 01 2022 at 18:33):InductiveS is a description of an inductive (with only recursive parameters)
indT implements it with indices
indT' with nonrec params
Gaëtan Gilbert (Apr 01 2022 at 18:38):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
Ali Caglayan (Apr 01 2022 at 18:42):Your formalization is very cool.
Ali Caglayan (Apr 01 2022 at 18:42):Thank you very much for the interesting discussion.
Ali Caglayan (Apr 01 2022 at 18:43):I seem to recall an example of -indices-matter breaking things in the test-suite for non-prop related things.
Ali Caglayan (Apr 01 2022 at 18:45):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
Ali Caglayan (Apr 01 2022 at 18:45):Not in the test-suite actually
Ali Caglayan (Apr 01 2022 at 18:46):So A can be in a big universe but if_spec lands in Set
Gaëtan Gilbert (Apr 01 2022 at 19:15):what about it?
Last updated: Dec 05 2023 at 05:01 UTC