[Agda] Problem proving inequality with HeterogeneousEquality

[Nils Anders Danielsson]

On 2020-05-20 23:28, Roman wrote:
> I use what I call "heteroindexed equality", see
> https://lists.chalmers.se/pipermail/agda/2016/009069.html

> [_]_≅_ : ∀ {X : Set} {x y} → (Z : X → Set) → Z x → Z y → Set
> [_]_≅_ {x = x} {y} Z a b = (x , a) ≡ (y , b)

I have also used this kind of equality, in some project where I used the
K rule (back in 2011), and it worked well.

I used this kind of construction:

   record [Z] : Set where
     constructor [_]
     field
       {x} : X
       {y} : Y x
       z   : Z x y

Equality of two values z : Z x y and z′ : Z x′ y′ could then be
expressed as [ z ] ≡ [ z′ ].

-- 
/NAD