Hi, all.
In some of slides and webpage on the topic `topos' as bridges. I can see a claim that the bridge technique could be implemented as an automatic tool to generating theorems. But in the given examples in the book and online, I do not see the bridges can be used without human effort. So is there any example that which sort of things should be automated? Or if we do need human's effort(which will be fine as well, just require some information provided by the user), is there any concrete description of the workflow of using the `bridges' in a theorem prover, or what should be implemented?
I have scanned some sections of the book but I should admit that I have not taken time to go through all the details. Therefore, it might be the case that some content in the book has already mentioned hint on this, but I did not see them. In this case, thanks for telling me where of any book or slides should I take more time to read.
Thank you for any attempt to help!
@yimingxu Hi Yiming Xu, thanks for your question.
For the 'automatic' computation or large classes of invariants, you may refer to the following papers, which treat respectively logically-inspired and topologically-inspired classes of invariants of toposes whose computation can be made automatic:
Topologies for intermediate logics
Site characterizations for geometric invariants of toposes
You may also look at the slides Deductive systems and Grothendieck topologies, which describe, taking my book as a reference, the proof-theoretic equivalence between between quotients theories and Grothendieck topologies, and its usefulness for the automatic computation of several natural constructions on theories.
Lastly, I should mention that, with some scientists at Huawei, we have recently begun investigating the possibility of implementing the technique of topos-theoretic 'bridges' on a computer; if any publication arises from this, I will announce it here.
@ocaramello I see there is concrete literature on the matter. Thank you! And I guess, no publication arose from the Huawei working group right?
@estebanricardo22 There are no papers available yet, but the subject is going to be developed in several directions. I shall post updates here.
