[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi Talia, In general the situation that you are describing here between I, B, J and C does not seem to be strong enough to derive any interesting properties about equalities in I. Consider the following example: I = Type B(A : I) = sigma (n : nat) . (Vec A n) J = nat C(n : J) = sigma (A : Type) . (Vec A n) Here "equiv (sigma (i : I) . B i) (sigma (j : J) . C j)” holds trivially but that does not say anything about equalities in I. Maybe some constraint on I, B, J, and C would make it possible to say something about equalities in I in the specific case(s) you are working with. One specific case that comes to mind would be if there is a bijection between f : I -> J such that forall i : I, equiv B(i) C(f(i)). However in that case I would have decidable equality (and hence UIP) if J has decidable equality. So it is probably not very useful for you. Regards, Amin > On 17 Feb 2020, at 13:39, Talia Ringer <[email protected]> wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hello, > > I have a question that has been bugging me for a long time, and I'm hoping > someone has some insight. I'm working in vanilla CIC, and right now I'm > interested in types "A : Type" and "B : I -> Type" for which there is a > function "indexer" that makes the following type equivalence hold: > > "forall i : I, equiv { a : A | indexer a = i} (B i)" > > Everyone's favorite example of this is a list, a vector, and the length > function. > > I know for a fact that when the type "I" of the index "i" has decidable > equality, without any axioms, I can derive that UIP holds on that index > type. That's true in the vector case, for example. > > Where I'm stuck is that I sometimes have types for which equality on "I" is > in general not decidable, but for which I can choose some "J" with > decidable equality and some "C : J -> Type" such that: > > "equiv (sigma (i : I) . B i) (sigma (j : J) . C j)" > > This means it's very easy to work over C, since I get UIP over the index. > But I'm not interested in functions and theorems that are defined over C. I > would like them over B. And I would like for equalities of equalities of > the indices of B to not be painful. > > Is there anything that I can say, without any additional axioms, about how > equalities between the indices of B relate to one another? That is, can I > get a result similar to UIP holding on the indices of B, even if it does > not hold in general on I? If so, how? If not, why not, and what additional > axioms would be necessary? > > Thanks! I'm happy to clarify if anyone is confused about any details; it > was hard to make this concise. > > Talia
