The Coq mailing list

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

Dear Jesús,

Thanks for the updates to `coq-lsp` and the upcoming port of `jsCoq` to 
`coq-lsp`; but your last update from `jscoq AT 0.15.1` to `jscoq AT 0.16.0` titled 
"Port the JS codebase to ES modules" had introduced some regressions in 
usability, which I learned the hard way (an afternoon wasted, lol)

Indeed, I was trying to integrate a `jsCoq template` into the `hotdocx` 
calendared-marketplace publisher:

https://hotdocx.github.io/#/hdx/25191CHRI43000    (jsCoq template)

but it turns out that `jsCoq` versions after 0.15.1 throw the error "Cannot 
use 'import.meta' outside a module" when used within a `Sandpack` sandbox 
environment.

Therefore I had to downgrade your `jsCoq` npm package down to `jscoq AT 0.15.1` 
to make it work; or could you try and find an alternative solution? In fact, 
with your help, we could upgrade `jsCoq` into a full integration instance 
`hotdocx/jsCoq` which would solve these two earlier goals attempts:

- Yves Bertot's "Coq Exchange" 

  https://project.inria.fr/coqexchange/news/

- Thomas Lamiaux's "Coq Platform Doc"  

  https://coq.inria.fr/docs/platform-docs

`hotdocx` is a sponsored open source project hosted on GitHub itself; and 
institutions such as INRIA/Coq can host their own instance of hotdocx:

https://github.com/sponsors/hotdocx

hotdocx/jsCoq would be the hottest fastest calendared marketplace publisher: 
publish your daily experiences apps, get paid.

Imagine a web and mobile app (published in the Android store), where users, 
anonymous or verified via Stripe or GitHub Sponsor payment, post events at 
local business places or online (via SharePoint Teams), based on `paper-app` 
AI templates (such as the `emdash`, `arrowgram`, `jsCoq` templates) which can 
cite/review references from overlaid document libraries such as arxiv + 
SharePoint + GitHub repositories, and which can be cited/reviewed (with 
confidentiality config options) by other remixing events conditioned by 
in-app purchases). This, is hotdocx and would be hotdocx/jsCoq.

Here is an example of an `arrowgram` AI template in hotdocx:

https://hotdocx.github.io/#/hdx/25188CHRI26000

I specially created this new `arrowgram` drawing app for hotdocx; it hooks 
into the markdown rendering pipeline and renders category-theory commutative 
arrow diagrams SVG from (AI generated) JSON specifications (or from imported 
`https://q.uiver.app` drawn-diagrams).

https://github.com/hotdocx/arrowgram

These hotdocx AI templates pipelines, such as the `arrowgram` template, can 
generally be extended with markdown/latex, katex math, mermaid conceptual 
diagrams, vega-lite data analysis charts, two-columns papers, reveal-js 
presentation slides, etc. In general these hotdocx AI templates pipelines can 
be prefixed by a Mistral AI OCR preprocessing of PDF files input to extract 
markdown latex math text together with base64-encoded images; and of course 
the pipeline and its whole context of files and agentic tools can be 
post-processed in cascade by the Gemini 2.5 Pro AI.

Here are other examples of how I specially created this new `emdash` 
functorial programming language for hotdocx, to show how hotdocx AI templates 
are:

- re-formattable,
 
  https://hotdocx.github.io/#/hdx/25188CHRI25004
  
- and experiment-able,
  
  https://hotdocx.github.io/#/hdx/25188CHRI27000

`emdash` is a new functorial programming language implemented in Typescript; 
it features a bidirectional type checker with higher-order unification-based 
hole solving for interactive proof, definitional equality via βδι-reduction 
(including user-supplied rewrite rules and unification rules), Higher-Order 
Abstract Syntax (HOAS) for binders, and features a new "functorial 
elaboration" paradigm where coherence laws (e.g., functoriality, naturality) 
for kernel constructors are definitionally verified via Kosta Dosen 
techniques. `emdash` implementation in typescript was "essentially generated" 
by Gemini 2.5 Pro AI from a specification written in Lambdapi (i.e. a manual 
correction to a "mathematically-correct bug" in HOAS architecture made all 
the standard dependent-types unit-tests pass from 300 seconds down to less 
than 1 second, etc.):

https://github.com/1337777/cartier/blob/master/cartierSolution18.lp

https://github.com/hotdocx/emdash/blob/main/docs/emdash.pdf

https://github.com/hotdocx/emdash

This `emdash` example illustrate the importance and necessity for hotdocx 
templates pipelines to be able to leverage AI.

Therefore do you think hotdocx.github.io would be a good platform for us to 
co-editorialize a new version of Bertot's "Coq Exchange" with hotdocx/jsCoq 
integration?

If not, then I will just steal Coq kernel source code into my `emdash` 
functorial proof assistant anyway, and ask Gemini 2.5 Pro to rebrand it, lol


References:
[1]   Kosta Dosen; Zoran Petric. “Cut Elimination in Categories” (1999)
[2]   Pierre Cartier.
[3]   Gemini 2.5 Pro. via hints



# APPENDIX PART 1 — EMDASH SPECIFICATION IN LAMBDAPI

TLDR: the composition term `∘>` is clearly decreasing in the functionality 
rule  `F a' ∘> F a  ↪  F (a' ∘> a)`  but it is not clear how one should 
orient the naturality rule  `ϵ._X ∘> G a  ↪  (F a) _∘> ϵ._X'`  so that the 
composition term on the RHS is smaller; the key insight by Dosen is that the 
RHS is actually a Yoneda/hom action/transport not the usual composition... 
Then extensionality/univalence is directly expressible via rules such as 
`@Hom Set $X $Y ↪ (τ $X → τ $Y)`. The prerequisite benchmark becomes whether 
`symbol super_yoneda_functor : Π [A : Cat], Π [B : Cat], Π (W: Obj A), 
Functor (Functor_cat B A) (Functor_cat B Set)` becomes computationally 
expressible in this specification by `reflexivity` proofs alone. Furthermore 
simplicial/cubical ω-categories become expressible via an elementary insight: 
given the usual triangle simplex `{0,1,2}` with arrows `f : 0 -> 1`, `g: 1 -> 
2` and `h: 0 -> 2`, then the `projection functor` which maps a surface `σ: f 
-> h over g` to its base line `g` will indeed also functorially map a volume 
from `σ` down to a base surface from `g`... visually: 

https://cutt.cx/fTL 

Ultimately it becomes expressible to extend the sheafification functor from a 
site topology closure operator, and to specify a co-inductive computational 
logic interface for algebraic-geometry schemes, as outlined in 

https://github.com/1337777/cartier/blob/master/cartierSolution16.lp


```
constant symbol Cat : TYPE;

injective symbol Obj : Cat → TYPE;

injective symbol Hom : Π [A : Cat] (X: Obj A) (Y: Obj A), TYPE;

constant symbol Functor : Π(A : Cat), Π(B : Cat), TYPE;

symbol fapp0 : Π[A : Cat], Π[B : Cat], Π(F : Functor A B), Obj A → Obj B;
symbol fapp1 : Π[A : Cat], Π[B : Cat], Π(F : Functor A B),
  Π[X: Obj A], Π[Y: Obj A], Π(a: Hom X Y), Hom (fapp0 F X) (fapp0 F Y);

constant symbol Transf : Π [A : Cat], Π [B : Cat], Π (F : Functor A B), Π (G 
: Functor A B), TYPE;

// notation:  (ϵ)._X  for  tapp ϵ X
symbol tapp : Π [A : Cat], Π [B : Cat], Π [F : Functor A B], Π [G : Functor A 
B],
  Π (ϵ : Transf F G), Π (X: Obj A), Hom (fapp0 F X) (fapp0 G X);

constant symbol Functor_cat : Π(A : Cat), Π(B : Cat), Cat;

unif_rule Obj $Z ≡ (Functor $A $B) ↪ [ $Z ≡ (Functor_cat $A $B) ];

rule @Hom (Functor_cat _ _) $F $G ↪ Transf $F $G;

unif_rule Obj $A ≡ Type ↪ [ $A ≡ Set ];

rule @Hom Set $X $Y ↪ (τ $X → τ $Y);

// yoneda covariant embedding functor to Set; also TODO: contravariant Yoneda
// notation:  f _∘> a  for  (fapp1 (hom_cov W) a) f;
constant symbol hom_cov : Π [A : Cat], Π (W: Obj A), Functor A Set;

rule fapp0 (hom_cov $X) $Y ↪ Hom_Type $X $Y;

constant symbol Cat_cat : Cat;

unif_rule Obj $A ≡ Cat ↪ [ $A ≡ Cat_cat ];

rule @Hom Cat_cat $X $Y ↪ Functor $X $Y;

constant symbol hom_cov_cat : Π [A : Cat], Π (W: Obj A), Functor A Cat_cat;

// the objects-map of hom_cov_cat is hom_cov
rule Obj (fapp0 (hom_cov_cat $W) $Y) ↪ Hom $W $Y;
rule fapp0 (fapp1 (hom_cov_cat $W) $a) $f ↪ (fapp1 (hom_cov $W) $a) $f;

// notation:  `f ∘> g`   or   `g <∘ f`   for  `compose_morph g f`
symbol compose_morph : Π [A : Cat], Π [X: Obj A], Π [Y: Obj A], Π [Z: Obj A], 
Π (g: Hom Y Z), Π (f: Hom X Y),  Hom X Z;

// f _∘> a   ≡   f ∘> a
unif_rule (fapp1 (hom_cov $W) $a) $f ≡ compose_morph $a $f ↪ [ tt ≡ tt ];

// F a' ∘> F a  ↪  F (a' ∘> a) 
rule compose_morph (@fapp1 _ _ $F $Y $Z $a) (@fapp1 _ _ $F $X $Y $a')
  ↪ fapp1 $F (compose_morph $a $a');
  
  //  ϵ._X ∘> G a  ↪  (F a) _∘> ϵ._X'
rule compose_morph (@fapp1 _ _ $G $X/*/!\*/ $X' $a) (@tapp _ _ $F $G $ϵ $X)
↪ fapp1 (hom_cov _) (tapp $ϵ $X') (fapp1 $F $a);

// # ω-category, arrow/comma category, dependent arrow category of a 
dependent/fibration category 

constant symbol Total_cat [A : Cat] (M: Functor A Cat_cat): Cat;
injective symbol Total_cat_proj [A : Cat] (M: Functor A Cat_cat): Functor 
(Total_cat M) A;

rule Obj (Total_cat $M) ↪ `τΣ_ X : Obj _, Obj_Type (fapp0 $M X);

rule @Hom (Total_cat $M) $Y_f $Y'_f' 
↪ `τΣ_ a : Hom (sigma_Fst $Y_f) (sigma_Fst $Y'_f'), 
      @Hom_Type (fapp0 $M (sigma_Fst $Y'_f')) (fapp0 (fapp1 $M a) (sigma_Snd 
$Y_f)) (sigma_Snd $Y'_f');

rule fapp0 (Total_cat_proj $M) $Y_f ↪ sigma_Fst $Y_f;
rule fapp1 (Total_cat_proj $M) $a_ϕ ↪ sigma_Fst $a_ϕ;

// this expresses that  `@hom_cov_cat (Total_cat M) (W_,W) : Functor 
(Total_cat M) Cat`
//  is both fibred over  `Total_cat M` and is above/projects to  
`@hom_cov_cat A W_`
// also expresses composition in ω-category and whiskering/composition of 
2-cell by 1-cell
symbol hom_cov_cat_total_proj [A : Cat] (M: Functor A Cat_cat) (W : Obj 
(Total_cat M)):
  Transf (@hom_cov_cat (Total_cat M) W) (fapp1 (@hom_cov Cat_cat _) 
(@hom_cov_cat A (fapp0 (Total_cat_proj M) W)) (Total_cat_proj M));
```