Added Chlipala's PHOAS paper, Altenkirch/Reus paper on a representation of lambda terms being monadic, Shulman/Lumsdaine note on semantics of HITs.