About Opposition and Duality in Paraconsistent Type Theory

TL;DR

This paper extends paraconsistent type theory with co-function types, demonstrating that the opposite type constructor acts as an involution transforming types into their duals, and explores their interpretations.

Contribution

It introduces co-function types into paraconsistent type theory and shows the opposite type constructor functions as an involution, providing new insights into duality in type systems.

Findings

Opposite types act as involutions transforming types into duals.

Extended type system includes co-function types.

Interpretations vary under different type interpretations.

Abstract

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.