[Agda] Problem with propositional equality (or my understanding of it)

[José Pedro Magalhães]

Hi all,

(This post is in literate Agda.)

I hit a problem in Agda where I expect two ways of proving the same
thing to be equivalent, but Agda doesn't believe me. Let's say I
have the following two universes:

\begin{code}
module Test where

open import Data.Unit
open import Data.Maybe

data U₁ : Set where
  Z₁ : U₁
  S₁ : U₁ → U₁

⟦_⟧₁ : U₁ → Set
⟦ Z₁   ⟧₁ = ⊤
⟦ S₁ x ⟧₁ = Maybe ⟦ x ⟧₁

data U₂ : Set where
  Z₂ : U₂
  S₂ : U₂ → U₂

⟦_⟧₂ : U₂ → Set
⟦ Z₂   ⟧₂ = ⊤
⟦ S₂ x ⟧₂ = Maybe ⟦ x ⟧₂
\end{code}

It's pretty clear they are equivalent. Let's show that:

\begin{code}
U₁→U₂ : U₁ → U₂
U₁→U₂ Z₁     = Z₂
U₁→U₂ (S₁ x) = S₂ (U₁→U₂ x)

open import Relation.Binary.PropositionalEquality public

⟦⟧₁≡⟦⟧₂ : (C : U₁) → ⟦ C ⟧₁ ≡ ⟦ U₁→U₂ C ⟧₂
⟦⟧₁≡⟦⟧₂ Z₁     = refl
⟦⟧₁≡⟦⟧₂ (S₁ x) = cong Maybe (⟦⟧₁≡⟦⟧₂ x)
\end{code}

Now let's define a function on interpretations of the first universe,
to be used later. This function is nothing more than a "deep" identity:
\begin{code}
id₁ : (C : U₁) → ⟦ C ⟧₁ → ⟦ C ⟧₁
id₁ Z₁     tt       = tt
id₁ (S₁ x) (just y) = just (id₁ x y)
id₁ (S₁ x) nothing  = nothing
\end{code}

Alright. Now let's write conversion functions between the two universes.
Since we have a proof of equivalence of their interpretations, we reuse it:
\begin{code}
module FirstTry where

  ≡→ : {A B : Set} → A ≡ B → A → B
  ≡→ refl x = x

  ⟦⟧₁→⟦⟧₂ : (C : U₁) → ⟦ C ⟧₁ → ⟦ U₁→U₂ C ⟧₂
  ⟦⟧₁→⟦⟧₂ C = ≡→ (⟦⟧₁≡⟦⟧₂ C)
\end{code}

So far so good. Now let's prove that we can remove applications of
our identity function:
\begin{code}
  prop : (C : U₁) → (x : ⟦ C ⟧₁) → ⟦⟧₁→⟦⟧₂ C (id₁ C x) ≡ ⟦⟧₁→⟦⟧₂ C x
  prop Z₁     tt       = refl
  prop (S₁ x) (just y) = cong {!just!} (prop x y)
  prop (S₁ x) nothing  = refl
\end{code}

Unfortunately Agda does not accept the term in the hole, saying:
  just (≡→ (⟦⟧₁≡⟦⟧₂ x) (id₁ x y)) !=
  ≡→ (cong Maybe (⟦⟧₁≡⟦⟧₂ x)) (id₁ (S₁ x) (just y)) of type
  Maybe ⟦ U₁→U₂ x ⟧₂
  when checking that the expression cong ? (prop x y) has type
  ⟦⟧₁→⟦⟧₂ (S₁ x) (id₁ (S₁ x) (just y)) ≡ ⟦⟧₁→⟦⟧₂ (S₁ x) (just y)

This seems to be caused by us having written the function ⟦⟧₁→⟦⟧₂ using
⟦⟧₁≡⟦⟧₂. What if we write it by induction on the universe codes instead?
\begin{code}
module SecondTry where

  ⟦⟧₁→⟦⟧₂ : (C : U₁) → ⟦ C ⟧₁ → ⟦ U₁→U₂ C ⟧₂
  ⟦⟧₁→⟦⟧₂ Z₁     tt       = tt
  ⟦⟧₁→⟦⟧₂ (S₁ x) (just y) = just (⟦⟧₁→⟦⟧₂ x y)
  ⟦⟧₁→⟦⟧₂ (S₁ x) nothing  = nothing

  prop : (C : U₁) → (x : ⟦ C ⟧₁) → ⟦⟧₁→⟦⟧₂ C (id₁ C x) ≡ ⟦⟧₁→⟦⟧₂ C x
  prop Z₁     tt       = refl
  prop (S₁ x) (just y) = cong just (prop x y)
  prop (S₁ x) nothing  = refl
\end{code}

Now we can define prop as expected.

My question is: why?


Thanks,
Pedro