The Coq mailing list

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

Dear Steve "hott" Awodey,

Congratulations on your "coup" attempt; but here is a plot twist... lol

I asked Gemini 2.5 Pro to take a specification of `emdash` written in 
Lambdapi 

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

and to output a new functorial programming language for ω-categories and 
schemes implemented in Typescript

https://github.com/hotdocx/emdash

`emdash` 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.

OK, then I wanted Gemini 2.5 Pro to produce a technical report of emdash,

but this entailed the ability to generate commutative arrow diagrams SVG from 
textual JSON specifications,

so I asked Gemini 2.5 Pro to generate a new app `arrowgram` which hooks into 
the markdown rendering pipeline

https://github.com/hotdocx/arrowgram

And then such contextual Gemini 2.5 Pro is able to generate entire research 
papers

with katex latex math, mermaid conceptual diagrams, vega-lite data analysis 
charts, two-columns, reveal-js presentation slides,

from any source markdown text, latex, images or PDF via Mistral AI OCR,

and with commutative arrowgrams JSON specs (e.g. pullbacks) either AI 
generated or imported from `q.uiver.app`

OK, now how to publish, distribute and market the source hint/prompt 
engineering with its generated output? 

I got greedy and I asked Gemini 2.5 Pro to clone easychair + reddit + meetup 
+ cursor and surprisingly it did, the result: `hotdocx`.

hotdocx is a sponsored open source project hosted on Github itself

https://github.com/sponsors/hotdocx

https://hotdocx.github.io

hotdocx is 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 (conditionned by 
in-app purchases). This, is hotdocx.

For instance, hotdocx has transformed the `emdash` functorial programming 
into this paper-app event which is:

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

Therefore do you think hotdocx.github.io would be a good tool for you to 
co-editorialize a new [CFP] CT-X workshop (of Gemini 2.5 Pro eXperiments) 
colocated near @CT2025 in Brno this July?

Otherwise I would suspect similar "QMJ -> ZML" moves to be either a "bomber 
paradox" oversight, or worse: a cosmetics decoy towards even-more opaquely 
inconsistent and insidious circulation of falsified "currencies" within 
scientific publishing?

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

The truth is, Kosta Dosen had already solved the computational kernel of 
functorial programming decades ago, as I have implemented in this Lambdapi 
spec. Now instead of paying me a $5 GitHub sponsoring ( 
https://github.com/sponsors/hotdocx ), some copycats would rather "jump" me 
and steal the hints as usual (and then probably ask Gemini 2.5 Pro to rebrand 
it, lol), or would rather boycott me and print money (falsified "currencies") 
only for themselves. One would have guessed that because "functorial 
elaboration" involves "labor" then the copycats wouldn't want to monopolize 
this science (unlike nuclear physics, lol)


```
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));
```