ニョロニョロのメタリーズニング

絵図形式

左に a を入れるの省略。

 　f    f
 η|    |
 ∩|    |
 ||| ≡ |
 |∪    |
 |ε    |
 f      f

自然演繹形式

(1)から(6)の番号は絵との対応を取るためのもの。

snake::: (a.η*f);(a.f*ε) ≡> a.f^

{(a.η*f);(a.f*ε) :: True ⇒ a.f≦a.f

                 True
   ==================================[dup True]
    True                         True
 ===========[unit]           ===========[counit]
     A^                          g*f
 (1)----[η]                 (4)-----[ε]
    f*g                          B^
 =============[a.]           =================[f*]
     a.A^                       f*(g*f)
 (2)--------[a.η]           (5)-------[f*ε]
    a.(f*g)                     f*B^
 ======================[*f]  =====================[a.]
     (a.A^)*f                   a.(f*(g*f))
 (3)-------------[(a.η)*f]  (6)-----------[a.(f*ε)]
    (a.(f*g))*f                 a.(f*B^)
 =====================[calc] =====================[calc]
     a.f                        a.(f*g*f)
   -----------[a.η*f]        -----------[a.f*ε]
    a.(f*g*f)                     a.f
 ==================================================[; a.(f*g*f)]
          a.f
        ---------[(a.η*f);(a.f*ε)]
          a.f
}
≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡[snake]
{a.f^:: True ⇒ a.f≦f

       True
     =======[id f]
         f
       ----[f^]
         f
     =========[a.]
       a.f
      ------[a.f^]
       a.f
}

不等号形式

snake::: (a.η*f);(a.f*ε) ≡> a.f^

{(a.η*f);(a.f*ε) :: True ⇒ a.f≦a.f

                           True
   ==================================================[dup True]
    True                                    True
 ================[unit]                 ==================[counit]
 (1)A^≦f*g by η                       (4)g*f≦ B^ by ε
 =============[a.]                      ========================[f*]
 (2)a.A^≦a.(f*g) by a.η               (5)f*(g*f)≦f*B^ by f*ε
 ========================[*f]           =================================[a.]
 (3)(a.A^)*f≦(a.(f*g))*f by (a.η)*f    (6)a.(f*(g*f))≦a.(f*B^) by a.(f*ε)
 =====================================  ====================================
   a.f≦a.(f*g*f) by a.η*f              a.(f*g*f)≦a.f  by  a.f*ε
 =================================================================[; a.(f*g*f)]
          a.f≦a.f by (a.η*f);(a.f*ε)
}
≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡[snake]
{a.f^:: True ⇒ a.f≦a.f

       True
     =============[id f]
      f≦f by f^
     ==================[a.]
     a.f≦a.f by a.f^
}

シーケント形式

snake::: (a.η*f);(a.f*ε) ≡> a.f^

{(a.η*f);(a.f*ε) :: True ⇒ a.f→a.f

                           True
   ==================================================[dup True]
    True                                    True
 ================[unit]                 ==================[counit]
 (1)A^→f*g by η                       (4)g*f→B^ by ε
 =============[a.]                      ========================[f*]
 (2)a.A^→a.(f*g) by a.η               (5)f*(g*f)→f*B^ by f*ε
 ========================[*f]           =================================[a.]
 (3)(a.A^)*f→(a.(f*g))*f by (a.η)*f    (6)a.(f*(g*f))→a.(f*B^) by a.(f*ε)
 =====================================  ====================================
   a.f→a.(f*g*f) by a.η*f              a.(f*g*f)→a.f  by  a.f*ε
 =================================================================[; a.(f*g*f)]
          a.f→a.f by (a.η*f);(a.f*ε)
}
≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡≡[snake]
{a.f^:: True ⇒ a.f→a.f

       True
     =============[id f]
      f→f by f^
     ==================[a.]
     a.f→a.f by a.f^
}