You can now watch my thesis defense on computational reflection in intensional type theory. Some minor hicups during the talk but otherwise gives a very high-level overview of MirrorCore and Rtac at the time (2014).