[Agda] An article by Jean-Yves Girard

[Neel Krishnaswami]

Hello,

Girard's work in this space is very interesting.

 From the point of view of proof theory, there are at least two sensible 
equality
predicates -- the identity type of MLTT, and the 
Girard/Schroeder-Heister equality.
It is the latter formulation which gives rise most naturally to pattern 
matching, and
explains why the Coquand/McBride approach to dependent pattern matching
seemed to require UIP/Axiom K -- it tried to use the G/SH elimination 
rule with
the identity type, and since the two equalities are (ironically enough) 
different
the fit was not perfect.

However, while the G/SH equality is well-behaved from a proof theoretic 
basis,
its semantics have never been well-understood, and Girard and his 
collaborators
have discovered a bafflingly wide array of fascinating connections 
(cut-elimination in linear logic, to unification, and even to complexity 
theory). I
don't remotely pretend to understand it all, but it is all

On 21/04/2020 20:13, Martin Escardo wrote:
>
>
> On 21/04/2020 14:24, mechvel at scico.botik.ru wrote:
>> On 2020-04-21 15:54, Xuanrui Qi wrote:
>>>> The result was that simple notions
>>>> and proofs were reformulated in a complex way, and the proofs have
>>>> become many times larger and many times more complex.
>>>
>>> I'm afraid many people on this list would not agree with this
>>> statement. From what little I know about topos theory, many proofs can
>>> be greatly simplified using topos theory. Ingo Blechschmidt, for
>>> example, used topos theory to simplify many proofs in algebraic
>>> geometry [1]. Ingo himself might be on this list, so I won't say too
>>> much about his work. But this is a divergence.
>>
>>
>> I just transfer the opinion of a certain expert in logic who is aware 
>> of the topos
>> approach. He referred this way to a certain dissertation. This was in 
>> about 1995.
>
> One should avoid giving opinions about things one doesn't understand. 
> In particular, one should avoid transferring opinions.
>
> Toposes are very nice and elegant and useful and precisely explained 
> in the literature, so that if you want to understand them, you can. I 
> have used them and I will continue to do so.
>
> I am not sure about mustard watches, but then I am not an expert and 
> hence I refrain from giving an opinion. However, I do agree that the 
> abstract and the introduction of the given article in this thread 
> don't give enlightening explanations. And this is part of the reason I 
> am not an expert on this subject - whenever I try to have a go at it, 
> I don't get anywhere by reading the published work - perhaps you need 
> to be initiated in person to be able to grasp it - or perhaps I just 
> didn't get it and it is my fault, which I don't discard as a possibility.
>
> Best,
> Martin
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda