Categorical Framework for Typed Extensional and Intensional Models in Formal Semantics

Intensional computation derives concrete outputs from abstract function definitions; extensional computation defines functions through explicit input-output pairs. In formal semantics: intensional computation interprets expressions as context-dependent functions; extensional computation evaluates expressions based on their denotations in an otherwise fixed context. This paper reformulates typed extensional and intensional models of formal semantics within a category-theoretic framework and demonstrates their natural representation therein. We construct $\textbf{ModInt}$, the category of intensional models, building on the categories $\textbf{Set}$ of sets, $\textbf{Rel}$ of relations, and $\textbf{Kr}$ and $\textbf{Kr}_\textbf{b}$ of Kripke frames with monotone maps and bounded morphisms, respectively. We prove that trivial intensional models are equivalent to extensional models, providing a unified categorical representation of intensionality and extensionality in formal semantics. This approach reinterprets the relationship between intensions and extensions in a categorical framework and offers a modular, order-independent method for processing intensions and recovering extensions; contextualizing the relationship between content and reference in category-theoretic terms. We discuss implications for natural language semantics and propose future directions for contextual integration and exploring $\textbf{ModInt}$'s algebraic properties.