[Agda] Irrelevance and equalities?

[Dan Doel]

On Thursday 31 March 2011 4:38:55 AM Nils Anders Danielsson wrote:
> On 2011-03-31 09:06, Nicolas Pouillard wrote:
> > record Irr {a} (A : Set a) : Set a where
> > 
> >    constructor irr
> >    field
> >    
> >      .cert : A
> 
> What would happen if we replaced the irrelevance machinery with a single
> type like Irr? (I think such a type is more commonly called a "squash"
> or "bracket" type.) Would we lose anything?

Doing that probably wouldn't lose anything, in theory, over the current 
implementation.

However, if there are plans to ever actually support types like:

  .(x : A) -> B x

then squash types are at best a klunky solution.

  reverse : .(A : Set) -> .(n : Nat) -> Vec A n -> Vec A n

versus

  reverse : (SA : Irr Set) -> (Sn : Irr Nat) -> Vec (cert SA) (cert Sn)
          -> Vec (cert SA) (cert Sn)

And at worst, they're simply inadequate. The work on erasure pure type systems 
suggests that .(x : A) -> B x cannot be replicated with the squash type, but I 
don't thik they were considering the existence of things like irrelevant 
projections.

-- Dan