[Agda] Associativity of vector concatenation

[Martin Escardo]

On 27/10/16 22:55, Andrea Vezzosi wrote:
>> 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).
> 
> Side note: You can prove F x and F y equal without univalence, "ap F
> p" (aka "cong F p") suffices.

Yeah. This is a wart in my post, which I noticed and waited for somebody
to point out. :-)

Martin

> 
> 
> On Thu, Oct 27, 2016 at 11:30 PM, Martin Escardo
> <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
>>
>> 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
>> https://lists.chalmers.se/mailman/listinfo/agda

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