• Agda
• categorical logic
• category theory
• counterpart semantics
• dependent types
• formalization
• temporal logics

The aim of this thesis is to provide a complete presentation of the semantics of first-order temporal logics based on the counterpart paradigm: we start by introducing a standard set-based semantics and then we define a categorical semantics based on relational presheaves. The constructions are formalized using the dependently typed programming language and proof assistant Agda, and we employ the agda-categories library to adequately capture the notions of category theory required in our setting.