如何在Cubical Agda中证明两次谬论模式应用结果等价？

在定义自然变换并证明其交换图可交换时，遇到核心问题：两次应用接收空类型的函数（即ex falso quodlibet原则，从谬论导出任意结论）的结果无法被判定为等价。

相关代码中的目标定义如下：

plugin1unit : NaturalTransformation idF (constantPolynomial ∘F plugIn1)
plugin1unit = record { 
    η = λ X → (λ x → x , λ _ → tt) ⇄ λ fromPos () ;
    commute = λ f@(mapDir ⇄ mapPos) → {!   !} ;
   }
}

该commute目标的类型为：

((λ x → Arrow.mapPosition f x , (λ _ → tt)) ⇄
       (λ fromPos z → Arrow.mapDirection f fromPos ((λ ()) z)))
      Cubical.≡
      ((λ x → Arrow.mapPosition f x , (λ x₁ → tt)) ⇄
       (λ fromPos z → (λ ()) z))

以下是逐步细化目标时遇到的错误：

1. 细化为：

commute = λ f@(mapDir ⇄ mapPos) → λ i → {!   !} ;

此时目标类型为：

Arrow X
      (MkPolynomial
       (Σ (Polynomial.position Y₁) (λ x → Polynomial.direction Y₁ x → ⊤))
       (λ _ → ⊥))

2. 省略部分自动推导步骤后，细化为：

commute = λ f@(mapDir ⇄ mapPos) → λ i → (λ x → mapDir x , λ x₁ → tt) ⇄ {!   !} ;

此时目标类型为：

(fromPos : Polynomial.position X) →
      ⊥ → Polynomial.direction X fromPos

3. 进一步细化为接收两个参数的函数（其中一个为空类型⊥）：

commute = λ f@(mapDir ⇄ mapPos) → λ i → (λ x → mapDir x , λ x₁ → tt) ⇄ λ fromPos x → {!   !} ;

但使用空模式匹配的常规方案会报错：

(λ { fromPos () }) fromPos z != Arrow.mapDirection f fromPos ((λ ()) z)

若定义一个比目标类型更通用的函数：

fromAnythingToAnythingElse : {A B : Set} → A → ⊥ → B
fromAnythingToAnythingElse x ()

并将其填入第二步的目标中，会出现无法实例化元变量的错误。

核心疑问：为何(λ ()) z会与任何表达式不等价？根据定义，它应该能返回任意类型！

内容的提问来源于stack exchange，提问作者André Muricy