Tutorial on HoTT Coq Variant Syntax
I would like to explore a variant of Homotopy Type Theory (HoTT) Coq. I am browsing the website http://homotopytypetheory.org/ , I have installed the Coq variant and I would like to play around with it a bit, write from example books, etc. But I cannot find a pdf / html file explaining the basic syntax. When I try to use hoqide (HoTT coqide variant) the code snippet
Require Import HoTT.
Inductive circle:Type1 := | ZERO : circle | loop : ZERO = ZERO.
I get the error "Error: Reference ZERO not found in the current environment". I am assuming that I am not loading enough libraries, or perhaps that is ZERO = ZERO
not the correct note for the type of paths from ZERO to myself. The blog also uses ZERO ~~> ZERO
and notations Paths ZERO ZERO
, but they don't work here. Where can I find a tutorial to get started?
source to share
I don't know of any tutorials for the style you're looking for, but as far as I know, HoTT doesn't change the syntax of inductive types in Coq. Instead, they use a function known as private inductive types, in addition to axioms, to define higher inductive types while maintaining consistency. For example, see how the circle is defined in the HoTT library itself.
source to share
I'm not familiar with the HoTT-enabled CoQ variant, but when you define an inductive type for a type circle
, all of your constructors should actually create elements of that type. You cannot write for example.
Inductive mytype : Type :=
| foo1 : mytype (* ok *)
| foo2 : nat -> mytype (* ok *)
| foo3 : nat -> False (* urk! Not ok. *)
| foo3 : nat -> 0 = 1 (* urk! Not ok. *)
.
otherwise, the logic would become inconsistent pretty quickly. Now you might think that because it ZERO = ZERO
is a theorem, assuming that the proof that it exists is harmless, but Coq cannot automatically implement it. Moreover, such a proof is certainly not a constructor ZERO
. Probably a better alternative is to use for example
Variable foo3 : ZERO = ZERO .
or one of the similar commands ( Axiom,Hypothesis,...
).
source to share
There is a Bruno Barras branch of Coq that allows a syntax like this. See for example an example hit-hoh.v file :
Inductive circle : U :=
base
// loop : base=base.
Alas, this version of Coq has not been updated since late 2015 and there is no such native support in the current version of Coq.
The way the HoTT library encodes higher inductive types is related to the expansion of private inductive devices. For example, in the old version of the circle file (which has since been replaced by the definition via coequaliziers), we can see:
Module Export Circle.
Private Inductive S1 : Type1 :=
| base : S1.
Axiom loop : base = base.
Definition S1_ind (P : S1 -> Type) (b : P base) (l : loop # b = b)
: forall (x:S1), P x
:= fun x => match x with base => fun _ => b end l.
Axiom S1_ind_beta_loop
: forall (P : S1 -> Type) (b : P base) (l : loop # b = b),
apD (S1_ind P b l) loop = l.
End Circle.
The keyword Private Inductive
tells Coq to turn off pattern matching outside of the current module; this allows us to force users to only use the exclusion / induction principles defined in this module. We then axiomatize the path constructors, axiomize their computation rules, and define a rectifier. Note that the rectifier must use the path ( l: loop # b = b
) argument in its body, otherwise Coq will assume that what you pass as this argument is irrelevant.
~~~~~
Where can I find a tutorial to get started?
I am not currently aware of such a tutorial, but I might suggest looking at and which contain many links between the HoTT book / exercises and the HoTT / HoTT library. A glance at how these theorems and exercises are formulated and proven can be helpful (and feel free to contribute your own solutions / proofs to problems / theorems that aren't related to anything yet!). contrib/HoTTBook.v
contrib/HoTTBookExercises.v
source to share