The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Here's the pointed version of UIP-respecting-isomorphism:

Set Implicit Arguments.

(** * Step 1: UIP ports across type isomorphism at a point. *)

Section UIP_iso.

   Variables A B : Type.

   Variable AtoB : A -> B.

   Variable BtoA : B -> A.

   Hypothesis AtoB_BtoA : forall a, AtoB (BtoA a) = a.

   Lemma f_equal_cancel : forall (x y : B) (e : x = y),

       e = match AtoB_BtoA x in _ = X return X = _ with

           | eq_refl =>

             match AtoB_BtoA y in _ = Y return _ = Y with

             | eq_refl => f_equal AtoB (f_equal BtoA e)

             end

           end.

   Proof.

     intros.

     subst.

     simpl.

     generalize (AtoB_BtoA y).

     destruct e.

     reflexivity.

   Qed.

   Theorem UIP_iso_pointed : forall (b : B) (e : b = b), f_equal BtoA e = eq_refl -> e = eq_refl.

   Proof.

     intros b e H.

     rewrite (f_equal_cancel e), H; simpl.

     case (AtoB_BtoA b); reflexivity.

   Qed.

End UIP_iso.

I think the most general form here is the encode-decode method of homotopy type theory, which is a method for classifying the equality type of types.  There's some code here: https://github.com/HoTT/HoTT/issues/757#issuecomment-102128029

On Wed, Aug 31, 2016 at 4:04 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

>> I wasn't able to use Adam's scheme on recursive inductive types like
>> list or nat because it requires UIP to be universal on the substructure,
>> but in an inductive proof, one only has UIP at a point on the
>> substructure via the inductive hypothesis.  I tried to rewrite Adam's
>> UIP_iso proof so that it only requires UIP for the type A at a single
>> point, but failed.