We provide a construction which co-freely adds elementary structure to a primary doctrine in the sense of Lawvere. We show that the construction preserves all the first order logical structures that the starting doctrine may have. Moreover it forces the Principle of Propositional Extensionality when applied to triposes.
A Co-free Construction for Elementary Doctrines / F. Pasquali. - In: APPLIED CATEGORICAL STRUCTURES. - ISSN 0927-2852. - 23:1(2015 Feb), pp. 29-41. [10.1007/s10485-013-9358-z]
A Co-free Construction for Elementary Doctrines
F. Pasquali
2015
Abstract
We provide a construction which co-freely adds elementary structure to a primary doctrine in the sense of Lawvere. We show that the construction preserves all the first order logical structures that the starting doctrine may have. Moreover it forces the Principle of Propositional Extensionality when applied to triposes.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
s10485-013-9358-z.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Licenza:
Nessuna licenza
Dimensione
289.3 kB
Formato
Adobe PDF
|
289.3 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
