This blog actually begins

It is very convenient that I have already setup a blog. The first post was not even that bad, after some editing! Or so I think. Anyway, now I will finally start posting some content. As proof I know how to use a blog, I will figure out how to use latex! \[ \DeclareMathOperator{\Set}{Set} \DeclareMathOperator{\suc}{suc} \DeclareMathOperator{\Id}{Id} \DeclareMathOperator{\refl}{refl} \DeclareMathOperator{\Cong}{cong} \DeclareMathOperator{\prf}{prf} J : \prod(A : \Set) (P : \Pi(x\ y : A) (I : \Id x\ y), \Set), \\ (\Pi(a : A), P(a,a,\refl A a)) \to (\Pi(x\ y : A)(i : \Id x\ y), P\ x\ y\ i) \] This is the glorious induction principle for equality in dependent type theory. More on this later!