[Qualifier] Functorial Programming

This text implements Kosta Dosen’s functorial programming. 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 with Yoneda lemma for fibrations. 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. This text also demo that it is possible to do a roundtrip between some concrete data structures and the above abstract prover grammar; this is very subtle. The concrete application of these datatypes is the computation with the addition function of two variables that 1+2=3 via 3 different methods: the natural numbers category via intrinsic types, the natural numbers object via adjunctions/product/exponential, and the category of finite sets/numbers via coproducts/limits.  https://github.com/1337777/cartier/blob/master/cartierSolution13.lp  https://github.com/1337777/cartier/blob/master/cartierSolution14.lp

Outline:

• Categories, functors, profunctors, hom-arrows, transformations.
• Composition is Yoneda “lemma”.
• Outer cut-elimination or functorial lambda calculus.
• Inner cut-elimination or decidable adjunctions.
• Synthetic fibred Yoneda.
• Substructural fibred Yoneda.
• Comma elimination (“J-rule arrow induction”).
• Cut-elimination for fibred arrows.
• Pi-category-of-fibred-functors and Sigma-category.
• And why profunctors (of sets)?
• What is a fibred profunctor anyway?
• Higher inductive types, the interval type, concrete categories.
• Universe, universal fibration.
• Weighted limits.
• Duality Op, covariance vs contravariance.
• Grammatical topology.
• Applications: datatypes or 1+2=3 via 3 methods: nat numbers category, nat numbers object and colimits of finite sets.
• References.
• Qualifier quiz before peer-review.

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] Applications: datatypes or 1+2=3 via 3 methods: natural numbers category via intrinsic types, natural numbers object via adjunctions, and category of finite sets/numbers via colimits:
https://github.com/1337777/cartier/blob/master/cartierSolution14.lp
[8] Pierre Cartier

File link:
https://anthroplogic.sharepoint.com/:w:/s/cycle1/EYkAAiTctHlKm2pLCICagNcBawLjQWesCmefUk8Xi9CPxw?e=J0BZfI&action=embedview