  This paper introduces a natural deduction calculus for intuitionistic logic
of belief $\mathsf{IEL}^{-}$ which is easily turned into a modal
$\lambda$-calculus giving a computational semantics for deductions in
$\mathsf{IEL}^{-}$. By using that interpretation, it is also proved that
$\mathsf{IEL}^{-}$ has good proof-theoretic properties. The correspondence
between deductions and typed terms is then extended to a categorical semantics
for identity of proofs in $\mathsf{IEL}^{-}$ showing the general structure of
such a modality for belief in an intuitionistic framework.
