The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

On 09/02/2016 01:08 AM, Jason Gross wrote:
> 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.

A proof that UIP is preserved by sigma types. Remark that eq_rect
is useful here to implement equality between terms of "isomorphic"
dependent types (ie P a <~> P b when a = b).

Dominique

-----------------

Definition uip (X : Type) := forall (x : X) (H : x = x), H = eq_refl.

Section sigma_type.

  Variables (X : Type) (P : X -> Type).

  Let sigma_eq (x y : X) (H : x = y) (a : P x) (b : P y) : eq_rect _ P a
_ H = b -> existT _ x a = existT _ y b.
  Proof.
    destruct H; simpl.
    intros []; reflexivity.
  Defined.

  Let eq_sigma_inv (x : sigT P) : forall y, x = y -> Prop :=
    match x with
      | existT u a => fun y =>
      match y with
        | existT v b => fun H => exists (e1 : u = v) (e2 : eq_rect _ P a
_ e1 = b), H = sigma_eq _ _ e1 _ _ e2
      end
    end.

  Let eq_inv x y H : @eq_sigma_inv x y H.
  Proof.
    subst y.
    destruct x as [ x t ]; simpl.
    exists eq_refl; simpl.
    exists eq_refl; reflexivity.
  Qed.

  Hypothesis uip_X : uip X.
  Hypothesis uip_P : forall x, uip (P x).

  Theorem uip_sigma_type : uip (sigT P).
  Proof.
    intros [ x t ] H.
    generalize (eq_inv _ _ H); simpl.
    intros (e1 & H1).
    rewrite (uip_X _ e1) in H1; simpl in H1.
    destruct H1 as (e2 & H2).
    rewrite (uip_P _ _ e2) in H2; assumption.
  Qed.

End sigma_type.

Check uip_sigma_type.