[Agda] Stymied by a proof irrelevance requirement

[Conor McBride]

On 4 Apr 2013, at 23:52, Guillaume Brunerie wrote:

> On 2013/4/4 Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
>> On 03.04.13 5:46 PM, Dan Licata wrote:
>>> 
>>> That 'subst' at a constant function is the identity is definitely part
>>> of the computational story about homotopy type theory, but I don't have
>>> anything implementable for you yet.
>>> 
>>> On Apr02, Nils Anders Danielsson wrote:
>>>> 
>>>> On 2013-04-02 03:36, Jacques Carette wrote:
>>>>> 
>>>>> Also, might it be a good idea to "upgrade" the standard library's
>>>>> cong₂ to this dependent version?
>>>> 
>>>> 
>>>> The dependent one is often more awkward to use. The awkwardness would
>>>> disappear if one could make
>>>> 
>>>>   subst (λ _ → B) eq x
>>>> 
>>>> reduce to x. Perhaps Conor McBride or Dan Licata know how this can be
>>>> accomplished.
>> 
>> 
>> Nicolai suggested to me the reduction rule
>> 
>>  subst P (eq : a == b) (x : P a) --> x  if P a = P b definitionally
>> 
>> This would of course cover this case, but then subst needs to be a primitive
>> in Agda.  Also, it does not fit the current style of dealing with equality
>> which is matching against refl.

Doesn't Alan Jeffrey's trick with "trustMe" get you out of this jam?
Something like

remember : forall {X}{x y : X} -> .(x == y) -> x == y
remember _ = trustMe

where the computational behaviour of trustMe is such that it becomes refl
whenever the equation holds definitionally.

Of course, "trustMe" is unsafe, but "remember" is ok...

> 
> Also it’s completely wrong from the point of view of homotopy type
> theory, you can easily prove UIP using that.

...unless you actually want equality proofs to contain information.

All the best

Conor