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