[Agda] Are two equal things the same?

[Martin Escardo]

Are two equal things the same?

Let me not have any implicit parameter other than Sets, so that I can
be explicit about what I am talking about:

\begin{code}
module AreTwoEqualThingsTheSame where

data _≣_ {X : Set} : X → X → Set where
   Refl : ∀(x : X) → x ≣ x

data Σ {X : Set} (Y : X → Set) : Set where
      _,_ : (x : X) → Y x → Σ \(x : X) → Y x

infix 30 _≣_
infixr 30 _,_
\end{code}

This is what I would like to witness:

\begin{code}
two-equal-things-are-the-same : {X : Set} →
  (t : Σ \(x : X) → Σ \(y : X)→ x ≣ y) → Σ \(z : X) → (z , z , Refl z) ≣ t
two-equal-things-are-the-same {X} (x , y , s) = (x , lemma)
  where
   observation : x ≣ y
   observation = s

   lemma : (x , x , Refl x) ≣ (x , y , s)
   lemma = {!!}
\end{code}

The code produced so far type checks (but has a gap).

In order to fill the gap, we would have to show that, in particular,
the equation Refl x ≣ s holds. This seems to amount to the uniqueness
of identity proofs:

\begin{code}
uip : {X : Set} → ∀(x y : X) → ∀(r s : x ≣ y) → r ≣ s
uip x .x (Refl .x) (Refl .x) = Refl (Refl x)
\end{code}

But I don't think so. In fact, while the above typechecks, if you add
the following conjecture to the above code, you now get something that
doesn't typecheck (it complains, in the definition of the conjecture,
that y != x):

\begin{code}
two-equal-things-are-the-same' : {X : Set} →
  (t : Σ \(x : X) → Σ \(y : X)→ x ≣ y) → Σ \(z : X) → (z , z , Refl z) ≣ t
two-equal-things-are-the-same' {X} (x , y , s) = (x , lemma)
  where
   observation : x ≣ y
   observation = s

   conjecture : Refl x ≣ s
   conjecture = ?

   lemma : (x , x , Refl x) ≣ (x , y , s)
   lemma = {!!}
\end{code}

So, it is not that the conjecture can't be proved: it can't even be
formulated (the formulation doesn't type check).

But how come the lemma type checks, but the conjecture doesn't? I am
not claiming this is a bug, but I am puzzled. In fact, suppose you
wanted to replace "s" in uip above by Refl z for suitable z (e.g. x or
y): you won't succeed, because Agda will complain that x != y, even if
x ≡ y is the assumption, and this does seem right. It seems that two
equal things cannot in general be proved to be the same, even if,
internally from the point of view of the compiler, they have to be the
same (definitionally). Or have I missed something? (I wish this is the
case.)

Martin