[Agda] Stymied by a proof irrelevance requirement
Conor McBride
conor at strictlypositive.org
Fri Apr 5 14:18:18 CEST 2013
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
More information about the Agda
mailing list