Theoretical Computer Science
type-theory functional-programming dependent-type typed-lambda-calculus proof-assistants
Updated Sun, 29 May 2022 12:42:30 GMT

Structural equality of Pi Types with heterogeneous equality?


I'm trying to implement a proof of the following type:

(X X' : Type0) -> (Y : (X -> Type0)) (Y' : (X' -> Type0) -> (X Type0~=~Type0 X') 
-> ( Y (X -> Type0)~=~(X' -> Type0) Y' )
-> ((x : X) -> Y x) Type0~=~Type0 ((x' : X') -> Y' x')

i.e. if we have two function types with equal domain and codomain, then the pi types are themselves equal.

I'm using (z Z~=~W w) to denote McBride's Heterogeneous equality between (z : Z) and (w : W).

I'm wondering, can we prove this:

  1. with dependent pattern matching?
  2. using just the J axiom for heterogeneous equality?
  3. Using J and K for heterogeneous equality?

I can see how I can start with a proof that ((x : X) -> Y x) ~=~ ((x : X) -> Y x), but if I use J to rewrite X to X', then (Y x') is ill typed.

I think I can see how to do it with dependent pattern matching, because matching on the proof of (X ~=~ X') rewrites X' to X both in the goal type and in the context for the goal. And I know that dependent pattern matching can be decomposed to eliminators + Axiom K a la Goguen et al. But it's not immediately clear to me how to do the proof directly, and whether it relies on K.



Solution

I am not aware that J or K exists for heterogeneous equality. It does not need an elimination principle, because it can be simply defined as a sigma type:

coe : {i}{A B : Set i}  A  B  A  B
HEq :  {i}{A B : Set i}  A  B  Set _
HEq {_}{A} {B} x y =  (A  B)  p  coe p x  y

To do anything with HEq, it is enough to consider J and K for propositional equality. Dependent pattern matching is usually equivalent to J + K, although in Agda we can have pattern matching which is equivalent only to J.

So the question boils down to whether we can prove your lemma with J, or we need K as well. I prefer to work with uniqueness of identity proofs (UIP) instead of K (they are logically equivalent), so let's do that.

UIP :  {i}{A : Set i}{x : A}{p : x  x}  p  refl

The answer is that we need UIP. Writing the lemma in Agda:

lem :
   (A A : Set)
    (A : HEq A A)
    (B : A  Set)
    (B : A  Set)
    (B : HEq B B)
   HEq ( x  B x) ( x  B x)
lem A A (p , A) B B (q , B) = ?

It jumps at us that

A : coe p A  A
p   : Set  Set

In the absence of UIP, it is not provable that A A, and therefore lem is not provable either. We can make it work with UIP. Agda code with intentionally puritan J usage:

{-# OPTIONS --without-K #-}
open import Data.Product
infix 4 __
data __ {a} {A : Set a} (x : A) : A  Set a where
  refl : x  x
postulate
  UIP :  {i}{A : Set i}{x : A}{p : x  x}  p  refl
J :
   { }{A : Set } {x : A}(P :  y  x  y  Set )
   P x refl  {y : A}  (w : x  y)  P y w
J P pr refl = pr
tr :  {i j}{A : Set i}(B : A  Set j){a : A}{a : A}(a : a  a)  B a  B a
tr B p x = J ( x _  B x) x p
coe : {i}{A B : Set i}  A  B  A  B
coe = tr ( x  x)
ap : {i j}{A : Set i}{B : Set j}(f : A  B){a a : A}(a : a  a)
      f a  f a
ap f p = tr ( a  f _  f a) p refl
sym :  {i}{A : Set i}{x y : A}  x  y  y  x
sym p = tr ( y  y  _) p refl
HEq :  {i}{A B : Set i}  A  B  Set _
HEq {_}{A} {B} x y =  (A  B)  p  coe p x  y
lem :
   (A A : Set)
    (A : HEq A A)
    (B : A  Set)
    (B : A  Set)
    (B : HEq B B)
   HEq ( x  B x) ( x  B x)
lem A A (p , A) B B (q , B) =
  tr ( p  (A : coe p A  A)  HEq ( x  B x) ( x  B x))
     (sym (UIP {p = p}))
     ( A 
          refl ,
          J ( A A   B B (q : (A  Set)  (A  Set))
                       coe q B  B
                       ((x : A)  B x)  ((x : A)  B x))
            ( B B q B 
               tr ( q  coe q B  B  ((x : A)  B x)  ((x : A)  B x))
                  (sym (UIP {p = q}))
                  ( B  ap ( f   x  f x) B)
                  B)
            A B B q B)
     A

This might seem a handful, but after some practice such code is a mechanical exercise which generally follows the compilation of pattern matching.

At this point we might ask if a variant of the lemma is provable only with J. The following is such, for example.

lemJ :
   (A A : Set)
    (A : A  A)
    (B : A  Set)
    (B : A  Set)
    (B : tr ( X  X  Set) A B  B)
   ( x  B x)  ( x  B x)
lemJ A A A B B B =
  J ( A A   B B (B : tr ( X  X  Set) A B  B)
               ((x : A)  B x)  ((x : A)  B x))
    ( B B B  ap ( f   x  f x) B)
    A B B B





External Links

External links referenced by this document:

References