PS

Free theorem vs. dinaturality

圏論 Haskell

Free dinaturality

Free theoremはdinaturalityについても有効である(らしい)。

命題

Free naturalityが成立するならば、free dinaturalityも成立する。

以下、非常に怪しい証明･･･

証明

Twisted arrow category - PSによる、

  • \big( \forall _ {c} S(c, c) \rightarrow T(c, c) \big) \cong \big( \forall _ {f : c \rightarrow c' } S(c', c) \rightarrow T(c, c') \big)

を利用する。詳しくは、morphism族:

  • \big( \tau _ c : S(c, c) \rightarrow T(c, c) \big) _ c

について、

  • \phi_{f : c \rightarrow c'} = T(1 _ c, f) \circ \tau _ c \circ S(f, 1 _ c) : S(c', c) \rightarrow T(c, c')

とすると、これはfreely natural*1。よって、

  • (\phi _ {1 _c} = \tau _ c) _ c

は、dinatural。

参考文献

*1:本当に右側の形式がfreely naturalなのかは別問題･･･