You can follow Getting Started - PLFA but ignore all the PLFA-specific stuff.
Agda tutorial session <2021-11-19 Fri> .
Author: Tianyu Chen
Created: 2021-11-19 Fri 13:56