Re: [TYPES] Question about UIP and decidable equality

[ 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