Introduction: Curry-Howard-Lambek correspondence. What would be a category of proofs? Core sequent calculus L: sequents A ⊢ B, rules (ax) and (cut). Intepretation ⟦_⟧ of L in a category. Kernel and image of ⟦_⟧. Cut reduction.
Adding a (endo)functor. Unary connective □ (modality), rule (□), categorical interpretation, cut reduction, axiom reduction.
Adding a (endo)bifunctor. Binary connective ⍟, rule (⍟), categorical interpretation, cut reduction, axiom reduction.
Units.
Sequent calculus IL: intuitionistic sequents A1,...,An ⊢ B, left and right rules (⍟L) and (⍟R).
Homework 5: due on October 24th.
Monoidal categories (MC). Definition and basic properties. Mac Lane's coherence theorem (admitted, proof of λ₁ = ρ₁).
Left and right rules (1L) and (1R). Categorical interpretation ⟦_⟧ of IL in monoidal categories.
Derivable and admissible rules. Axiom expansion.
Invariance of ⟦_⟧ under axiom expansion. Image of ⟦_⟧. Cartesian categories are monoidal.
Cut elimination for IL. Sub-formula property.
Commutation: exchange rule. Symmetric monoidal categories (SMC). Cut elimination. Cartesian categories are symmetric monoidal.
Homework 6: due on November 7th.
Structural rules: contraction and weakening. Internal monoids and comonoids. Comonoid morphisms. Categories of comonoids are cartesian.
Implication. Symmetric monoidal closed categories (SMCC). Intuitionistic Multiplicative Linear Logic (IMLL).
Finite products. Additive connectives & and ⊤.
Finite coproducts. Additive connectives ⊕ and 0. Distributivity of ⊗ over ⊕. Intuitionistic Multiplicative Additive Linear Logic (IMALL).
Some provable properties in IMALL.
Modalities. Modal logic IK. Monoidal functors. Modal logic IS4. Monoidal comonads.
Structural rules restricted to !A as comonoid structures.
Categorical models of IMELL and ILL. Girard's translation vs coKleisli construction.