First-order Categorical Logic with quantifiers that respects duality?

[rockbr...@gmail.com]

All the approaches I've examined appear to want to codify BOUNDED
quantifiers rather than the quantifiers you see in first-order logic.
The problem with doing that is that since you're already making the
inference A |- B into a category-theoretic arrow A -> B; then the
minute you bound quantifiers you've just fed the object and morphisms
back into the term language! This, of course, leads eventually to a
formalism for "dependent types" and/or "number" or "set" objects and
suddenly you find yourself in the land of toposes and the like;
essentially trying to remake ALL the foundations of set theory and
arithemetic over into categorical form.

In addition, the approach is skewed one way only: only looking at
elements a: A of a type A which is linked to the notion of arrows of
the form p: 1 -> A; while ignoring the dual concept.

Curry's treatment of predicate logic seems to be the only comprehensive
formal approach that avoids the higher-order issue by keeping the
terms, propositions and judgements separate. But I'm not clear what
should count as a term then.

More generally, I want an approach that treats both directions of the
arrow equally.

If you have an assertional logic (where an assertion "|- A" is treated
as an arrow "1 -> A" for a terminal object 1) then there should be a
dual present for the [counter-factual] "query" B |- treating it as an
arrow "B -> 0" to the initial object 0.

Likewise if there is an "internal language" that expresses elements "a:
A" of assertions A equivalently as arrows "p = &a: 1 -> A" with inverse
a = *p and functions represented as f(a) = *(f o &a): B for f: A -> B
and a: A -- where o denotes composition -- then there should also be a
"co-language" with co-elements "b: B?" of queries B equivalently as
arrows "q = b*: B -> 0" with inverse b = q& then there should be an
internal "co-language" with "co-functions" {b}f = (b* o f)&: A? for f:
A -> B and b: B? that pulls back queries.

Corresponding to the internal lambda abstraction (lambda x)a_x: A x C
-> B for x: 1 -> C and a_x: A -> B where A x C denotes the product;
should be an internal "co-lambda" abstraction (gamma y)a_y: A -> D + B
for y: D -> 0 and a_y: A -> B where D + B denotes the co-product.

So even if you go the usual route with dependent types and/or bounded
quantifiers there should be a dual notation that binds with co-elements
rather than with elements.