記法：インデックス付きの同型写像

本編ネタ
  • Fam: Mono(A, B) → [A1, Nat(y^A2, B)]
  • Yon: Nat(y^A2, B) → B(A2)
  • Fam; [A1, Yon] : Mon(A, B) → [A1, B(A2)]
  • Split: [A1, B1×A2^B2] → [A1, B1]×[A1, A2^B2]
  • UnCurry: [A1, A2^B2] → [A1×B2, A2]
  • Split;([A1, B1]×UnCurry) : [A1, B1×A2^B2] → [A1, B1]×[A1×B2, A2]
  • Fam; [A1, Yon] ; Split;([A1, B1]×UnCurry) : Mono(A, B) → Lens(A, B)
  • Lens:Mono(A, B) → Lens(A, B)
  • UnLens: Lens(A, B) → Mono(A, B)