  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.
