[Agda] Associativity of vector concatenation

[Martin Escardo]

On 27/10/16 23:00, Tom Jack wrote:
> Does the elimination rule for heterogeneous equality really imply K?

If I am not mistaken, this was proved by the very person who introduced
heterogeneous equality in the first place, in his PhD thesis.

But I am open to be corrected.

Martin


> 
> Take the type as defined in agda stdlib
> Relation.Binary.HeterogeneousEquality:
> 
>     data _≅_ {i} {A : Set i} (x : A) : {B : Set i} → B → Set i where
>        refl : x ≅ x
> 
> This is the eliminator, right?
> 
>     elim-≅ : ∀ {i j} {A : Set i} {x : A}
>       (C : {B : Set i} {y : B} → x ≅ y → Set j)
>       → C refl
>       → {B : Set i} {y : B} (p : x ≅ y) → C p
>     elim-≅ C c refl = c
> 
> This does not imply K, does it?
> 
> On Thu, Oct 27, 2016 at 2:30 PM, Martin Escardo <m.escardo at cs.bham.ac.uk
> <mailto:m.escardo at cs.bham.ac.uk>> wrote:
> 
> 
>     Often people mention the formulation and proof of associativity of
>     vector concatenation as something tricky.
> 
>     The problem, of course, is that for vectors xs, ys, and zs, the
>     concatenations
> 
>         xs ++ (ys ++ zs)    of length l + (m + n)
> 
>     and
> 
>         (xs ++ ys) ++ zs    of length (l + m) + n
> 
>     belong to the different (but isomorphic) types
> 
>         Vec X  (l + (m + n)) and Vec X ((l + m) + n).
> 
>     One approach considers heterogeneous equality, which is a notion of
>     equality that allows to compare elements of different types. A
>     limitation of this equality is that its elimination rule implies the K
>     axiom (any two proofs of equality are equal), which is incompatible
>     with univalent type theory as in the HoTT Book or as in Cubical Type
>     Theory, which are type theories some people wish to either use or at
>     least be compatible with.
> 
>     Not only can we be compatible with univalent type theory, but also
>     we can learn from it (even without using univalence or other
>     features that
>     don't belong to Martin-Loef Type Theory as represented by Agda).
> 
>     I would like to advertise this here, as the ideas are of general use,
>     even if one is not interested in HoTT, and hopefully intuitive and
>     natural too.
> 
>     Given a type X and a type family F:X->Set, suppose we have x,y:X,
>     p:x≡y and a : F x and b : F y. Even though x and y are equal, the
>     types F x and F y are not the same (they are equal under univalence,
>     but we don't want to use this). So can't compare a and b for equality.
> 
>     But we can define a notion of equality between the types F x and F y,
>     dependent on p:x≡y,
> 
>         a ≡[ p ] b,
> 
>     by
> 
>         a ≡[ refl ] b   =   a ≡ b.
> 
>     In particular, we get
> 
>     _≡[_]_ : ∀ {X} {m n} → Vec X m → m ≡ n → Vec X n → Set
>     xs ≡[ refl ] ys = xs ≡ ys
> 
>     Then vector associativity becomes
> 
>     ++-assoc : ∀ {X : Set} l m n (xs : Vec X l) (ys : Vec X m) (zs : Vec
>     X n)
>             → xs ++ (ys ++ zs)  ≡[ +-assoc l m n ]  (xs ++ ys) ++ zs
> 
>     where
> 
>     +-assoc : ∀ l m n → l + (m + n) ≡ (l + m) + n.
> 
>     Its proof is the same as that of associativity of list concatenation
>     (where the problem discussed in this message doesn't arise), but
>     taking care of the extra subscript p for dependent equality, in a way
>     that doesn't become disruptive or require new ideas, as shown here:
> 
>     http://www.cs.bham.ac.uk/~mhe/agda/VecConcatAssoc.html
>     <http://www.cs.bham.ac.uk/~mhe/agda/VecConcatAssoc.html>
> 
>     The idea is very similar to using heterogeneous equality, as you will
>     see.
> 
>     Anyway, I wanted to advertise this idea coming from univalent type
>     theory, and try to convince you of its simplicity and naturality and
>     usefulness.
> 
>     Martin
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
> 
> 

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