[Agda] Congruence and substitutivity rules in heterogeneous equality

[Nils Anders Danielsson]

On 2009-07-15 08:47, Liang-Ting Chen wrote:
> Thanks for it ! How about cong ?

For cong I suspect that you want something like the following:

  cong : {A : Set} {B C : A → Set} {x y : A} {u : B x} {v : B y} →
         (∀ {x y} → B x ≡₁ B y → x ≡ y) →
         (f : ∀ {x} → B x → C x) → u ≅ v → f u ≅ f v
  cong inj f eq with inj (≅⇒≡₁ eq) | eq
  ... | refl | refl = refl

Here you can instantiate B with Vec T, for instance:

  cong′ : ∀ {T m n} {C : ℕ → Set} {xs : Vec T m} {ys : Vec T n}
          (f : ∀ {n} → Vec T n → C n) → xs ≅ ys → f xs ≅ f ys
  cong′ = cong helper
    where
    helper : ∀ {T m n} → Vec T m ≡₁ Vec T n → m ≡ n
    helper refl = refl

However, implementing the latter function directly is perhaps easier:

  cong″ : ∀ {T m n} {C : ℕ → Set} {xs : Vec T m} {ys : Vec T n}
          (f : ∀ {n} → Vec T n → C n) → xs ≅ ys → f xs ≅ f ys
  cong″ f refl = refl

> subst looks not possible to drop the annotation before unless it is
> evaluated?

I do not understand what this means.

-- 
/NAD



This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.