nLab
unintentional type theory

Unintentional type theory

Unintentional type theory

Idea

In contrast to intensional type theory, which is a type theory containing an identity type x=yx=y whose elements are identifications of xx and yy, unintentional type theory has a mistaken identity type x?yx \overset{?}{\approx} y whose elements are inadvertent conflations of xx and yy. The mistaken identity type

greatly increases the expressive power of UTT by internalizing many proofs which previously required metametatheoretic techniques (e.g. user error on a blackboard). (Angiuli, p1)

Definition

The formation rule for the mistaken identity type says that any two terms, there is a type of inadvertent conflations of them.

ΓM:AΓN:BΓ(M:A?N:B)type\frac{\Gamma\vdash M:A \qquad \Gamma\vdash N:B}{\Gamma \vdash (M:A \overset{?}{\approx} N:B) \,type}

Note that the terms being (potentially) conflated do not have to belong to the same type.

The introduction rule says that from any reason to conflate two terms we can obtain an inhabitant of the mistaken identity type. It is important to note that the original reason for conflation of the terms is not remembered by the proof term.

ΓM:AΓN:BΓFIXME: are these equal?Γconfl(M,N):(M:A?N:B)\frac{\Gamma\vdash M:A \qquad \Gamma\vdash N:B \qquad \Gamma\vdash\text{FIXME: are these equal?}}{\Gamma\vdash confl(M,N) :(M:A \overset{?}{\approx} N:B)}

Finally, the elimination rule says that if we have a mistaken conflation of MM and NN, we may replace MM by NN anywhere inside another term PP whose type depends on MM. The precise syntax of this rule is somewhat complicated; see (Angiuli, p2) for details.

Semantics

Computer implementations

Unintentional type theory has not yet been implemented in computer proof assistants. However, Bauer has proposed that such implementation would be very useful pedagogically. This is because UTT can formalize the way children are taught to solve algebraic equations in school, by starting out pretending that two things are equal. Using a proof assistant with UTT could therefore help ensure that students are not doing anything right.

References

  • Carlo Angiuli?, The (,1)(\infty,1)-accidentopos model of unintentional type theory. Sigbovik ‘13; April 1, 2013. PDF
category: joke

Last revised on May 23, 2013 at 03:02:31. See the history of this page for a list of all contributions to it.