[Agda] Are two equal things the same?

[Martin Escardo]

Thanks, Dan, for both fulfilling my wish and pointing out what I was 
missing. Your blog post is very nice and clear!

Best,
Martin

On 16/12/11 23:38, Dan Licata wrote:
> 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

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe