[Agda] position in Deducteam — Lawvere/Dosen session on categorial logic/programming @ CT2023

[admin]

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!