Terms in Extensional MLTT don't contain equality-reasoning information (implicit transports), effectively meaning data is lost, which is bad. But at the same time, higher-order reasoning (reasoning about reasoning) is not present, which is good.

Terms in Intensional MLTT do contain equality-reasoning information (explicit transports), effectively meaning data is not lost, which is good. But at the same time, higher-order reasoning is present, which is bad.

Example of higher-order reasoning is having a term containing transports brought inside a type and then trying to inhabit that type. One has to then tinker with the transports, possibly having to apply different properties. Higher order reasoning is meaningless w.r.t. computational interpretation of TT where all transports act like identity function. Tinkering with transports is merely done to satisfy the type checker with zero computational meaning. The behaviour is highly undesirable because it's unnatural w.r.t. the computational interpretation and contains much extra reasoning, again, not present in the interpretation. I think it's safe to say that this problem is huge in the mathematical community and highly restraints the adoption of intensional MLTT as of a practical foundation of mathematics, as, Set Theory, the conventional foundation, is not plagued with higher-order reasoning in that sense.

Example why lost data is bad: it's impossible to automate unification for Extensional TT because unification requires decidable exchange rule. But in order to implement it we have to be able to decide whether a term depends on one of the variables in the context, which is impossible in presence of equality reflection. Again the is huge because problems like that make Extensional TT unsuitable for automation on a computer.

Question is, can we have a type theory where equality-reasoning information is preserved and where reasoning is first-order (= no reasoning about reasoning)?

  • 2
    $\begingroup$ You may want to restrict "computational interpretation of TT" to MLTT, because in computational univalent type theories, transports may not be the identity. There is a path from Bool to itself such that its transport is equal to negation. $\endgroup$
    – Trebor
    Jan 28 at 8:33
  • $\begingroup$ And have you considered first order logic with equality? Sounds like it's pretty first order :) $\endgroup$
    – Trebor
    Jan 28 at 8:34
  • $\begingroup$ Yes, I meant computational interpretation of MLTT with proof-irrelevance. $\endgroup$
    – Russoul
    Jan 28 at 8:46
  • $\begingroup$ The word first(higher)-order in the context of logic designates something else. $\endgroup$
    – Russoul
    Jan 28 at 8:51
  • 1
    $\begingroup$ But seriously, higher order logic with equality seems to completely fit the bill. Since there is no (essential) dependency, no transport will ever appear in a type. $\endgroup$
    – Trebor
    Jan 28 at 8:53


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.