The Coq mailing list

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

Salut DCC, ton 2ème cours sémantique m'ennuyait alors en attente du 3ème 
cours syntaxique voici une response at yesterday's Joyal hint towards hes 
alternative presentation via barrels (profunctors):

  https://ncatlab.org/joyalscatlab/published/Distributors+and+barrels

implemented as cut-elimination in the double category of 
dependent-profunctors with J-rule-eliminated adjunctions:

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

Here, a covering (co)sieve is implemented simply as a fibration of 
profunctors, which covers some base (unit-hom) profunctor at some fixed 
covariant variable (the contravariant piece is understood as some codomain 
fibration of categories). This was hinted also in Joyal's page.

Now this failure of sieves being monomorphisms is the motivation for the new 
“grammatical sheaf cohomology”, where the redundant storage space for 
functions defined over the topology is what allows possibly-incompatible 
functions to be glued:

  gluing: F(U0)⊕F(U1)⊕F(U01) → F(U)
  ((f0,f01),(g1,g01),(h01)) ↦ (f0,g1,f01+g01-h01)

Another alternative from “type theory” and its types with (global) elements, 
is instead Kosta Dosen-style “categorial programming” which is about 
morphisms (generalized elements) between profunctor-types (of arrows data). 
This new functorial lambda calculus evaluation has been implemented as:

  “ϵ_(B,O)∘ B⊗(g)” ∘ (x⊗f)
  = “ϵ_(A,O)∘ A⊗((x⇒O) ∘ (g ∘ f))” , for x:A→B

where the input argument x is simply accumulated using the implication _⇒_ 
bifunctor. And the new “J-rule” has been implemented as simply the 
construction that, given some global element of some profunctor datatype, it 
generates the morphism (transformation) from the unit-hom-profunctor towards 
this profunctor datatype (semantically by covariant/contravariant 
action/composition):

  | Unit_con_transf : Π [I A B J : cat] [F : func I A] [R : mod A B] [G : 
func I B], Π (M : func J A), hom F R G → transf (Unit_mod M F) Id_func (M ∘>> 
R) G

Therefore, this general setup has facilitated the implementation of 
cut-elimination (J-rule elimination) for any adjunctions of functors and of 
their decidability of equations between data (arrows inside categories). Also 
this implementation has expressed and proved computationally that any right 
adjoint functor preserves the profunctor-weighted limits of other functors:

  assert [B J J' A I : cat] (F : func J B) (W : mod J' J) (F_⇐_W : func J' B) 
(isl : isLimit F W F_⇐_W) (R : func B A) (L : func A B) (isa : isAdj L R) (M 
: func I A) ⊢
  ((((M)_'∘> (Adj_cov_hom isa F)) ⇐2 (Id_transf W))
    ''∘ (limit_intro_transf isl (M ∘> L)))
          ''∘ ((Adj_con_hom isa M) ∘>'_(F_⇐_W))
  : transf ((Unit_mod M (R <∘ F)) ⇐ W) Id_func (Unit_mod M (R <∘ F_⇐_W)) 
Id_func

This implementation moreover would enable new executable applications to the 
study of graphs transformations understood as categorial rewriting in a 
double category, where the objects are graphs, the vertical monomorphisms are 
pattern-matching subterms inside contexts and the horizontal morphisms are 
congruent/contextual rewriting steps.

Finally, the core difficulty at implementing Kosta Dosen (ref [1], [2], [3], 
[4], [5]) would be the long-term synchronized industrial labor and the new 
format for reviewers-productive-output, which requires tools such as:

  [CfP] WorkSchool 365 is a new marketing format for authors/brands to 
disqualify reviewers/customers, sign-in at https://WorkSchool365.com 

[1] Dosen-Petric: Cut Elimination in Categories 1999;
[2] Proof-Theoretical Coherence 2004; 
[3] Proof-Net Categories 2005; 
[4] Coherence in Linear Predicate Logic 2007; 
[5] Coherence for closed categories with biproducts 2022
[6] Pierre Cartier