At the time of writing Lean 4 is almost ready for a
stable release. If you haven't heard of it, it is an easier
to install proof assistant and has more powerful automation
compared to Agda. However Lean 4 does not plan to support
Homotopy Type Theory at all (while Lean 3, the current
stable version, has limited support to HoTT) so the last
part of this book cannot be applied on Lean 4.
1. Equal, in type the time we can just sim‐
plify this since we would
The term "definitional hardly ever need the concept
equality" may be confusing. of set of all sets in pro‐
However it basically means gramming.
that the two sides of the
equality can be reduced to 3. Inductive types
the same term. Notice that
by the property of well You may think inductive
typed terms, the reducing is types are just about more
guaranteed to terminate, so complex composition of basic
in Agda definitional equal‐ types, however in the type
ity can be directly solved theory inductive types are
by the proof assistant most also the more "safe" way to
of the time. However in some extend the theory than just
more subtle variants of type make some constants. For
theory, notably NuPRL's type that reason, the positivity
theory, the reducing does check of inductive types is
not having termination pro‐ implemented in proof assis‐
perty. In that case, manual tants of type theory.
guide of term rewriting is
of most of the time neces‐ 4. Homotopy type theory
sary.
The most essential con‐
2. Universe cept of HoTT is about equal‐
ity type. In the "ordinary"
While at first glance type theory we would just
it seems that Dependent type assume all the witnesses of
theory is the result of equality types are defini‐
adding function computation tional equal, that is, they
to type level, universe is have no interesting computa‐
something added to prevent tional contents.
the paradox. However most of CONTINUE=>
However, in HoTT, one 4.3. Path traveler
cannot easily consider two
witnesses of quality types, The path operations
or path types, are equal. are, actually ways to coerce
This means axiom K, which is the type of the witness in
about the uniqueness of the type theory, if think compu‐
inhabitant of path types, is tationally. There space
disabled for HoTT mode. With interpretations are more
that in mind type theory can subtle.
be derived to a language
ideal for geometry or what‐ 5. Univalence
ever of interests of certain
mathematicians. The concept is any two
equivalent types can be
4.1. Leibniz equality proved definitional equal by
univalence axiom. Then, we
In some of the early can ignore the implementa‐
proof assistants, due to the tion detail of data types
lack of fancy unification since different representa‐
algorithms (actually Agda tions are able to be
would also try to rewrite automatically transported by
the goal with hypotheses), UA. Both operations on data
the Leibniz equality is used and proofs about them can be
in place of the definitional bridged easily.
equality before mentioned.
In section 9.1.4 a proof
that Leibniz equality is Many results of
propositional equal to univalence presented in this
definitional equality is chapter are just seems more
given. fancy concept presentation
of similar concepts already
4.2. In the space existed in NuPRL to me.
Other than that, I got the
The HoTT interpretation impression that higher
of types is types are inductive types are only
spaces, inhabitants of types interesting to geometry
are points in spaces, and related fields. Overall this
the path types are paths book is a gentle introduc‐
between two points. One can tion to logic and type
imagine path types can be theory. It seems my
concatenated. The lack of interests in type theory has
axiom K means paths can not been refreshed again.
be easily contracted to
points.
