Proof assistants

Differences in notation

Scientists use a variety of notations for \(\Pi\)- and \(\Sigma\)-types, primarily depending on the field they are working in.

The mathematical notation for these types normally looks like

\[\prod_{x:A}B(x) \qquad \sum_{x:A}B(x)\]

Here, \(B:A\to\mathcal{U}\) is a dependent type, seen as a function, evaluated at the point \(x:A\).

In logic, one often sees

\[\prod_{x:A}B \qquad \sum_{x:A}B\]

where \(A\) and \(B\) are now seen as syntactic expressions, and in particular the expression \(B\) may use the variable \(x\) of type \(A\). Hence the “evaluation” of \(B\) at \(x\) is dropped, compared to the mathematical notation.

In Agda-style proof assistants, \(\Pi\)-types are denoted

(x : A) -> B x

and \(\Sigma\)-types as

(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 \(\Pi\)-types are denoted

forall x : A, B x

which may be somewhat confusing since the “forall-quantifier” \(\forall\) is used in HoTT solely for logical notation of propositions as in Definition 3.7.1 in the HoTT book. \(\Sigma\)-types are written as in Agda, but also as

{ 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 \(\Pi\)- and \(\Sigma\)-types, commonly making use of unicode support of the underlying language.

Finally, inductively defined types in proof assistants correspond to 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:

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:

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 HoTT Coq library.)

Agda

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

RedPRL

RedPRL is a proof assistant aims to implements Computational Higher Type Theory. It is similar in spirit to NuPRL, which is a type theory of 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.

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 library

Compared to UniMath, this library uses more features of Coq. See the paper for a description [BGL+17].

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 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.