Major update to the coq_introduction

includes .gitignore file, Makefile
creates .tex, .pdf and .html
cleaned up
extend with univalence and example