The Coq mailing list

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

Salut Ciryl

[updated]: https://github.com/1337777/cartier/blob/master/cartierSolution15.lp

Indeed your goal could be non-trivial if translation implies compilation via 
machine learning, especially Kosta Dosen's normalization of functorial 
programs.

Kosta Dosen’s book « Cut-elimination in categories » (1999) is how some good 
substructural formulation of the Yoneda lemma, via profunctors, allows for 
computation and automatic-decidability of categorial equations. For example, 
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 –)

This new stricter typing discipline is still successful to compute with 
polynomials (morphisms of polynomial-bicomodules along cofunctors of 
categories, substitution of polynomials, and their prafunctor semantics) via 
their underlying profunctors. It is conjectured that these computations can 
be extended to analytic functors and their automatic differentiation (via 
linear-logic's exponential comonad on the underlying profunctors) in 
reverse-mode (differential categories) for gradient-based neural-learning...

And now this updated implementation of fibred profunctors has a draft 
application to inductively-constructed covering sieves and sheaf topology: a 
sieve is a fibred profunctor dependent over the hom-profunctor; and the 
Yoneda action and lemma (gluing) still holds when the hom-profunctor (the 
total sieve) is replaced by any covering sieve and the presheaf is replaced 
by a sheaf.


  symbol _'∘>yonedaTotalDep : Π [X Y I: cat] [F : func I X] [R : mod X Y] [G 
: func I Y] [r : hom F R G] [A : catd X] [B : catd Y] [II] [FF : funcd II F 
A] [RR : modd A R B] [GG : funcd II G B], Π [J: cat] [M : func J X] [JJ : 
catd J] (MM : funcd JJ M A), 
  homd r FF RR GG → transfd ((M)_'∘>yonedaTotal r) (Unit_modd MM FF) Id_funcd 
(MM ∘>>d RR) GG; 


This is not yet another "categorical semantics of", but here the categories 
are syntax which compute (in the Lambdapi proof assistant). For example, here 
is my review of the folks at "categoricaldeeplearning.com" : it is mostly 
categorical semantics fluff of structural-invariants (by permutation, by 
translation, etc.) over the domain's metric (discrete, fully-connected, 
shortest path, etc.) that are baked into each neural network architecture 
(Deep Sets, Transformers, Graph Neural Networks, Convolutional Neural 
Networks, etc)... nothing "deep", lol

Unlike this bad faith's "blind expert peer reviewer" enT8 at ACT2024 who 
wrote about cartierSolution15.lp : « This talk purports to prove that 1 + 2 = 
3 in multiple ways ... is full of comments saying "todo" ... » but aren't 
these cartierSolution13.lp cartierSolution14.lp done? [CfP] Would this 
reviewer kindly disclose hemself so that we settle 1 + 2 = 3 on a blackboard 
at CT2024 or at re365.net:

re365.net is a free open source Microsoft 365 app, developed by a community 
(https://meetup.com/dubai-ai) of 2,000+ contributors, to Schedule reviews 
with authors and businesses, with the end-goal to co-author or by-product an 
AI interface for their papers and apps API. And https://dailyReviews.link is 
an instance of re365.net for the topics of math.CT/cs.LG/cs.LO; it is some 
kind of tiktok-style calendar overlay of arxiv.org and producthunt.com (and 
soon semanticscholar.org) for users (and editors/marketers) to schedule 
reviews with VIP authors/developers.

Frankly, re365.net tries to answer this question: what does the usual 
practice of citing an (arxiv) preprint paper mean, if it does not mean a 
"blind expert peer review"?