About Opposition and Duality in Paraconsistent Type Theory

Juan C. Agudelo-Agudelo
(Universidad de Antioquia)
Andrés Sicard-Ramírez
(Universidad EAFIT)

A paraconsistent type theory (an extension of a fragment of intuitionistic type theory by adding opposite types) is here extended by adding co-function types. It is shown that, in the extended paraconsistent type system, the opposite type constructor can be viewed as an involution operation that transforms each type into its dual type. Moreover, intuitive interpretations of opposite and co-function types under different interpretations of types are discussed.

In Mauricio Ayala-Rincon and Eduardo Bonelli: Proceedings 16th Logical and Semantic Frameworks with Applications (LSFA 2021), Buenos Aires, Argentina (Online), 23rd - 24th July, 2021, Electronic Proceedings in Theoretical Computer Science 357, pp. 25–37.
Published: 8th April 2022.

ArXived at: https://dx.doi.org/10.4204/EPTCS.357.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org