  Fitch-style modal deduction, in which modalities are eliminated by opening a
subordinate proof, and introduced by shutting one, were investigated in the
1990s as a basis for lambda calculi. We show that such calculi have good
computational properties for a variety of intuitionistic modal logics.
Semantics are given in cartesian closed categories equipped with an adjunction
of endofunctors, with the necessity modality interpreted by the right adjoint.
Where this functor is an idempotent comonad, a coherence result on the
semantics allows us to present a calculus for intuitionistic S4 that is simpler
than others in the literature. We show the calculi can be extended \`{a} la
tense logic with the left adjoint of necessity, and are then complete for the
categorical semantics.
