[Agda] An article by Jean-Yves Girard

[Martin Escardo]

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