From High School Algebra to University Algebra

High School Algebra (HSA) is the equational theory of semirings with exponentiation satisfying the usual laws. Tarski conjectured that HSA without zero is complete for the natural numbers. This was refuted by Wilkie, who constructed a counterexample; Gurevich later showed that the theory is not even finitely axiomatizable. Di Cosmo and Fiore extended this incompleteness to the categorification of HSA—the theory of bicartesian closed categories (without an initial object).

What happens if we add dependent types? We consider the theory of categories with families (CwFs) with Π-types, Σ-types, and the types 1 and 2, which we call University Algebra (UA). We show that the Wilkie counterexample is derivable in this setting. This motivates the question: is UA, unlike HSA, complete?