Tutorial about syntax of HoTT variant of Coq

Question

I'd like to learn the Homotopy Type Theory (HoTT) variant of Coq. I am browsing the web site http://homotopytypetheory.org/, I have installed the variant of Coq, and I would like to play a little bit with it, write down the examples of the book, etc... But I cannot find a pdf/html file explaining the basic syntax. When I try in hoqide (the HoTT variant of coqide) the piece of code

Require Import HoTT.
Inductive circle:Type1 := | ZERO : circle | loop : ZERO = ZERO.

I get the error "Error: The reference ZERO was not found in the current environment." I guess that I don't load enough libraries, or maybe that ZERO = ZERO is not the correct notation for the type of paths from ZERO to itself. In the blog, the notations ZERO ~~> ZERO and Paths ZERO ZERO are also used, but they don't work here. Where can I find a tutorial to start ?

Answer 1

I don't know of any tutorials in the style you are looking for, but as far as I know HoTT doesn't really change the syntax of inductive types in Coq. Instead, they use a feature known as private inductive types in addition to axioms to define higher inductive types while maintaining consistency. For instance, see how the circle is defined in the HoTT library itself.

Answer 2

I'm not familiar with the HoTT-enabled variant of Coq, but when you define an inductive type like circle, all your constructors must actually construct elements of that type. You can't write e.g.

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 quite fast. Now, you might think that since ZERO = ZERO is a theorem, assuming that a proof of that exists is harmless, but Coq can't automatically realize that. Further, such a proof is surely not a constructor of ZERO. Probably a better alternative is to use e.g.

Variable foo3 : ZERO = ZERO .

or one of the similar commands (Axiom,Hypothesis,...).

Answer 3

There is an old branch of Bruno Barras' fork of Coq that allows syntax roughly like that. See, for example, in the example file hit-hoh.v:

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 codes higher inductive types is with the extension of private inductives. For example, in an older version of the circle file (which has since been replaced with a 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 Private Inductive keyword tells Coq to disable pattern matching outside the current module; this allows us to force users to use only elimination/induction principles defined in the given module. We then axiomatize the path constructors, axiomatize their computation rules, and define the eliminator. Note that the eliminator must make use of the path argument (l : loop # b = b) in its body, or else Coq will assume that what you pass as that argument doesn't matter.

~~~~~

Where can I find a tutorial to start ?

I am not aware of any such tutorial at present, but I might suggest looking at contrib/HoTTBook.v and contrib/HoTTBookExercises.v which contain many links between the HoTT book / exercises and the HoTT/HoTT library. Looking at how these theorems and exercises are stated and proven might be useful (and feel free to contribute your own solutions/proofs to problems/theorems that are not linked to anything yet!).