Proof assistants
================
Differences in notation
---------------------------------------------
Scientists use a variety of notations for :math:`\Pi`- and
:math:`\Sigma`-types, primarily depending on the field they are working in.
The **mathematical** notation for these types normally looks like
.. math::
\prod_{x:A}B(x) \qquad \sum_{x:A}B(x)
Here, :math:`B:A\to\mathcal{U}` is a dependent type, seen as a
function, evaluated at the point :math:`x:A`.
In **logic**, one often sees
.. math::
\prod_{x:A}B \qquad \sum_{x:A}B
where :math:`A` and :math:`B` are now seen as syntactic expressions,
and in particular the expression :math:`B` may use the variable
:math:`x` of type :math:`A`. Hence the "evaluation" of :math:`B` at
:math:`x` is dropped, compared to the mathematical notation.
In **Agda-style** proof assistants, :math:`\Pi`-types are denoted
.. code-block:: agda
(x : A) -> B x
and :math:`\Sigma`-types as
.. code-block:: agda
(x : A) * B x
The motivation behind these notations is that ``(x : A) -> B x`` is
like a visual generalization of the independent function type ``A ->
B``, and that ``(x : A) * B x`` is a visual generalization of the
independent product type ``A * B``.
In **Coq-style** proof assistants, the :math:`\Pi`-types are denoted
.. code-block:: coq
forall x : A, B x
which may be somewhat confusing since the "forall-quantifier"
:math:`\forall` is used in HoTT solely for logical notation of
propositions as in Definition 3.7.1 in the HoTT book.
:math:`\Sigma`-types are written as in Agda, but also as
.. code-block:: coq
{ x : A & B x }
which reminds of set comprehension. However, this notation is used
rarely, unless each ``B x`` is a proposition.
Many libraries define their own notation for :math:`\Pi`- and
:math:`\Sigma`-types, commonly making use of unicode support of the
underlying language.
Finally, inductively defined types in proof assistants correspond to
:ref:`w_types`.
.. todo::
is the last thing true? up to homotopy, maybe. computational
behavior is not specified the same way.
Coq
---
.. todo:: say something about ``Prop`` and ``Set`` and ``Type``
Coq consists of several layers of programming languages. The most
famous one is the tactic language that is used to prove theorems. But
since theorems are interpreted by types, and proofs by elements of
those types, really tactics just construct terms. For example:
.. code-block:: coq
Definition decidablepaths_equiv
(A : Type) {B : Type} (f : A -> B) `{IsEquiv A B f}
: DecidablePaths A -> DecidablePaths B.
Proof.
intros d x y.
destruct (d (f^-1 x) (f^-1 y)) as [e|ne].
- apply inl. exact ((eisretr f x)^ @ ap f e @ eisretr f y).
- apply inr; intros p. apply ne, ap, p.
Defined.
results in the term:
.. code-block:: coq
decidablepaths_equiv =
fun (A B : Type) (f : A -> B) (H : IsEquiv f) (d : DecidablePaths A) (x y : B) =>
let d0 := d (_^-1 x) (_^-1 y) in
match d0 with
| inl e => inl (((eisretr _ x)^ @ ap f e) @ eisretr _ y)
| inr ne => inr (fun p : x = y => ne (ap f^-1 p))
end
With some imagination, it can be seen that this is just a
type-theoretical expression: ``fun`` indicates a lambda expression,
``match`` is a case analysis, ``@`` is path concatenation, ``^`` is
path inversion, ``^-1`` takes the inverse of an equivalence, ``_`` is
an automatically inferred term.
(The above is an example from the :ref:`hott_coq`.)
Agda
----
.. _proof_assistant_cubical:
cubicaltt
---------
.. todo::
- interval is abstract (as opposed to, say, an interval of reals):
cubical set (though necessarily *not* Kan, see semantics section)
- earlier iteration: cubical
.. _smlredprl:
`RedPRL `_
------------------------------------------------------
RedPRL is a proof assistant aims to implements :ref:`chtt`. It is
similar in spirit to NuPRL, which is a type theory of :ref:`sets
`, except that RedPRL provides a type theory of higher types.
Terms can be specified not just by the Martin-löf terms, but by
arbitrary programs.
.. _proof_assistants_libraries:
Libraries
---------
UniMath
^^^^^^^
In February 2010, Vladimir Voevodsky started writing the *Foundations*
library to make precise his ideas collected in *A very short note on
the homotopy λ-calculus*. Other libraries were
subsequently built on top of this. UniMath was founded in spring
2014, by combining some libraries.
See also Benedikt Ahrens' `UniMath: its origins, present, and future
`_.
The code can be found on the `UniMath github `_.
.. _hott_coq:
HoTT Coq library
^^^^^^^^^^^^^^^^^^^^
Compared to UniMath, this library uses more features of Coq. See the
paper for a description :cite:`bauer:hott:library`.
The code can be found on the `HoTT github `_.
HoTT agda library
^^^^^^^^^^^^^^^^^^^^
The code can be found on the `HoTT-Agda github `_.
cubicaltt
^^^^^^^^^^^^^
The cubicaltt compiler, that implements :ref:`cubical_type_theory`,
ships with code implementing various parts of HoTT.
The code can be found on the `cubicaltt github
`_.
Lean
^^^^
The Lean proof assistant includes HoTT libraries (work of Floris van
Doorn et al.).
Lean 2 supports hott and has a (rather large) hott library, if you
include the spectral libray.
Lean 3 doesn't support hott directly, because of changes to the
kernel, but nonetheless there is an experimental library for this.
Other libraries
^^^^^^^^^^^^^^^
- The `cubical agda library by Dan Licata et
al. `_, which aims to
optimize some homotopical proofs in a type theory in which the
higher constructors of HITs satisfy a *typal* computation rule,
rather than a judgmental one.
- Various scientists have a personal library for doing HoTT.