Comment by ndrwnaguib

Yes; the goal is to finish the first volume. I am particularly looking forward to formalizing the well-known 1+1 proof.