In HoTT we can define types with additional equality, for example the circle skeleton and the type of unordered pairs:
Family CircleSkeleton GenericPoint (CircleSkeleton) Loop (GenericPoint = GenericPoint)
Family Couple (Type ⇒ Type) Couple (T (Type), a (T), b (T) ⇒ Couple[T]) Mirror (T (Type), a (T), b (T) ⇒ [Couple[T, a, b] = Couple[T, b, a]])
HoTT types form (∞,0)-categories, but we probably could allow nonreflexive arrows on the first H-Level to represent incomplete (or nonterminating) computations. Let's define a type of Natural numbers together with possibly incomplete addition:
Family Nat (Type) Zero (Nat) Succ (Nat ⇒ Nat)
Directed-Family Nat-Plus-Addition extending Nat Add (Nat, Nat ⇒ Nat-Plus-Addition) ZeroReduction (x (Nat) ⇒ [Add [Zero, x] = x]) SuccReduction (a (Nat), b (Nat) ⇒ [Add[Succ[a], b] = Succ[Add[a, b]]])
Nat-Plus-Addition is now the type of expressions involving natural numbers and addition, and we can, step-by-step, by applying reductions, convert it to a Nat, preserving equality. ZeroReduction and SuccReduction are the computation rules in sense of Interaction Nets. Assuming univalence, ‖Nat-Plus-Addition‖ = Nat means precisely that Nat-Plus-Addition can always be reduced to Nat.
How can we prove that some ‖Type-Plus-Computation‖ = Type?
We certainly can do it only relatively to some wellfoundness postulate. Optimally, we have to represent ordinals α as universal interaction nets Cα of complexity up to α, than map interaction net Type-Plus-Computation in question onto Cα in such a way that elements of type Type are mapped onto Zero. The postulate that o is wellfounded should then have the form Cα = Unit we should be able to conclude that Type-Plus-Computation = Type.
Probably, we could use Takeuti Diagrams (encoded as Directed-Families) as universal interaction nets of corresponding complexities.