Aufhebung in type theory

 Consider the Barendregt Cube or more specifically the system of logics studied in Jacobs book 'Categorical Logic and Type Theory' which starts with simple type theory and culminates in higher-order dependent type theory which subsumes all the rest. There is a process in which each level subsumes the previous one in particular through reflection-into-self, the prototype being the subobject classifier wherein Prop becomes a Type. The culmination of the Barendregt cube is $\lambda C$. There is a parallel with Hegel's development of Concept (Begriff). In the simple typed lambda calculus we have the classical division between subject and predicate $ t : T$, $t$ is of type $T$, $t$ is a $T$, which corresponds to the division between term and type. The development along the directions of the cube expresses the increased dependency of terms on types, types on terms (and types on types) until the distinction is all but subsumed and abolished in $\lambda C$. There is only one pure 'type' $\square$ which expressed the Concept. Jacob's book allows us to trace this in terms of fibered categories.

 We propose that we extend the Barendregt cube incorporating substructural logics via monoidal categories and generalisations of linear logic. This involves replacing the cartesian product with the monoidal product and losing weakening and contraction. Note that symmetric monoidal categories are a primary example of the internalization of the hom-sets of a category within that category.

 Consider how predicate logics are extended via propositions-as-types. The poset (or preorder) for Prop becomes a full-blown category of proof-terms. This is like the Understanding in the Hegelian dialectic that wishes to erase the past, the temporal dynamic constitutive and genetic process of a concept. The understanding says what matters is what is proven not the process of the proof (repressed history). Against this dialectical reasoning forces the proof itself to be remembered and speculative reasoning incorporates the proof-process into a concept, thus turning propositions into types and proofs into terms.