The Coq mailing list

[DONNIE BRASCO <OOO1337777 AT outlook.com>]

✓ Where: Outside 2nd ItaCa Workshop @ 
https://appsource.microsoft.com/en-us/product/office/WA200003598

✓ What: Grammatical sheaf cohomology, its MODOS proof-assistant and 
WorkSchool 365 market for learning reviewers ↪ 
https://nicolasbourbaki365-demo.workschool365.com

✓ Context: The “double plus” definition of sheafification says that not-only 
the outer families-of-families are modulo the germ-equality, but-also the 
inner families are modulo the germ-equality. This outer-inner contrast is the 
hint that the “double plus” should be some inductive construction... that 
grammatical sheaf cohomology exists!
    And the MODOS proof-assistant implements the cut-elimination confluence 
of this inductive construction where the decreasing measure of 
families-gluing is the restricting covering: | Gluing : (forall (G : Site) (v 
: Site( G → V | in sieveV )), PreSheaves(Restrict F (sievesW_ v) → Sheafified 
E)) ⊢ PreSheaves(Restrict F (Sum sievesV_ over sieveU) → Sheafified E). And 
the separateness-property is expressed via the congruence-conversions 
clauses. Then the generalization to cohomology beyond 0th (sheaf) is that the 
grammatical sieves could be programmed such to inductively store the 
(possibly incompatible) data along with its gluing-differentials: Any list of 
(semantically-equal) arrows in the grammatical sieve now stores both data (on 
the singleton lists) and differentials (on the exhaustive ordered listings), 
and the (inductive) differentials of the outer-gluing of inner-gluings 
correctly-compute the differentials of the total/sum gluing because ∂∂ = 0… 
Moreover, the generating topological site has its own cut-elimination 
confluence of arrow-terms, each arrow-term is covered by its arrow-subterms, 
and the algebra-operation of composition ⟦f⟧*⟦B⟧*⟦g⟧ → ⟦f ∘_B g⟧ is indeed 
geometric, is some sheaf condition. Possible applications are the 
constructive connecting-snake lemma for additive sheaves, or the constructive 
dependent homotopy types or the constructive geometry of quantum fields in 
physics.
    This research is the fusion of prompts from two expert mathematicians: 
Kosta Dosen and Pierre Cartier. But should this research be 
immediately-conclusive and peer-reviewed only by experts in some 
publishing-market susceptible under falsifications/intoxications? And what 
sense is peer review of already-computer-verified mathematics? WorkSchool 365 
is Your Market for Learning Reviewers. WorkSchool 365 is your education 
marketplace where the prompting authors pay to get peer reviews of their 
documents from any learning reviewers who pass the test quiz inside the 
prompting document, with shareable transcripts receipts of the school work. 
WorkSchool 365 documents are Word templates with business-logic automation 
and playable Coq scripts. WorkSchool 365 is free open-source code Microsoft 
Teams app in the web browser with authentication via only no-password email. 
Enroll today! WorkSchool365.com