Abstracts.2020.STLCCC

Simply-Typed λ-Calculus and Cartesian Closed Categories

by Andreas Abel and Sandro Stucki

~~Two~~Three-part lecture series scheduled for Nov 5 and 12 and 19, 2020.

Recapitulation of simply-typed λ-calculus (STLC) with named bound variables, judgements Γ ⊢, ⊢ A, Γ ⊢ t : A, Γ ⊢ t = u : A, and function types A → B
Internalization of substitutions as terms by adding judgements Δ ⊢ σ : Γ, Δ ⊢ σ = τ : Γ and explicit substitutions Δ ⊢ t ∘ σ : A
Nameless representation of bound variables (de Bruijn style)
Reduction of de Bruijn indices n to weakenings 0 ∘ pⁿ of the first de Bruijn index 0 by adding substitutions Γ, A ⊢ p : Γ
Internalization of contexts as types by adding unit and product types 1 and A × B

Categories: Basic definition and structures of the algebra of functions
Cartesian closed categories (CCCs) 𝒞 with a choice of
- Terminal object 1 : 1 → 𝒞
- Binary products -×- : 𝒞 × 𝒞 → 𝒞
- Exponential/internal hom objects -^A : 𝒞 → 𝒞 for each A : 𝒞
Note that each of these three categorical structures can be defined as "the" right adjoint to a previously defined functor, and thus both by a universal property but also purely equationally.

In this part we plan to work out (some) of the following topics:

Prove the equivalence of the two definitions of Cartesian Closed Categories, CCC₁ with eval : B^A × A → B and CCC₂ with apply(t : C → B^A,u : C → A) : C → B (in Agda)
Prove the equivalence of the two definitions of a CCC with a strong monad, ML₁ with bind : M(A) × M(B)^A → M(B) and ML₂ with mu : M(M(A)) → M(A), M(t : A → B) : M(A) → M(B), tau : A × M(B) → M(A × B) (in Agda)
Prove that the collection of substitutions for any name-free substitution calculus (with or without explicit weakening) form a category, this category has finite products, and this category is equivalent to the category of types if the calculus has finite products (in Agda)
Do exercises from Andreas' ccc.pdf (2020 edition) (with pen on paper)
Read section 6.6 in Awodey's book (see literature below) and do exercise 14 (set-theoretic models of the theory of a reflexive domain) (with pen on paper)

Reading on this lecture:

Wikipedia, Curry-Howard-Lambek-Correspondence
Andreas Abel, Lambda-Kalkül, Kapitel 7 (7.0, 7.3, 7.4) und 9 (9.0, 9.1, 9.3, 9.4) (in German)
Jonathan Prieto-Cubides, The Simply Typed Lambda Calculus, slides: From named terms to de Bruijn terms; type-checking. Based on Agda code by gergoerdi
Steve Awodey, Category theory, Section 6.6
Joachim Lambek and Philip J. Scott, Introduction to higher order categorical logic

Further reading on categorical logic of typed λ-calculus: