Doctrinal Semantics of Directed First-Order Logic

Andrea Laretto, Fosco Loregian, Niccolò Veltri

We present a first-order logic equipped with an "asymmetric" directed notion of equality, which can be thought of as rewrites between terms, allowing for types to be interpreted as…