# 2nd part

## Lecture 11 (Jan. 9th)

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.
Intuitionistic sequents A1,...,An ⊢ B. Left and right rules (⍟L) and (⍟R). Derivable rule.

Homework 6: due on January 16th.

## Lecture 12 (Jan. 11th)

Sequent calculus `IL`: intuitionistic sequents A1,...,An ⊢ B, left and right rules (⊗L) and (⊗R).
Monoidal categories (MC). Definition and basic properties. Mac Lane's coherence theorem (admitted).
Left and right rules (1L) and (1R). Categorical interpretation ⟦_⟧ of `IL` in monoidal categories. Image of ⟦_⟧.

## Lecture 13 (Jan. 16th)

Admissible rule (≠ derivable). Cut elimination of `IL`. Sub-formula property.
Commutation: exchange rule. Symmetric monoidal categories (SMC).

Homework 7: due on January 23th.

## Lecture 14 (Jan. 18th)

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`).
Products and coproducts. Additive connectives &, ⊕, ⊤ and 0. Distributivity of ⊗ over ⊕. Intuitionistic Multiplicative Additive Linear Logic (`IMALL`).

## Lecture 15 (Jan. 23rd)

Some provable properties in `IMALL`. Cut elimination for additives.
Modalities. Modal logic `IK`. Monoidal functors and monoidal natural transformations. Modal logic `IS4`. Monoidal comonad.
Structural rules restricted to `!A` as comonoid structures.
Categorical models of `ILL`. Girard's translation vs coKleisli construction.