Missing cast properties

[gallais]

Realised tonight we don't have these (and their equivalents for Vec)

cast-is-id : ∀ {m} (eq : m ≡ m) (k : Fin m) → cast eq k ≡ k
cast-is-id eq Fin.zero    = refl
cast-is-id eq (Fin.suc k) = cong Fin.suc (cast-is-id (suc-injective eq) k)

cast-is-subst : ∀ {m n} (eq : m ≡ n) (k : Fin m) → subst Fin eq k ≡ cast eq k
cast-is-subst refl k = sym (cast-is-id refl k)

Note that it would also be nice to prove commutation lemmas for subst &
constructors for the various inductive types we have.

[JacquesCarette]

I also ended up needing

  cast-cast-is-id : ∀ {m n} (eq₁ : m ≡ n) (eq₂ : n ≡ m) (k : Fin n) → cast eq₁ (cast eq₂ k) ≡ k
  cast-cast-is-id {ℕ.suc m} {.(ℕ.suc _)} eq₁ eq₂ F.zero = refl
  cast-cast-is-id {ℕ.suc m} {.(ℕ.suc _)} eq₁ eq₂ (F.suc k) = cong Fin.suc (cast-cast-is-id (suc-injective eq₁) (suc-injective eq₂) k)

  cast-trans : ∀ {m n o} (eq₁ : m ≡ n) (eq₂ : n ≡ o) (k : Fin m) → cast (trans eq₁ eq₂) k ≡ cast eq₂ (cast eq₁ k)
  cast-trans {ℕ.suc m} {ℕ.suc n} {ℕ.suc o} eq₁ eq₂ F.zero = refl
  cast-trans {ℕ.suc m} {ℕ.suc n} {ℕ.suc o} eq₁ eq₂ (F.suc k) = cong Fin.suc (cast-trans (suc-injective eq₁) (suc-injective eq₂) k)

where I did need to expand out those implicits to get the casts to fire.

[gallais]

cast-cast-is-id seems to be a direct corollary of cast-is-id and cast-trans.

[JacquesCarette]

That could be - I proved cast-cast-is-id first, and then cast-trans was needed later...

[jamesmckinna]

Can/Should we (try to) do this for milestone 2.0?