The Coq mailing list

[CHRISTOPHER MARY <OOO1337777 AT outlook.com>]

... indeed as I promised
Appendix: What is the minimal example of sheaf cohomology? Grammatically
Short: Hold any Dosen-style cut-elimination confluence of arrow-terms (for 
some comonad, or pairing-product, or 2-category, or proof-net star-autonomous 
category,... ), and form the (petit) grammatical-globular site (double 
category) whose objects are the arrow-terms and where any (necessarily 
finite) covering family of morphisms is either any reduction-conversion 
linkage or all the (immediate proper, including unit-arrows in cuts) subterms 
of some redex arrow-term. Define any model (in Set) to be some grammatical 
sheaf (hence globular copresheaf) of (span of) sets over this site, where 
each covering family become limit cone (constructively, using compatible 
families). Now starting with some generative presheaf data, then 
sheafification-restricted-below-any-sieve of this presheaf can be inductively 
constructed by refinements of the sieves. Moreover, it may be assumed some 
generating cocontinuous adjunction of sites; the result is some 
dependent-constructive-computational-logic of geometric dataobjects 
(including homotopy-types): MODOS. Now globular homology of any copresheaf 
computes the composable occurrences of arrow-terms (cycles from 0 to 1). Also 
grammatical cohomology of the sheafification (graded by the nerve of its 
sieve argument) computes the global solutions of occurrences of all 
arrow-terms in the model which satisfy the confluence of reductions in the 
site. Contrast to the covariant sketch models of some coherent theory; but 
now any globular-covariant (contravariant finite-limit sketch) concrete model 
is some category with operations on arrows. The sense mimicks the usual 
Kripke-Joyal sense, as explicit definitions. The generic model 
contravariantly sends any object G to the covariant diagram of sets 
represented by the sheafified G over only the finitely-presentable (data) 
sheaf-models: G ↦ Hom(sheafified(Hom(–, G)), fpModelsSet(_)) … and further 
could be sliced over any (outer/fixed) dataobject.

(1.) Morphisms: the shape of the point is now “A” instead of singleton, 
context extension is polymorph…
for (B over Delta) and for variable (Theta), then
Span(Theta ~> (Delta;B))  :<=>  Hom( (x: Gamma; a: A( h(x) )) ~> B( f(x) ) ) 
with some (f: Gamma -> Delta) and (h: Gamma -> Theta) and (A over Theta)

ERRATA: (2.) Algebraic-geometric dataobjects: the elimination schema for the 
dataobjects gives the base of the construction for the sheafification; 
continued with the refinements/gluing schema below any sieve...

| Constructing : asConstructor F U f
______________________________________
Hom( Restrict U VV ~> Restrict F VV ))

| Destructing : (forall U (f : F U) (cons_f : asConstructor F U f), 
                        Hom( Restrict U VV ~> E ))
___________________________________________________________________
Hom( Restrict F VV ~> Sheafified E VV )

| Refining : (forall W (v : Site( W ~> V | in sieve VV )), 
                        Hom( Restrict F WW_v ~> Sheafified E WW_v ))
____________________________________________________________________
Hom( Restrict F WW_VV ~> Sheafified E WW_VV )

Lemma: cut-elimination holds. Corollary: grammatical sheaf cohomology exists.

Applications: with 2-category sites, get some constructive homotopy types; 
with proof-net star-autonomous categories sites, get some constructive 
alternative to Urs Schreiber's geometry of quantum-fields physics.

https://nicolasbourbaki365-demo.workschool365.com
( https://github.com/1337777/cartier/blob/master/cartierSolution0.v )

-----

        La République de Christopher

<bourbaki> alors, as tu résolu la faim dans le monde avec ton machin là?
<chris.> donc l'étalon pour moi c'est de résoudre la faim dans le monde? je 
ne peux pas aussi faire des «mathématiques de maintenance» médiocres comme 
tout le monde?
<bourbaki> non
<chris.> et c'est sans appel? le tribunal ne pouvant directement réviser une 
juridiction académique, je vais donc contourner et demander au tribunal le 
statut moi-même de décideur académique
<bourbaki> mais c'est ridicule
<chris.> exactement! ridicule par rapport à qui, à quoi, à quel 
retranscriptions et reçus de faits? il faudra bien un compte rendu et 
réexamen public pour comparer à quel point cela est ridicule... ou pas
<bourbaki> beaucoup de gens n'y voient aucun problème
<chris.> ce n'est pas beaucoup d'individus. c'est une interdépendance 
synchronisée qui s'auto-signent des chèques en blanc débiteurs du trésor 
public, basés sur des devises monétaires falsifiées et intoxiquées; où toute 
tentative de marketing et vente directe au grand public est considérée comme 
"arrogance" ou "spam". comme-ci j'avais osé compter des morphismes au lieu de 
compter des bananes; ils m'ont pris pour le petit Kirikou ou quoi. ah, voilà! 
le fameux «ils», mais je ne nommerai pas des «communautés qu'on ne peut pas 
nommer» ...
<bourbaki> je ne savais pas que t’étais un Soralien
<chris.> mon combat ou action directe, si je puis me permettre ces 
expressions, ne s'arrête pas là. au péril d'être classé fiche S par les 
Services, j'irais même jusqu'à dire que dans l'absolu, un braqueur de banque 
est plus respectable. lui au moins il est «cash». pas d'embrouilles et 
diarrhées mentales pour inverser la réalité
<bourbaki> qu'est ce qui est réel? le statu quo crée une réalité. tu n'as pas 
dû lire la Caverne de Platon... vas-y abrège
<chris.> ReadMyReply.com