[Agda] Associativity of vector concatenation

[Dan Licata]

Hi,

Here’s the thread I had in mind from a “few” years ago :) 
https://lists.chalmers.se/pipermail/agda/2008/000153.html
See in particular Conor’s reply here:
https://lists.chalmers.se/pipermail/agda/2008/000155.html
and here:
https://lists.chalmers.se/pipermail/agda/2008/000159.html

In current Agda (2.5.1.1), it looks like the existential interpretation is there: you can prove (even without K) by pattern matching that

data HId {A : Set} (M : A) : {B : Set} → B → Set where
   HRefl : HId M M

is equivalent to 

(p : Id A B) * Id{B} (coe p a) b

See 
https://github.com/dlicata335/hott-agda/blob/master/misc/Heterogeneous.agda
for the main idea (I didn’t wrap with Sigma types).  

Note that Id (coe p a) b is equivalent to the inductive family path-over type 
PathOver (\X -> X) p a b, but I wanted to keep the file as small as possible.  

I didn’t include it in the file, but we know that that Sigma-type is equivalent to Id{(A : Set) * A} (A,a) (B,a), 
which is the construction Conor uses in his thesis Section 5.1.5 (http://strictlypositive.org/thesis.pdf)
to show that you can get heterogeneous equality from homogeneous equality with K.


Regarding UIP, it’s also constructed in Conor’s thesis, Sec 5. It’s described in the context of 
equality of telescopes, but here’s the special case of telescopes of length 1, inspired by that: 

Suppose you have heterogeneous equality with, as an elimination rule,
J for homogeneous instances of heterogeneous equality (i.e. J for HId {A} a {A} a’). 
(Note that Agda —without-K helpfully prevents you from proving this, or else we’d be in trouble!) 

From this, you get that such a homogeneous heterogeneous equality implies homogeneous equality
(without the coercion by an existentially quantified type equality), and 
this will be an equivalence because both types have the same intro and elim (refl and J).  
Moving along this equivalence, it suffices to prove UIP for homogeneous instances
of heterogeneous equality.  This follows from 

    UIP1' : {A : Set} {x : A} {y : A} (p : HId {A} x {A} y) → HId {HId x x} HRefl {HId x y} p 

which you can prove because using heterogeneous equality in the result gets around
the usual type checking failure that stops you from proving UIP.  Then the y=x case is a 
homogeneous instance of heterogeneous equality, so it can be converted to a homogeneous equality.  

-Dan

> On Oct 28, 2016, at 2:36 PM, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
> 
> 
> 
> On 28/10/16 15:59, Dan Licata wrote:
>>> The idea is very similar to using heterogeneous equality, as you will
>>> see.
>> 
>> More precisely, I think that heterogeneous equality (a:A) == (b:B) is equivalent to either
>> (writing PathOver F p a b for your a ≡[ p ] b to make the type family explicit,
>> and writing == for the homogeneous identity type)
>> 
>> (p : A == B) -> PathOver (\X -> X) p a b
>> 
>> or
>> 
>> (p : A == B) * PathOver (\X -> X) p a b
>> 
>> depending on what the rules for the (a:A) == (b:B) type are
>> (there was a thread a few years ago about whether this should imply A==B or require A==B, but I can’t find it right now).
> 
> I'd also like to understand this, and also the claim that the elimination principle for heterogeneous equality implies K.
> 
> Martin
>