This is a two part talk presenting Laver's proof that the algebra generated by a rank-to-rank elementary embedding, equipped with the operation of application, is a free left self distributive algebra.