日々の流転

λ. Extensible datatypes. Andres Löh

を読んだ。

λ. Inductive Types for Free

を読んだ。

• Containerは存在自体は知っていたが、嬉しさがようやく理解できた
• strictly positive の定義は?
  • 【追記】 下の Representing Nested Inductive Types using W-types の方に書いてあった。
• LCCC = locally cartesian closed category
• Representation Theorem 面白い
• Martin-Löf category = LCCC + W-types
• 「M-types can be constructed from W-types」というのはどうやるのだろう?

λ. Representing Nested Inductive Types using W-types

• <URL:http://www.cs.nott.ac.uk/~txa/publ/icalp04.pdf>
• <URL:http://www.cs.nott.ac.uk/~txa/publ/>

∑_A: C/A → C が π_B^*: C/A → C/∑_AB の左随伴というのは何を言っている?

coproduct が disjoint であるときに、A+B ⊢ C ⟼ (A ⊦ κ^* C, B ⊢ κ'^* C) で定義されている関手 C/A+B → (C/A)×C/B がequivalenceになるのがどうしてなのか、わからない。