是否可定义相等类型间的值转换函数？Eq.subst限制适配问询

是可以定义的，标准库已经提供了开箱即用的实现，不需要手动实现基础版本。

1. 直接使用标准库cast函数 #

你给出的示例可以直接用cast完成：

example {α β : Type} (hab : α = β) (x : α) : β := cast hab x

cast的类型签名完全匹配你的需求：

cast : ∀ {α β : Sort u}, α = β → α → β

它没有将返回值限制在Prop宇宙，支持任意宇宙的类型转换。

2. 手动实现的方案 #

你提到的Eq.subst确实是特化到Prop的版本，但相等类型的 eliminator Eq.rec本身支持任意宇宙的 motive，你可以基于它自己实现转换函数：

def custom_cast {α β : Sort u} (hab : α = β) (x : α) : β :=
  Eq.rec (motive := fun t _ => α → t) (fun a => a) hab x

这里的 motive 可以返回任意Sort u，不存在Prop的限制，完全可以适配你的使用需求。

3. 更通用的依赖类型传输场景 #

如果你需要转换的是依赖于α的类型实例（比如F α转F β，其中F : Type → Type），可以结合congrArg使用cast：

example {F : Type → Type} {α β : Type} (hab : α = β) (x : F α) : F β :=
  cast (congrArg F hab) x

内容的提问来源于stack exchange，提问作者Yifan Dai