It shouldn't be too hard to add support for irrelevance to the current system. The question is whether we want to have support for both kinds of definitional irrelevance in Agda, or if we can get away with just implementing Prop and desugaring irrelevant arguments to it. Either way, it seems like a good idea to add support for Prop first:

• Add the Prop sort to the syntax
• Update the typing rules for universes and pi types to include the cases for Prop
• Update the typing rule for case expressions to disallow casing on Prop unless the motive is in Prop itself
• Update the conversion checker to take irrelevance into account (either making it type-directed, or adding irrelevance markers to the term syntax).