Title:A Strongly Normalizing Computation Rule for Univalence in Higher-Order Minimal Logic

Abstract:Homotopy type theory offers the promise of a formal system for the univalent foundations of mathematics. However, if we simply add the univalence axiom to type theory, then we lose the property of canonicity --- that every term computes to a normal form. A computation becomes `stuck' when it reaches the point that it needs to evaluate a proof term that is an application of the univalence axiom. So we wish to find a way to compute with the univalence axiom.
As a first step, we present here a system of higher-order propositional logic, with a universe Omega of propositions closed under implication and quantification over any simple type over Omega. We add a type M =A N for any terms M, N of type A, and two ways to prove an equality: reflexivity, and the univalence axiom. We present reduction relations for this system, and prove the reduction confluent and strongly normalizing on the well-typed terms.