Structural equality of Pi Types with heterogeneous equality?

Question

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.

Answer 1

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₀₁