[Agda] Stymied by a proof irrelevance requirement

Guillaume Brunerie guillaume.brunerie at gmail.com
Fri Apr 5 00:52:31 CEST 2013

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.


More information about the Agda mailing list