Are Irrelevant types Recomputable?

[jamesmckinna]

Issue #2493 (and related upstream ones) arose when trying to extend Relation.Nullary.Recomputable to include a proof that for any A, Recomputable (Irrelevant A) is provable, i.e.

lemma : .(Irrelevant A) → Irrelevant A

Perhaps this is trivial, but I'm not seeing it (and if it's not provable, then perhaps we need to reconsider the relationship between Data.Irrelevant and the dot modality? Never mind the recent extensions to Agda with @0 etc.)

Given the definitions (not in stdlib)

-- Relationship with the . modality: wrapped/unwrapped application

infixr -1 _$ⁱ_ _$ᵢ_

_$ⁱ_ : (.A → B) → Irrelevant A → B
f $ⁱ [ a ] = f a
{-# INLINE _$ⁱ_ #-}

_$ᵢ_ : (Irrelevant A → B) → .A → B
f $ᵢ a = f [ a ]
{-# INLINE _$ᵢ_ #-}

it's clear that Irrelevant A is somehow equivalent to .A, but unfortunately, I can't seem to find a way to prove lemma.

NB. If Irrelevant were a monad (but it's not: as the type _>>=_ : Irrelevant A → (.A → Irrelevant B) → Irrelevant B betrays, it's only a 'monad up to irrelevance'), then lemma would reduce/be equivalent to the diagonal join...

[fredrikNordvallForsberg]

I wouldn't call it trivial, since the version using the record constructor rather than a copattern doesn't work, but it's certainly short:

lemma : .(Irrelevant A) → Irrelevant A
irrelevant (lemma [ a ]) = a

[jamesmckinna]

@fredrikNordvallForsberg astonishing! Thanks very much, you've lightened my darkness today.

Mind you, these things still baffle me:

irrelevant (irrelevant-recomputable [a]) = irrelevant [a]

fails, with the dreaded warning

Projection  irrelevant  is irrelevant.
Turn on option --irrelevant-projections to use it (unsafe)
when checking that the expression irrelevant [a] has type A

so back to school for me for the interaction of copatterns with irrelevance :-(