[Agda] Are two equal things the same?

[Dan Licata]

Hi Martin,

You can definitely prove two-equal-things-are-the-same from J, without
using UIP.  In fact, two-equal-things-are-the-same together with 'subst'
gives you J.  

The reason 'conjecture' doesn't type check is that 

s : x ≣ y
Refl x : x ≣ x

and you can't state an equation between two things with different types.

The reason lemma does is that at the type 

Σ (\ y -> x ≣ y) 

you can state an equation between

(y , s) and (x, Refl).

Homotopy-wise, think of Σ (\ y -> x ≣ y) as "paths with a free end point
y".  There are more equations between paths with a free end-point than
between paths with two fixed end-points.  In fact, J says that the space
of "paths from x with a free end point" is inductively generated by
(x,Refl).  See this blog post for more:

http://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/

-Dan

On Dec16, Martin Escardo wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda