The Coq mailing list

[admin <admin AT AnthropLOGIC.onmicrosoft.com>]

Dear director Kumar Murty of the Fields Institute,

On day 30th of June 2022 at the Max Planck-Fields twinned conference in 
homotopy, your delegate Shane Liu哥 has failed the Fields Institute's mission 
that « a place where mathematicians from Canada and abroad, from academia, 
business, industry and financial institutions, can come together to carry out 
research », has failed by using the emergency enforcers (police constables) 
to force the denial of my access to the Fields Institute's stated mission, 
despite that there was no emergency. This denial of access was on the ground 
of disability-or-perceived-disability because your delegate intoxicated-liar 
Shane Liu哥 did feel that his interlocutor is incapable (defenceless, 
vulnerable, disenfranchised, impotent, helpless, disabled) enough that he 
could use the emergency enforcers despite that there was no emergency and 
that there are alternative accommodations that preserve the Fields 
Institute's mission. You are kindly invited to continue this dialogue at the 
upcoming HRTO Tribunal file 2022-50344-I, or at the Police station, lol. You 
could remedy by cohosting my twinned workshop:

CfP: Workshop on proof-assistants, sheaves and applications, collocated 
around Ehrhard's 60th at CNAM Paris on 29 September 2022
Registration for authors and qualifying reviewers at: https://WorkSchool365.ca
Context: H¹(Δ²) = 0, H¹(S¹) ≠ 0 grammatically ?
  https://github.com/1337777/cartier/blob/master/cartierSolution11.v
  
https://anthroplogic.sharepoint.com/:w:/s/cycle1/EawPJF6xy0JJvnIetDv3Nt0BZohPMCYmdwqGCHF-LOT1gA?e=4ghBF8

For the computer, the relevance of "how" is witnessed onto the grammar/syntax 
and thus cannot be avoided, and Per Martin-Löf "equality of equalities" 
becomes, when taken seriously, (cubical) homotopy-path types (hott). Then the 
elimination principle for such path types, which should be some monodromy 
principle for locally constant sheaves, suggests the mediation via some 
univalence-axiom. Elsewhere Kosta Dosen cut-elimination confluence techniques 
in category theory provide some direct-encoding alternative to type theory 
(internal-logic encoding). Moreover the simplicial methods, instead of the 
globular/cubical shape of the boundaries, seem to be the better context for 
(Cech) sheaf cohomology, quasicategories-operad algebras...

Concretely this attempt at grammatical sheaf cohomology has shown that H¹(Δ²) 
= 0, H¹(S¹) ≠ 0. The augmented cochain complex for the (barycentric 
subdivision of the) 2-simplex Δ² is acyclic: the contracting homotopy is some 
grammatical (possibly-incompatible) gluing operation of the presheaf. Indeed 
the existence of semantic models satisfying such postulated grammar 
operations is demonstrated (by using the barycentric U0 U1 U01 as the good 
cover instead of U0 U1 ...). Finally the circle S¹ specifies some hole in the 
nerve of this 2-simplex Δ², thus breaking this acyclicity H¹(S¹) ≠ 0 (for the 
twisted locally constant sheaf). In full generality, with Kosta Dosen 
techniques, it should be possible to program the nerve of any topological 
site with structure (co-)sheaf, its (possibly-incompatible) 
gluing-differential and (co-)sheaf (co-)homology, up to any (Verdier) duality.

Here is the outline for the implementation of the idea (in COQ mathcomp 
ssralg). The nerve inductive type (where structCoSheafO could come from 
duality or from extension by 0, Stacks Lemma 00A4) is approximately:
Inductive nerve : forall (dimCoef: nat) (cell: seq vertexSet), Type :=
| GlueDiff : (_ : structCoSheafO [i_0; ... i_n])
(coface : forall i, nerve dimCoef [i; i_0; ... i_n] )
(face : forall j, nerve dimCoef [i_0; ... <i_j>; ... i_n]),
nerve (dimCoef+1) [i_0; ... i_n]  | Diff : ... | Empty : ... .

The presheaf record structure is approximately:
Structure shfyCoef_struct := { shfyCoef : forall (cell: seq vertexSet), Type;
restrict : forall j, shfyCoef [i_0; ... <i_j>; ... i_n] -> shfyCoef [i_0; ... 
i_n];
glue : (f_ : forall i, shfyCoef [i; i_0; ... i_n]) -> shfyCoef [i_0; ... i_n];
_ : restrict (glue (fun i => f_ i)) = glue (fun i => restrict (f_ i));
_ : glue (fun i => @restrict 0 f : shfyCoef [i; i_0; ... i_n]) = f;  ... }

Then the definition of the gluing-differential operation is approximately:
Definition diffGluing : (ff_ : forall cell, nerve dimCoef cell -> shfyCoef 
F_sh cell) ->
(forall cell, nerve (dimCoef+1) cell -> shfyCoef F_sh cell).

Finally the homotopy to the null-complex when the nerve has no holes is 
approximately:
glue (fun i => restrict 0 (ff_ [i_0; ... i_n]) +
                (\sum_(j < n+1) (-1)^(1 + j) * restrict (1 + j) (ff_ [i; i_0; 
... <i_j>; ... i_n])))
+ \sum_(j < n+1) (-1)^j * restrict j
     (glue (fun i => ff_ [i; i_0; ... <i_j>; ... i_n])
      + \sum_(k < n) (-1)^k * restrict k (ff_ [i_0; ... <i_k>; ... <i_j>; ... 
i_n])) = 
ff_ [i_0; ... i_n]

This setup is similar as the acyclicity of the mapping cone of some (gluing 
with shift -1) quasi-isomorphism, so that the shift is now -2. And this 
acyclicity proof is new, when compared to the Stacks Project Lemma 03AT, 
Lemma 0G6S, Lemma 01EM, Lemma 01FM, Lemma 02FU. This setup contains the proof 
that d ∘ d = 0, which should rely on the usual simplicial face relations δ_j 
∘ δ_i = δ_i ∘ δ_(j+1) for i <= j; however grammatically it becomes relevant 
how those faces-of-faces are specified and oneself may care about relevance 
up to d ∘ d ≠ 0 with d ∘ d ∘ d = 0 ... As for the Scholze Lean experiment, 
the first step has been some acyclicity proof.

The generalization to computational logic constructors is by recognizing that 
the pullback-sieve and the sum-sieve should be blended as 
sum-of-pullbacks-sieve in the definition of topological sites, approximately:
| GluingDiff : (sievesV_ : for all G with Site( G ~> U | in sieveU ), for 
some G' with Site( G ~> G' ),
                              is-sieve at G' refining-the-fixed-cover)
  (u_ : forall j, Site( G_ j ~> U | in sieveU )) 
  (ff_ : forall j, PreSheaves( Nerve structSheafO (sievesV_ (u_j)) [u_0; ... 
<u_j>; ... u_n] ~> Sheafified F ))
⊢ PreSheaves( Nerve structSheafO (sum-of-pullbacks sievesV_ over sieveU) 
[u_0; ... u_n] ~> Sheafified F )

The significance of such research programme, prompted from the mathematicians 
Kosta Dosen and Pierre Cartier, is similar as the significance of homotopy 
type theory or differential linear logic. Earlier COQ proofs of 
cut-elimination confluence for Maclane associativity coherence (the pentagon 
is some recursive square), adjunctions, comonads, cartesian products, 
enriched categories, internal categories, 2-categories, were published. This 
is sufficient evidence to "pay" long-term attention into this research 
programme.