Coq casts for function domains and codomains and results
Definition fun_dom_cast{X Y Z : Type}(eq : X = Y)(f : X → Z) : Y → Z :=
match eq in _ = Y' return Y' → Z with
| eq_refl ⇒ f
end.
Lemma dom_map_cast :
∀(X Y Z : Type)(T : Type → Type)
(TM : ∀(A B : Type), (A → B) → (T A → T B))
(eq_lift : ∀(A B : Type), A = B → T A = T B)
(eq : X = Y)(f : X → Z),
(∀(A : Type), eq_lift A A eq_refl = eq_refl) →
TM Y Z (fun_dom_cast eq f) =
fun_dom_cast (eq_lift X Y eq) (TM X Z f).
Definition fun_codom_cast{X Y Z : Type}(eq : Y = Z)(f : X → Y) : X → Z :=
match eq in _ = Z' return X → Z' with
| eq_refl ⇒ f
end.
Lemma codom_map_cast :
∀(X Y Z : Type)(T : Type → Type)
(TM : ∀(A B : Type), (A → B) → (T A → T B))
(eq_lift : ∀(A B : Type), A = B → T A = T B)
(eq : Y = Z)(f : X → Y),
(∀(A : Type), eq_lift A A eq_refl = eq_refl) →
TM X Z (fun_codom_cast eq f) =
fun_codom_cast (eq_lift Y Z eq) (TM X Y f).