The Coq mailing list

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

Salut Louis Auguste « L'Enfermé » Blanqui,

  A new implementation of dependent types via Dosen's substructural 
categorial programming: example of the Yoneda lemma for fibrations

This closes the open problem of implementing a dependent-types computer for 
category theory, where types are categories and dependent types are 
fibrations of categories. The basis for this implementation are the ideas and 
techniques from Kosta Dosen's book « Cut-elimination in categories » (1999), 
which essentially is about the substructural logic of category theory, in 
particular about how some good substructural formulation of the Yoneda lemma 
allows for computation and automatic-decidability of categorial equations.

The core of dependent types/fibrations in category theory is the Lawvere's 
comma/slice construction and the corresponding Yoneda lemma for fibrations 
(https://stacks.math.columbia.edu/tag/0GWH), thereby its implementation 
essentially closes this open problem also investigated by Cisinski's directed 
types or Garner's 2-dimensional types. What qualifies as a solution is subtle 
and the thesis here is that Dosen's substructural techniques cannot be 
bypassed.

In summary, this text implements, using Blanqui's LambdaPi metaframework 
software tool, an (outer) cut-elimination in the double category of fibred 
profunctors with (inner) cut-eliminated adjunctions. The outer 
cut-elimination essentially is a new functorial lambda calculus via the « 
dinaturality » of evaluation and the monoidal bi-closed structure of 
profunctors, without need for multicategories because (outer) contexts are 
expressed via dependent types. This text also implements (higher) inductive 
datatypes such as the join-category (interval simplex), with its 
introduction/elimination/computation rules. This text also implements 
Sigma-categories/types and categories-of-functors and more generally 
Pi-categories-of-functors, but an alternative more-intrinsic formulation 
using functors fibred over spans or over Kock's polynomial-functors will be 
investigated. This text also implements a dualizing Op operations, and it can 
computationally-prove that left-adjoint functors preserve profunctor-weighted 
colimits from the proof that right-adjoint functors preserve 
profunctor-weighted limits. This text also implements a grammatical 
(univalent) universe and the universal fibration classifying small 
fibrations, together with the dual universal opfibration. Finally, there is 
an experimental implementation of covering (co)sieves towards grammatical 
sheaf cohomology and towards a description of algebraic geometry's schemes in 
their formulation as locally affine ringed sites (structured topos), instead 
of via their Coquand's formulation as underlying topological space...

References:

[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] Cut-elimination in the double category of fibred profunctors with inner 
cut-eliminated adjunctions: 
https://github.com/1337777/cartier/blob/master/cartierSolution13.lp 
[7] Pierre Cartier

Subscribe for live updates, WorkSchool365.com : 
https://www.youtube.com/@workschool365

FAQ:

* How is « substructural » contrasted vs « synthetic » ? The substructural 
Yoneda lemma for fibrations is expressed via a blend of the 
universality/introduction rule of the transported/pulledback objects inside 
fibred categories:

  constant symbol Fibration_con_intro_homd : Π [I X X'  : cat] [x'x : func X' 
X] (G : func X I) [KK : catd X'] [F : func X' I] [II : catd I] (II_isf : 
isFibration_con II) (FF : funcd KK F II) (f : hom x'x (Unit_mod G Id_func) F) 
[X'0 : cat] [x'0x : func X'0 X] [X'' : cat] [x''x' : func X'' X'] [x''x'0 : 
func X'' X'0] (x'0x' :  hom x''x'0 (Unit_mod x'0x x'x) x''x') [JJ : catd X'0] 
(MM : funcd JJ x'0x (Fibre_catd II G)) [HH : funcd (Fibre_catd KK x''x') 
x''x'0 JJ],
homd ((x'0x' '∘ ((x'0x)_'∘> f))) HH (Unit_modd (MM ∘>d (Fibre_elim_funcd II 
G)) Id_funcd) ((Fibre_elim_funcd KK (x''x')) ∘>d FF) →  
homd x'0x' HH (Unit_modd MM (Fibration_con_funcd G II_isf FF f)) 
(Fibre_elim_funcd KK (x''x')) ;

together with the composition operation (in Yoneda formulation) inside fibred 
categories:

  constant symbol ∘>d'_ : Π [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], homd r FF RR GG → 
Π [J: cat] [M : func J Y] [JJ : catd J] (MM : funcd JJ M B), 
transfd ( r ∘>'_(M) ) (Unit_modd GG MM) FF (RR d<<∘ MM ) Id_funcd;            
    

* How is « J-rule arrow induction » contrasted vs « fibrational transport » ? 
The above intrinsic/structural universality formulation comes with a 
corresponding reflected/internalized algebra formulation, which is the comma 
category where the J-rule elimination ("equality/path/arrow induction") 
occurs. Similarly, pullbacks have a universal formulation (fibre of 
fibration), an algebraic formulation (composition of spans), or mixed 
(product of fibration-objects in the slice category).

  constant symbol Comma_con_intro_funcd : Π [A B I : cat] [R : mod A B] (BB : 
catd B) [x : func I A] [y : func I B] (r : hom x R y),
funcd (Fibre_catd BB y) x (Comma_con_catd R BB);

  constant symbol Comma_con_elim_funcd : Π [I X : cat] (G : func X I)  [II : 
catd I] (II_isf : isFibration_con II) [KK : catd I] (FF : funcd KK Id_func 
II), 
funcd (Comma_con_catd (Unit_mod G Id_func) KK) G II;

* Are substitutions explicit or intrinsic/structural? Ordinary (non-fibred) 
cut-elimination considers pairs of composable arrows p : X → Y then q : Y → 
Z, but fibred cut-elimination should also consider pairs of arrows p : X → 
f*Y then q : g*Y → Z, where f*Y is the pullback of Y along f, and such a pair 
is not manifestly/grammatically/syntactically-composable but only 
semantically-composable as g'*p : g'*X → g'*(f*Y) then f'*q : f'*(g*Y) → 
f'*Z, where f' = g*f is the pullback of f along g and g' = f*g is the 
pullback of g along f. The remedy is to make those pullback 
intrinsic/implicit in the implementation's grammar, so that p : X → f*Y is 
really notation for a judgment with 3 parameters X, Y and f, which can be 
read as « p is a fibred arrow forward-above the arrow f », and similarly q : 
g*Y → Z is read as « q is a fibred arrow backward-above the arrow g », and 
more generally r : g*X → f*Z is read as « r is a fibred arrow above the span 
of arrows g backward with f forward ». Ultimately it should be possible to 
express arrows fibred over polynomial-functors, so that the distributivity 
(ΠΣ = ΣΠε*) in the composition of polynomial-functors is intrinsic in the 
implementation's grammar... Finally, all of these intrinsic structures are 
reflected/internalized as an explicit substitution/pullback-type-former for 
any fibration.

* What is the difference between the Pi-type of sections and the 
category-of-functors? Ordinary Pi/product-types consider only the sections of 
some fibration, but Pi-categories should consider all the 
category-of-functors to some fibration, this leads to the new construction of 
Pi-category-of-functors. The preliminary implementation in this text does not 
yet use the more-intrinsic formulation using functors fibred-above-a-span of 
functors. It should be noted that Sigma/sum-categories can be already 
intrinsically-implemented using only functors fibred-forward-above a single 
functor.

* And why profunctors (of sets)? The primary motivation is that they form a 
monoidal bi-closed double category (functorial lambda calculus). Another 
motivation is that the subclass of fibrations called discrete/groupoidal 
fibrations can only be computationally-recognized/expressed instead via 
(indexed) presheaves/profunctors of sets. And the comma construction is how 
to recover the intended discrete fibration. Ultimately profunctors enriched 
in preorders/quantales instead of mere sets could be investigated (Tholen's 
TV, lol).

* What is a fibred profunctor anyway? The comma/slice categories are only 
fibred categories (of triangles of arrows fibred by their base), not really 
fibred profunctors. One example of fibred profunctor from the coslice 
category to the slice category is the set of squares fibred by their diagonal 
which witnesses that this square is constructed by pasting two triangles. 
This text implements such fibred profunctor of (cubical) squares (thereby 
validating the hypothesis that computational-cubes should have 
connections/diagonals...). For witnessing the (no-computational-content) 
pasting along the diagonal, this implementation uses for the first time the 
LambdaPi-metaframework's equality predicate which internally-reflects all the 
conversion-rules; in particular the implementation uses here the 
categorial-associativity equation axiom, which is a provable metatheorem 
which must *not* be added as a rewrite rule!