Dependently typed programming in Agda