{{language|Agda2}}{{implementation|Agda2}}{{stub}}