The Coq mailing list

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

Salut Ciryl, indeed it is about time to start industrial labor into Dosen's 
ideas and techniques. In one line: the problem of contextual composition (cut 
elimination) and monoidal units (J-rule elimination) is solved by alternative 
formulations of adjunctions.

CfP: Workshop on implementing Dosen's categorial programming, collocated 
“around” CT2023 in July 2023

Registration: WorkSchool 365 is a new marketing format for authors/brands to 
disqualify reviewers/customers, with extra specialties for Coq via a Word 
document add-in; sign-in at https://WorkSchool365.com

Context: There is now sufficient evidence (ref [6], [7]) that Kosta Dosen's 
ideas and techniques (ref [1], [2], [3], [4], [5]) could be implemented for 
proof-assistants, sheaves and applications; in particular cut-elimination, 
rewriting and confluence for various enriched, internal, indexed or double 
categories with adjunctions, monads, negation, quantifiers or additive 
biproducts; quantitative/quantum linear algebra semantics; 
presheaf/profunctor semantics; inductive-sheafification and sheaf semantics; 
sheaf cohomology and duality...

[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

Proposal for prospective implementation:

The problem of “formulations of adjunction”, the problem of “unit objects” 
and also the problem of “contextual composition/cut” can be understood as the 
same problem. The question arises when one attempts to write precisely the 
counit/eval transformation ϵ_X ∶ catA(F G X, X) where F : catB → catA is the 
left-adjoint. One could instead write ϵ_X ∶ catA(F ,1)(G X, X) where the 
profunctor object/datatype catA(F ,1) is used in lieu of the unit 
hom-profunctor catA; in other words: F is now some implicit context, and the 
contextual composition/cut (in contravariant action) of some g:catB(Y, G X) 
in the unit profunctor against ϵ_X should produce an element of the same 
datatype: ϵ_X∘g : catA(F,1)(Y,X)... Ultimately Dosen-Petric (ref [5]) would 
be extended in this setting where some dagger compact closed double category, 
of left-adjoint profunctors across Cauchy-complete categories, is both inner 
and outer dagger compact closed where the dagger operation on profunctors (as 
1-cells) coincides with the negation operation on profunctors (as 0-cells), 
optionally with sheaf semantics and cohomology. The earlier Coq prototypes 
(ref [6] for example) show that the core difficulty is in the industrial 
labor and tooling, which requires a coordinated workshop of workers (not 
celebrities, lol).

Recall that closed monoidal categories (with conjunction bifunctor ∧ with 
right adjoint implication functor →) are similar as programming with linear 
logic and types. Now to be able to express duality, 
finitely-dimensional/traced/compact closed categories are often used to 
require the function space (implication →) to be expressible in basis form. 
But along this attempt to express duality, two (equivalent) pathways of the 
world of substructural proof theory open up: one route is via Barr’s 
star-autonomous categories and another route is via Seely’s linearly 
distributive categories with negation.

For star-autonomous categories, one adds a “dualizing unit” object ⊥ which 
forces the evaluation arrow A ⊢ (A → ⊥) → ⊥ into an isomorphism. For linearly 
distributive categories with negation, one adds a “monoidal unit” object ⊥ 
for another disjunction bifunctor ∨ whose negation A'∨- is right-adjoint to 
the conjunction A∧- where this adjunction is expressed via the help of some 
new associativity rule A∧(B∨C) ⊢ (A∧B)∨C called “dissociativity” or “linear 
distributivity” (used to commute the context A∧ - and the negated context 
-∨C); and it is this route chosen by Dosen-Petric to prove most of their 
Gentzen-formulations and cut-elimination lemmas (ref §4.2 of [3] for linear, 
ref §11.5 of [2] for cartesian, and ref §7.7 of [2] for an introductory 
example). In summary, those are two routes into some problem of “unit 
objects” in non-cartesian linear logic.

Some oversight about the problem of “unit objects” is the belief that it 
should have any definitive once-for-all solution. Instead, this appears to be 
a collection of substructural problems for each domain-specific language. 
Really, even the initial key insight of Dosen-Petric, about the 
cut-elimination formulation in the domain-specific language of categorial 
adjunctions, can be understood as a problem of “unit profunctor” in the 
double category of profunctors and the (inner) cut elimination lemma becomes 
synonymous with elimination of the “J-rule”; and recall that such 
equality/path-induction J-rule would remain stuck in (non-domain-specific) 
directed (homotopy) type theory.

Now the many “formulation of adjunctions” are for different purposes. Indeed 
the outer framework (closed monoidal category) hosting such inner 
domain-specific language (unit-counit formulation) could itself be in another 
new formulation of adjunctions (bijection of hom-sets) where the implication 
bifunctor  → is accumulated during computation via dinaturality (in contrast 
to the traditional Kelly-MacLane formulation).

Finally the problem of “contextual composition/cut” also arises from the 
problem of the structural coherence of associativity or dissociativity or 
commutativity, which now enables gluing the codomain/domain of compositions 
such as A∧f ∶ A∧X → A∧(B∨C) then g∨C ∶ (A∧B)∨C → Y∨C, or such as η_A ∶ I → 
A'∧A then ϵ_A∘f∧A' ∶ A∧A' → I, and which would force the outer framework to 
explicitly handle compositions under contexts/polycategories modulo 
associativity (“Gentzen cuts”) or to handle trace functions on arrows loops 
modulo cyclicity (for compact closed categories)... In other words, the meta 
framework (such as Blanqui’s LambdaPi and surprisingly not Coq’s CoqMT at 
present) of the framework should ideally implement those strictification 
lemmas (ref §3.1 of [2]) to be able to compute modulo structural coherence.

[6] Cut-elimination in the double category of profunctors with 
J-rule-eliminated adjunctions: 
https://github.com/1337777/cartier/blob/master/cartierSolution12.v ( 
/cartierSolution12.lp ; /maclaneSolution2.v MacLane’s pentagon is some 
recursive square! )

[7] Pierre Cartier