[Agda] Associativity of vector concatenation
Tom Jack
tom at tomjack.co
Fri Oct 28 01:47:01 CEST 2016
I guess that you are referring to the 'John Major' equality in Conor
McBride's thesis here? http://strictlypositive.org/thesis.pdf
In section 5.1.3 (page 120), there is the following note:
Observe that eqElim is not the elimination rule which one would expect if
> ≃ was inductively defined. The ‘usual’ rule eliminates over all the
> formable equations, and it is quite useless...
Even if the usual rule is useless, it is what we will have in Agda for an
inductively defined heterogeneous equality :).
It is trivial using the 'useless' rule to give an equivalence between (a ≅
b) and (A , a) ≡ (B , b), where _≡_ is the usual homogeneous equality. So
then _≅_ will be related to your _≡[_]_ as total space to fiber.
On Thu, Oct 27, 2016 at 3:49 PM, Martin Escardo <m.escardo at cs.bham.ac.uk>
wrote:
>
>
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161027/97c4bcb3/attachment.html
More information about the Agda
mailing list