This is for an attempt to formalize in Agda a simple higher-dimensional type theory in the form seen in http://www.cs.bham.ac.uk/~mhe/TT-perhaps-eating-itself/TT-perhaps-eating-itself.html, starting with the 2TT theory of Licata & Harper since it's a simplified type theory that already uses explicit substitutions.