So, this is where I'm at so far:
- Heyting algebras model propositional intuitionistic logic (IL)
- so do Cartesian closed categories which also model the simply typed lamda calculus
- co-Heyting algebras model propositional co-intuitionistic logic (co-IL) and ??
- Locally Cartesian closed categories model dependent type theory (TT)
- Locally (and not) co-Cartesion co-closed categories model ?what exactly?
I became interested in co-Heyting algebras because of mereology for linguistics but then I learned that they model co-IL. I found a proof theory using a single-assumption multiple-conclusion natural deduction that works well as a refutation calculus dual to IL. This led me to a few questions which I can't find much research on (and I don't know much category theory.)
- Are there any term assignments for co-IL? What exactly would be "the construction c [that] refutes A −< B iff c [which]is a general method of construction such that applied to a hypothetical construction a that refutes A, c(a) refutes B"?
- Can one generalize to first-order quantifiers and if so, what do they look like? Would it be the coproduct that takes on some more computational meaning rather than how product does in TT?