Categorical semantics for counterpart-based temporal logics

This repository contains the Agda presentation of the categorical semantics for a quantified linear temporal logic QLTL based on counterpart semantics in the sense of Lewis.

We use the agda-categories library as a practical foundation to construct the models of our logic by means of relational presheaves.

Positive normal form

Some results on a positive normal form of this logic in the case of linear trace-like models can be found at https://github.com/iwilare/qltl-pnf/.

Requirements

• agda-categories 1.7
• agda-stdlib 1.7.1
• agda 2.6.2.2