Welcome to the JsCoq/JsHoTT Interactive Online System!

Welcome to the JsCoq technology demo! This page requires Chrome >= 48 or Firefox >= 45.


Alt-Enter (Cmd should work in Macs too) goes to the current point; Alt-N/P or Alt-Down/Up will move through the proof; F8 or the power icon toogles the goal panel.

Setting up the environment:

We will first load the HoTT libraries and do a proof from the library.

Theorems about the circle [S1].

Definition of the circle:

We define the circle as the coequalizer of two copies of the identity map of [Unit]. This is easily equivalent to the naive definition:

Private Inductive S1 : Type1 :=
| base : S1
| loop : base = base.

but it allows us to apply the flattening lemma directly rather than having to pass across that equivalence.

But we want to allow the user to forget that we've defined the circle in that way.

The non-dependent eliminator

The loop space of the circle is the Integers.

We use encode-decode.


Once the basic enviroment has been setup, we can write, share, and run Coq programs and proofs.

JsCoq's homepage is at github https://github.com/ejgallego/jscoq ¡Salut!