Proof-assistants usually include a lot of machinery that assists in the creation of proofs. The creation process may be unsound without risking the soundness of the proof-assistant if the alleged proof that was created is later verified by a sound proof-verifier. The smaller this verifier is, the less likely it is to be unsound due to coding or reasoning errors. The term small kernel was coined to refer to such a verifier in Barendregt and Geuvers (the idea apparently goes back to De Bruijn).
I have found literature mentioning this concept in relation to Coq and HOL Light (among others), but not to Agda, hence the question:
Barendregt, Henk; Geuvers, Herman, Proof-assistants using dependent type systems, Robinson, Alan (ed.) et al., Handbook of automated reasoning. In 2 vols. Amsterdam: North-Holland/ Elsevier; 0-444-50812-0 (vol. 2); 0-444-50813-9 (set)). 1149-1238 (2001). ZBL1005.03011.