[TYPES] Question about UIP and decidable equality

[Talia Ringer]

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