[Agda] An article by Jean-Yves Girard

[mechvel at scico.botik.ru]

On 2020-04-21 22: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.
> [..]


Yes, Martin.
I apologize for transfering an opinion without understanding any in this 
toposes thing.
Long live toposes!

--
SM