[Agda] Associativity of vector concatenation

[Thorsten Altenkirch]

Indeed equalities living over equalities show up very naturally in cubical
type theory.

http://www.cs.nott.ac.uk/~psztxa/talks/icms16.pdf


Thorsten

On 27/10/2016, 22:30, "agda-bounces at lists.chalmers.se on behalf of Martin
Escardo" <agda-bounces at lists.chalmers.se on behalf of
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





This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.