nLab
Makkai duality

Idea

Makkai duality is a kind of syntax-semantics duality, due to Michael Makkai, relating pretoposes (categories having to do with the syntax of first-order logic) and ultracategories (which are a way of capturing the semantics of first-order logic). This leads to a proof of conceptual completeness for first-order logic.

References

Some more general variants are achieved in