The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You should prove that UIP is preserved by sigma types.  Then you can turn dependent fields into a single non-dependent one, and use UIP on that.

Given that, I think the appropriate way to get UIP on Fin is to first have some isomorphic type like

Inductive Fin' (n : nat) := FinZ : Fin' n | FinS : forall m, n = S m -> Fin' m -> Fin' n.

You should then separately prove that this is isomorphic to your Fin type, and that this Fin type has UIP for each n.  (Alternatively, you could pick the isomorphic type to be { ls : list unit | length ls <= n }, but that might be cheating.)

On Thu, Sep 1, 2016 at 2:47 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 09/01/2016 02:24 AM, Jason Gross wrote:
> I'm no longer convinced this can be done, but I bet asking on hott-cafe, or
> looking at the file PathGroupoid in the HoTT library, could get you ask
> answer (the HoTT name for [f_equal] is [ap])

I may try that, as I've hit another road block: types with indices or
dependent fields.  None of the methods discussed so far work for those,
even when using a dependent form of f_equal based on eq_rect.  For
instance, try to get UIP on Fin from UIP on nat.

-- Jonathan