[Agda] Associativity of vector concatenation
Tom Jack
tom at tomjack.co
Fri Oct 28 00:00:19 CEST 2016
Does the elimination rule for heterogeneous equality really imply K?
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>
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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161027/be036103/attachment.html
More information about the Agda
mailing list