Abstract

The simple connection of completeness and cocompleteness of lattices grows in categories into the Adjoint Functor Theorem. The connection of completeness and cocompleteness of Boolean algebras — even simpler — is similarly related to Paré's Theorem for toposes. We explain these relations, and then study the fibrational versions of both these theorems — for small complete categories. They can be interpreted as definability results in logic with proofs-as-constructions, and transferred to type theory