[HoTT] Re: new arxiv calendar overlay — [Coq-Club] Postdoc Machine Learning

[HoTT] Re: new arxiv calendar overlay — [Coq-Club] Postdoc Machine Learning

[admin]

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"?




-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/DS0PR20MB6232AB422CDB77864CEBEED191D42%40DS0PR20MB6232.namprd20.prod.outlook.com.