[Agda] Dependent injection without K?

[Matthieu Sozeau]

Le 21 févr. 2011 à 18:50, Brandon Moore a écrit :

> I am trying to prove something like fcinj in Coq. The code below compiles
> normally, but is rejected with the --without-K flag. Is this sort of goal
> provable without some sort of equality axiom?
> 
> data ℕ : Set where
>  Z : ℕ
>  S : ℕ → ℕ
> 
> data Fin : ℕ → Set where
>  fz : ∀{n} → Fin (S n)
>  fs : ∀{n} → Fin n → Fin (S n)
> 
> data FinCopy : ∀{n} → Fin n → Set where
>  FZ : ∀{n} → FinCopy (fz {n})
>  FS : ∀{n f} → FinCopy {n} f → FinCopy (fs f)
> 
> fcinj : ∀{n f} → FinCopy (fs {n} f) → FinCopy f
> fcinj (FS y) = y

Hi,

  It should be provable without K, as it is provable in Coq
without K. Something like the following should work:

fspred : forall {n} (f : fin n) -> Set
fspred fz = nat
fspred (fs f) = fincopy f

fsmatch : forall {n f} (fc : fincopy {n} f) -> fspred f
fsmatch FZ = Z
fsmatch (FS y) = y.

Then fcinj is just an instance of fsmatch.
-- Matthieu