[Agda] Stymied by a proof irrelevance requirement

[Andreas Abel]

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.

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/