Big list of learning Lean internals
CIC page in Coq
: an annotated version of the cubicaltt sources.
CPDT (certified programming with dependent types) chapter on equality
to learn about the various reduction rules.
Data structures to verify acyclicity of a graph on updates
: A New Approach to
Incremental Cycle Detection and Related Problems
Coq Coq correct
: Paper on
formally verifying the type checker for Coq, contains information about data structures used in the kernel.