[Agda] Stymied by a proof irrelevance requirement

[Guillaume Brunerie]

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.

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

Guillaume