The Coq mailing list

[Théo Zimmermann <theo.zimmermann AT telecom-paris.fr>]

Dear Christopher Mary,

The message you sent on Friday was in violation of the Coq Code of 
Conduct [1].

This is your second warning for a Code of Conduct violation in a 3-month 
period. It seems to indicate that you have not understood or not 
accounted for our previous warning.

Therefore, this second warning comes with a 6-month temporary ban from 
all official Coq spaces both online (Coq-Club mailing list, Zulip, 
Discourse, Coq GitHub organization) and offline (CoqPL and Coq 
workshop), starting today. We count on you to abide by this ban and to 
change your behavior when the ban is over. If it doesn't happen, we may 
be forced to issue a permanent ban.

If it is not completely clear to you why your message was in violation 
of the Code of Conduct or how you can change your behavior, you are free 
to write to us to coq-conduct AT inria.fr (the ban does not apply there).

Best regards,
The Coq Code of Conduct enforcement team

[1]: https://github.com/coq/coq/blob/master/CODE_OF_CONDUCT.md

On 04/10/2024 14:37, Christopher Mary wrote:
> Nicolas “pain au chocolat” Tabareau,
>
>      [ERRATA] 
> https://github.com/1337777/cartier/blob/master/cartierSolution16.lp
>
> En effet, merci de ton aide pour l’errata, mais conformément à l’article 6 de 
> la loi 2004-575, j’ai un droit de réponse à ton désaveu public… Sonya Massey 
> would say “I rebuke you too”, lol #MeToo
>
> -----
>
> Review of Max Zeuner defending “Constructive Algebraic Geometry”.
>
> MAX [1] shows an equivalence between functorial schemes X and 
> locally-ringed-lattice schemes Y, approximately:
>
>      LRDL^op( X ⇒ Spec , Y )  ≅   ( X ⇒ LRDL^op( Spec( – ), Y ) )
>
> Where  ( X ⇒ X' ) ∶= Fun( CommRing , Set )( X , X' ) are abbreviations in the 
> category of functors from commutative rings to sets, where LRDL^op is the 
> opposite of the category of “locally” ringed distributive lattices, where 
> Spec: Fun(  CommRing^op, LRDL^op ) is the functor sending a commutative ring 
> to (the underlying set of) its Zarisky lattice, and where “locally” for a 
> lattice Y with sheaf of rings O_Y means the existence of an operation
>
>       D: (u : Y) → O_Y (u) → u↓Y
>
> where D_u(f) is intended to be the open in the slice lattice under u where 
> the function f:  O_Y (u) is invertible.
>
> … But this won’t work; I judge Max’s defense as a “thèse à crédit”.
>
> A prerequisite is a computational logic (type theory) for categories, 
> presheaves, sites and locally ringed sites. This requirement is especially 
> manifest for the etale topology where the “objects” of the site are etale 
> morphisms (adjoint pairs of cocontinuous/continuous functors between sites). 
> Note that the existing attempts at “2-dimensional type theory” as in Marcelo 
> Fiore [2] have a flaw in that they try to implement the interchange law 
> directly  (α ∘_0 β) ∘_1 (γ ∘_0 δ) =  (α ∘_1 γ) ∘_0 (β ∘_1 δ) when in reality 
> it hides subtle Yoneda-actions related to the fact that the profunctor 
> C[F-,_] is a distinct computer type than the hom-profunctor C[-,_] of the 
> category C applied to outer objects of the form F- ...
>
> A draft solution has been implemented in
>
>      https://github.com/1337777/cartier/blob/master/cartierSolution16.lp
>
> as a natural transformation from the structure sheaf to the sieves-classifier 
> (“subobject classifier” for the small topos of the scheme Y)
>
>      D: O_Y → Ω
>
> where D_u(f) is intended to be the SIEVE in Ω(u) under u of all opens where 
> the function f: O_Y (u) is invertible. This requires the presence of a 
> classifier/universe Ω for sieves, but because of Kosta Dosen 
> cut-elimination-in-categories techniques, it is not necessary to work 
> “internally” as in Thierry Coquand [3] to get a logic which computes. Now a 
> sieve S under the object U can be realized as a (“dependent”) profunctor in 
> groupoids over the category of elements of U; that is the sieves need not be 
> (-1)-truncated subobjects as in Nicolas Tabareau [4, definition 5.5], because 
> checking instead that the cohomology differential is 0 will be an alternative 
> way to check for compatibility of a family of sections of the sheaf 
> (alternative to “internally” ensuring this compatibility)... Moreover, this 
> profunctor framework will allow a hybrid definition of the site and 
> functor-of-points approaches to schemes. But all this computational logic 
> foundations are still far from your typical birational algebraic geometry 
> conference [5], which usually start with blowing up schemes (projective Proj 
> bundles) and doing cases analyses with Cartier divisors...
>
> It is a strange coincidence that the formula D: O_Y→Ω resembles the formula 
> d:  O_Y→Ω  for Kahler differentials, but the open problem of discovering a 
> (graded) differential linear logic formulation for the algebraic-geometry’s 
> cohomology differentials will be investigated instead in an upcoming review 
> via the profunctorial semantics of linear logic in the context of sieves as 
> profunctors… It will also be reviewed how outrageous is Ehrhard’s [6, section 
> 3.1.1, page 44] definition of the composition of polynomials by the use of 
> differentials instead of by elementary concepts,
>
>       g ∘ f  =  Σ_(i: 0..n) (1/i!) g⋅d’^i⋅f^(⊗i)⋅c^i
>
> and how this motivates the search of a hybrid framework⋅ combining polynomial 
> functors (good algebra) “depending” on analytic functors (good logic) …
>
> [1] Max Zeuner “Univalent Foundations of Constructive Algebraic Geometry” 
> (defending Oct 4th 2024)
> [2] Marcelo Fiore “A type theory for cartesian closed bicategories”
> [3] Thierry Coquand “A foundation for synthetic algebraic geometry”
> [4] Nicolas Tabareau “Lawvere-Tierney sheafification in homotopy type theory”
> [5] SCMS 上海数学中心 “Workshop on Birational Geometry - September 2024”
> [6] Thomas Ehrhard “An introduction to differential linear logic: proof-nets, 
> models and antiderivatives”
>
> -----
>
> A copy of this review is at https://dailyReviews.link (by re365.net open 
> source Microsoft 365 app), the tiktok-style calendar overlay for all your 
> research communications!