added dependent version of ap
some cleanup
pretty syntax for ap in equational reasoning
prettify some of the equantional reasoning proofs
the sym defined by induction and the inverse is the same
added the constant function
added the dependent product syntax
now does not use the level of std library.

- We are moving towards a standalone hott library.
a placeholder io library for compiling main
a basic travis infrastructure