Example for different equality proofs

Question

I am looking for an example in Coq for different equality proofs.
This means:
Give some type T and two elements x,y : T and two proofs p1 , p2 : x=y with p1<>p2.

Answer 1

This is a classic example of incompleteness in Coq. In its basic theory (that is, without assuming any additional axioms), it is not possible to prove or disprove the following statement:

exists (T : Type) (x y : T) (p q : x = y), p <> q.

Thus, we cannot usually exhibit different proofs of equality between two points. What does this mean in practice? If you want to use Coq's theory as is, you must avoid talking about equalities between equality proofs, because there is nothing very useful we can do with them. The only exception are types with decidable equality, those for which we can prove forall x y : T, x = y \/ x <> y; in those cases, we can show the unicity of identity proofs:

UIP : forall (x y : T) (p q : x = y), p = q.

If we are willing to add axioms, the story changes. One of the axioms we can add is proof irrelevance, a generalization of the UIP principle above. It says

proof_irrelevance : forall (P : Prop) (p q : P), p = q.

Coq's theory was designed to allow such an axiom without incurring contradiction, and many developments do so. In that case, UIP holds for all types, and not just those that have decidable equality.

On the other hand, there are useful axioms we can add that are incompatible with UIP. The most famous one is the univalence axiom from Homotopy type theory, which roughly says that for all types A and B there is a one-to-one correspondence between proofs of equality A = B and equivalences between A and B -- that is, functions in A -> B that have a two-sided inverse. Here is a simplified version, just to explain the basic idea:

Record Equiv (A B : Type) : Type := {
  equiv_l : A -> B;
  equiv_r : B -> A;
  _ : forall x, equiv_l (equiv_r x) = x;
  _ : forall x, equiv_r (equiv_l x) = x
}.

Axiom univalence : forall A B, Equiv (A = B) (Equiv A B).

If we assume this axiom, we can show, for instance, that there are two different proofs of equality in bool = bool: one that corresponds to the identity function, and another one that corresponds to Boolean negation:

Definition id_Equiv : Equiv bool bool.
Proof.
  apply (BuildEquiv _ _ (fun x => x) (fun x => x)); trivial.
Defined.

Definition negb_Equiv : Equiv bool bool.
Proof.
  apply (BuildEquiv _ _ negb negb); intros []; trivial.
Defined.

Lemma not_UIP : exists p q : bool = bool :> Type , p <> q.
Proof.
  exists (equiv_r _ _ (univalence bool bool) id_Equiv).
  exists (equiv_r _ _ (univalence bool bool) negb_Equiv).
  intros H.
  assert (H' : id_Equiv = negb_Equiv).
  { now rewrite <- (equiv_lr _ _ (univalence bool bool)), <- H,
                   (equiv_lr _ _ (univalence bool bool)). }
  assert (H'' : equiv_l _ _ id_Equiv true = equiv_l _ _ negb_Equiv true).
  { now rewrite H'. }
  simpl in H''. discriminate.
Qed.

Bear in mind that the actual definition of univalence is more involved than the one I gave above, which I am not even completely certain of. You cannot just copy what I gave above and expect it to work smoothly. For the real definition, see IsEquiv here and isequiv_equiv_path here. If you want to use the axiom, it is better to work with one of the Homotopy type theory libraries available online: HoTT and UniMath. Note that the first one is actually a slightly modified version of Coq.