• Outline
• Motivation
• We need erasure
• Erasure in dependently typed languages
• Erasure cannot be fully automatic (Idris)
• Prop is cumbersome (Coq)
• Irrelevant types are too much (Agda)
• Other considerations
• The proposal: erasure annotations
• What they look like
• What they mean
• How it works
• Discussion
• Erasure annotations cannot (always) be inferred
• Implementation considerations
• Optional extensions