Table of Contents

Abstract . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Sketch of the solution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 The “generic point” notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5 Functors and NTs in this notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 The proof of the (syntactic part) of the Yoneda Lemma in DNC . . . . . . . . . 7 The proof of the Yoneda Lemma in DNC (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 Adjunctions as DNC diagrams . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 Introduction to CC (1) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .10 Pre-terms and pre-judgements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Naive semantics: λ and Π . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 Introduction to CC (2) - example of a valid derivation . . . . . . . . . . . . . . . . . 13 The rules of the Calculus of Constructions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 Some facts (i.e., theorems) about CC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 More facts about CC: “classes” of terms, variations of the rules . . . . . . . . 16 From CC with minimal contexts to ND and back . . . . . . . . . . . . . . . . . . . . . . .17 From CC with minimal contexts to ND and back (2) . . . . . . . . . . . . . . . . . . . 18 Representing propositions and proofs in CC . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 Terms for equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 Protocategories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 A very special example: Set as a □∗-protocategory . . . . . . . . . . . . . . . . . . . . 22 A typical □∗-protocategory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 System DNC: rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 System DNC: (⇒ I), example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .25 System DNC: (→^{•} I), example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .26 Future work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 What comes before studying SN for DNC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Notes for people downloading these slides . . . . . . . . . . . . . . . . . . . . . . . .29

Don’t believe any idea here that you can’t figure out the details yourself, or you’ve seen it stated in serious articles written by grown-ups. These notes contain unintentional errors and omissions. Feedback is not only welcome but also desperately needed. Etc, Etc.

Eduardo Ochs

http://angg.twu.net/
http://www.mat.puc-rio.br/~edrx/
edrx@inx.com.br

Note: I’m currently at McGill university, as a visitor — I’m doing a “sandwich PhD” (really!) thanks to a CAPES (http://www.capes.gov.br/) grant...

Abstract

(For the FMCS talk)

We will present a logic (system DNC) whose terms represent categories, objects, morphisms, functors, natural transformations, sets, points, and functions, and whose rules of deduction represent certain constructive operations involving those entities. Derivation trees in this system only represent the “T-part” (for “terms” and “types”) of the constructions, not the “P-part” (“proofs” and “propositions”): the rules that generate functors and natural transformations do not check that they obey the necessary equations. So, we can see derivations in this system either as constructions happening in a “syntactical world”, that should be related to the “real world” in some way (maybe through metatheorems that are yet to be found), or as being just “skeletons” of the real constructions, with the P-parts having been omitted for briefness.

Even though derivations in DNC tell only half of the story, they still have a certain charm: DNC terms represent “types”, but a tree represents a construction of a lambda-calculus term; there’s a Curry-Howard isomorphism going on, and a tree can be a visual help for understanding how the lambda-calculus term works — how the data flows inside a given categorical construction. Also, if we are looking for a categorical entity of a certain “type” we can try to express it as a DNC term, and then look for a DNC “deduction” having it as its “conclusion”; the deduction will give us a T-part, and we will still have to go back to the standard language to supply a P-part, but at least the search has been broken in two parts...

The way to formalize DNC, and to provide a translation between terms in its “logic” and the usual notations for Category Theory, is based on the following idea. Take a derivation tree D in the Calculus of Constructions, and erase all the contexts and all the typings that appear in it; also erase all the deduction steps that now look redundant. Call the new tree D′. If the original derivation, D, obeys some mild conditions, then it is possible to reconstruct it — modulo exchanges and unessential weakenings in the contexts — from D′, that is much shorter. The algorithm that does the reconstruction generates as a by-product a “dictionary” that tells the type and the “minimal context” for each term that appears in D′; by extending the language that the dictionary can deal with we get a way to translate DNC terms and trees — and also, curiously, with a few tricks more, and with some minimal information to “bootstrap” the dictionary, categorical diagrams written in a DNC-like language.

Motivation A language for “skeletons of proofs” that would...

• let me write down just the essential — an (imaginary) computer would fill out the missing details;

• allow me say things like “the natural entity of type/name a, (a ↦ b) ↦ b” (ev);

• have a diagrammatic version,

• and a linear version (for derivation trees and Curry-Howard);

• easy to translate to the usual languages;

• be able to represent categorical concepts;

• allow for the “right amount” of ambiguity;

• read aloud as something that’s happening in the simplest models — e.g., in Set instead of in an arbitrary topos;

• be concise and clear enough — because I have a very bad memory and I tended to change my notations madly, so I needed short diagrams that would “say everything”, without the need for pages of definitions...

Sketch of the solution A notation that looks like an ambiguous λ-calculus (I call it the “generic point” notation); add some symbols to GP to let it represent functors, natural transformations, objects, categories, etc; a \underline{dictionary} will translate GP terms into something precise (in the Calculus of Constructions) (diagrams and derivation trees are recyclable! Just change the dictionary...) modify the Calculus of Constructions to get something that looks more like natural deduction — i.e., that has discharges instead of “… ⊢ … ”s — to get rid of some redundancy The system of natural deduction for categories (“system DNC”) is essentially this modified CC, with the GP notation with categorical extensions, and a dictionary. DNC derivations can either represent just the “T-part” (terms and types) of categorical constructions, and omit the “P-part” (propositions and proofs), or they can be complete.

The “generic point” notation What would be the natural name for a variable in...

A  −−→ a  A = E[a]
B  −−→ b  B = E[b]
A × B −−→ a, b  A × B = E[a, b] = E[a] × E[b]
B^{A} −−→ a ↦ b B^{A} = E[a ↦ b] = E[b]^{E[a]}

We will allow strange \underline{\underline{names}} for variables and terms and we will have a \underline{dictionary} to translate these names into something precise (in the Calculus of Constructions).

‘E’ is pronounced as “the space of”.

Functors and NTs in this notation Choose sets A and B, and a function B →^{g} A. In GP/DNC notation we write Hom(A, −) as x ⇒ (a ↦ x). Note that from the name “x ⇒ (a ↦ x)” we can extract both the action on objects, E[x] ↦ E[a ↦ x], and the action on morphisms, (x ↦ y) ↦ ((a ↦ x) ↦ (a ↦ y)).

[figure: y; (a ↦ y); x; y; x; (a ↦ x); (a ↦ x); (a ↦ y); Y; Hom(A, Y); X; Y; f; X; Hom(A, X); Hom(A, X); Hom(A, Y); Hom(A,f)]

x →^{•} ((b ↦ x) ↦ (a ↦ x)) is a natural transformation going from x ⇒ (b ↦ x) to x ⇒ (a ↦ x). It works as E[x] ↦ ((b ↦ x) ↦ (a ↦ x)), but it also obeys a naturality condition...

[figure: (b ↦ x); (a ↦ x); x; (b ↦ x); x; (a ↦ x); x; •; Hom(B, X); Hom(A, X); X; Hom(B, X); Hom(B,−); X; Hom(A, X); Hom(A,−); X]

2002fmcs (typeset 2002jun17 23:37) Edrx http://angg.twu.net/

The proof of the Yoneda Lemma in DNC

\begin{matrix}O[a] & [O[x]]^{1} \\ E[a ↦ x] \end{matrix} ^{Hom^{C}}

O[x] ↦ E[a ↦ x] 1

\begin{matrix}\begin{matrix}[a ↦ x′]^{1} & [x′ ↦ x′′]^{2} \\ a ↦ x′′ \end{matrix} ; (a ↦ x′) ↦ (a ↦ x′′) & 1 \\ x ⇒ (a ↦ x) \end{matrix} (⇒ I); 2

{O[a] \atop a ↦ a} O[a]

\begin{matrix}{O[a] \atop x ⇒ (a ↦ x)} ; O[x ⇒ (a ↦ x)] ren & O[x ⇒ x^{F}] \\ E[x →^{•} ((a ↦ x) ↦ x^{F})] \end{matrix} Hom^{Set^{C}}

x →^{•} ((a ↦ x) ↦ x^{F}) [s]^{1}

(a ↦ a) ↦ a^{F} a^{F}

(x →^{•} ((a ↦ x) ↦ x^{F})) ↦ a^{F} 1

\begin{aligned}O_{a} & {O[x ⇒ x^{F}] \atop x ⇒ x^{F}} ren \\ & E[a^{F}] \end{aligned} ; a^{F} ; ^{[s]^{3}} \begin{matrix}\begin{matrix}O_{a} & [O_{x}]^{2} \\ E[a ↦ x] \end{matrix} ; a ↦ x^{[s]^{1}} & {O[x ⇒ x^{F}] \atop x ⇒ x^{F}} ren \\ a^{F} ↦ x^{F} \end{matrix}

x^{F}

(a ↦ x) ↦ x^{F} 1

x →^{•} ((a ↦ x) ↦ x^{F}) 2

a^{F} ↦ (x →^{•} ((a ↦ x) ↦ x^{F})) 3

\begin{matrix}\begin{matrix}[O_{a}]^{1} & [O[x ⇒ x^{F}]]^{1} \\ a^{F} ↦ (x →^{•} ((a ↦ x) ↦ x^{F})) \end{matrix} & \begin{matrix}[O_{a}]^{1} & [O[x ⇒ x^{F}]]^{1} \\ (x →^{•} ((a ↦ x) ↦ x^{F})) ↦ a^{F} \end{matrix} \\ a^{F} ↔ (x →^{•} ((a ↦ x) ↦ x^{F})) \end{matrix} ; (a; x ⇒ x^{F}) →^{•} (a^{F} ↔ (x →^{•} ((a ↦ x) ↦ x^{F}))) ; 1

2002fmcs (typeset 2002jun17 23:37) Edrx http://angg.twu.net/

The proof of the Yoneda Lemma in DNC (2) ...and if we want to prove that the functors implicit in the outer ‘→^{•}’ of (a; x ⇒ x^{F}) →^{•} (a^{F} ↔ (x →^{•} ((a → x) → x^{F}))) are really (proto!) functors, we need this:

\begin{aligned}[a′ ↦ a′′]^{1} & {[(x ⇒ x^{F′}) ↦ (x ⇒ x^{F′′})]^{1} \atop x →^{•} (x^{F′} ↦ x^{F′′})} ren \\ & a′^{F′} ↦ a′′^{F′′} \end{aligned} ; (a; x ⇒ x^{F}) ⇒ a^{F} ; 1

\begin{matrix}{[O_{a}]^{1} \atop x ⇒ (a ↦ x)} ; O[x ⇒ (a ↦ x)] ren & [O[x ⇒ x^{F}]]^{1} \\ E[x →^{•} ((a ↦ x) ↦ x^{F})] \end{matrix} Hom^{Set^{C}}

O[a; x ⇒ x^{F}] ↦ E[x →^{•} ((a ↦ x) ↦ x^{F})] 1

\begin{matrix}\begin{aligned}\begin{matrix}[a′ ↦ a′′]^{4} & [a′′ ↦ x]^{1} \\ a′ ↦ x \end{matrix} & \begin{aligned}[O_{x}]^{2} & [x →^{•} ((a′ ↦ x) ↦ x^{F′})]^{3} \\ & (a′ ↦ x) ↦ x^{F′} \end{aligned} \\ & x^{F′} \end{aligned} & \begin{aligned}[O_{x}]^{2} & [x →^{•} (x^{F′} ↦ x^{F′′})]^{4} \\ & x^{F′} ↦ x^{F′′} \end{aligned} \\ x^{F′′} \end{matrix} ; (a′′ ↦ x) ↦ x^{F′′} ; 1 ; x →^{•} ((a′′ ↦ x) ↦ x^{F′′}) ; (→^{•} I); 2 ; (x →^{•} ((a′ ↦ x) ↦ x^{F′})) ↦ (x →^{•} ((a′′ ↦ x) ↦ x^{F′′})) ; 3 ; (a; x ⇒ x^{F}) ⇒ (x →^{•} ((a ↦ x) ↦ x^{F})) ; (⇒ I); 4

2002fmcs (typeset 2002jun17 23:37) Edrx http://angg.twu.net/

Adjunctions as DNC diagrams

L ⊣ R is (a; b) →^{•} ((a^{L} ↦ b) ↔ (a ↦ b^{R}))

(−) × B ⊣ (−)^{B} is (a; c) →^{•} ((a, b ↦ c) ↔ (a ↦ (b ↦ c)))

[figure: b; b^{R}; R; a^{L}; b; a^{L}; a; L; a; b^{R}; c; b ↦ c; (−)^{B}; a, b; c; a, b; a; (−)×B; a; b ↦ c]

The functor from Sub(A) to Sub(A × B) (A, B sets, for example) has a left adjoint ∃ and a right adjoin ∀. The weakening functor induced by Γ, a ↦ Γ in a “good” codomain fibration has a left adjoint Σ and a right adjoint Π.

[figure: a|_{Q(a)}; (a, b)|_{Q(a)}; a|_{∃b.P (a,b)}; a|_{Q(a)}; a|_{∃b.P (a,b)}; (a, b)|_{P (a,b)}; ∃; (a, b)|_{P (a,b)}; (a, b)|_{Q(a)}; a|_{∀b.R(a,b)}; (a, b)|_{R(a,b)}; ∀; a|_{Q(a)}; a|_{∀b.R(a,b)}; a|_{Q(a)}; (a, b)|_{Q(a)}; a|_{Q(a)}; (a, b)|_{Q(a)}; (a, b)|_{Q(a)}; (a, b)|_{R(a,b)}; ^{(\begin{matrix}Γ, q \\ ↓ \\ Γ \end{matrix})}; ^{(\begin{matrix}Γ, a, q \\ ↓ \\ Γ, a \end{matrix})}; ^{(\begin{matrix}Γ, a, p \\ ↓ \\ Γ \end{matrix})}; ^{(\begin{matrix}Γ, q \\ ↓ \\ Γ \end{matrix})}; ^{(\begin{matrix}Γ, a, p \\ ↓ \\ Γ \end{matrix})}; ^{(\begin{matrix}Γ, a, p \\ ↓ \\ Γ, a \end{matrix})}; Σ; ^{(\begin{matrix}Γ, a, p \\ ↓ \\ Γ, a \end{matrix})}; ^{(\begin{matrix}Γ, a, q \\ ↓ \\ Γ, a \end{matrix})}; (\begin{matrix}Γ, (a ↦ r) \\ ↓ \\ Γ \end{matrix}); (\begin{matrix}Γ, a, r \\ ↓ \\ Γ, a \end{matrix}); Π; ^{(\begin{matrix}Γ, q \\ ↓ \\ Γ \end{matrix})}; (\begin{matrix}Γ, (a ↦ r) \\ ↓ \\ Γ \end{matrix}); ^{(\begin{matrix}Γ, q \\ ↓ \\ Γ \end{matrix})}; ^{(\begin{matrix}Γ, a, q \\ ↓ \\ Γ, a \end{matrix})}; ^{(\begin{matrix}Γ, q \\ ↓ \\ Γ \end{matrix})}; ^{(\begin{matrix}Γ, a, q \\ ↓ \\ Γ, a \end{matrix})}; ^{(\begin{matrix}Γ, a, q \\ ↓ \\ Γ, a \end{matrix})}; (\begin{matrix}Γ, a, r \\ ↓ \\ Γ, a \end{matrix})]

Introduction to the Calculus of Constructions (1) CC is a particular case of a pure type system. A PTS has a set of sorts (for CC, {∗, □}), a set of axioms involving sorts (for CC, {⊢ ∗:□}), and a set of pairs of sorts (for CC, {(∗, ∗), (∗, □), (□, ∗), (□, □)}) that specify which variations of the derivation rules are valid. We also need a countable set of variables — e.g. {a, b, c, …, A, B, C, … }. From that we define pre-terms, pre-judgements and (valid) derivations. Terms and judgements are pre-terms and pre-judgements that can appear in valid derivations.

Pre-terms and pre-judgements The set of pre-terms is the least set closed under the following rules:

• sorts are pre-terms

• variables are pre-terms If v is a variable, f, t, t′ pre-terms,

• ft is a pre-term (application)

• λv:t.t′ is a pre-term (abstraction, function)

• Πv:t.t′ is a pre-term (function space) Examples of (pre-)terms: λA: ∗ .λa:A.a (polymorphic identity) λI: ∗ .λA:(Πi:I.∗).(Πi:I.Ai) A pre-judgement is something like x_{1}:A_{1}, …, x_{n}:A_{n} ⊢ t:t′ where x_{1}, …, x_{n} \underline{are all distinct} and A_{1}, …, A_{n}, t, t′ are pre-terms. n can be 0 (“empty context”).

Naive semantics: λ and Π The λ of CC is like the usual λ of λ-calculus, but with a restriction on the type of the input. (λa:A.b)a′ will only be a (valid) term if a′:A. The Π forms function spaces: If b : B then (λa:A.b):(Πa:A.B). Dependent types: in λa:A.b and Πa:A.B, with b:B, B can be a term involving a! fa′ will only be a (valid) term if f and a′ can be typed as f:(Πa:A.B) and a′:A.

Naive semantics for ‘Π’: example: if I = {1, 2, 3}, then Πi:I.A_{i} = ∏_{i∈I} A_{i} = = {{(1, a_{1}), (2, a_{2}), (3, a_{3})} | a_{1} ∈ A_{1}, a_{2} ∈ A_{2}, a_{3} ∈ A_{3}} ≅ A_{1} × A_{2} × A_{3} Introduction to CC (2) - example of a valid derivation

{⊢ ∗:□ \atop X:∗ ⊢ X:∗} s_{□} \begin{matrix}⊢ ∗:□ & ⊢ ∗:□ \\ X:∗ ⊢ ∗:□ \end{matrix} ^{weak^{□}} {⊢ ∗:□ \atop X:∗ ⊢ X:∗} s_{□} X:∗, x:X ⊢ ∗:□ weak^{∗}

X:∗ ⊢ (Πx:X.∗):□ Π^{∗□}

X:∗, F:(Πx:X.∗) ⊢ F:(Πx:X.∗) s^{□}

A tree of (pre-)judgements The leaves are axioms The root is the conclusion The bars are applications of the rules (coming soon!) Most of the tree is “bureaucracy” (weakings, for example)

\underbrace{x_{1} \overbrace{:A_{1}}^{typing}, …, x_{n} \overbrace{:A_{n}}^{typing} ⊢}_{context} t \overbrace{:T}^{typing}

The terms are the pre-terms that can appear as ‘x_{i}’s, ‘A_{i}’s, t or T.

The rules of the Calculus of Constructions Rules of the system: ax, s, Π, λ, app, weak, conv (conv is not shown; if a:A and A =_{β} A′ then a:A′)

\begin{matrix}Γ ⊢ A:R & Γ, a:A ⊢ B:S \\ Γ ⊢ (Πa:A.B):S \end{matrix} Π_{RS}  ⊢ ∗:□ ax
\begin{matrix}Γ, a:A ⊢ b:B & Γ ⊢ (Πa:A.B):S \\ Γ ⊢ (λa:A.b):(Πa:A.B) \end{matrix} λ_{RS}  {Γ ⊢ A:R \atop Γ, a:A ⊢ a:A} s_{R}
\begin{matrix}Γ ⊢ f:(Πa:A.B) & Γ ⊢ a′:A \\ Γ ⊢ fa′:B[a := a′] \end{matrix} ^{app^{RS}}  \begin{matrix}Γ, Δ ⊢ c:C & Γ ⊢ A:R \\ Γ, a:A, Δ ⊢ c:C \end{matrix} ^{weak^{R}}

R, S sorts; a variable; Γ, Δ contexts All other letters (a′, A, b, B, c, C, f) represent terms (Remember: even in a pre-judgement we can’t have repeated declarations for the same variable)

Some facts (i.e., theorems) about CC Each term of CC is either a sort, or a member of a sort, or a member of a member or a sort. Each variable is a member of a member of a sort. If x_{1}:A_{1}, …, x_{n}:A_{n} ⊢ t:T then the list x_{1}, …, x_{n} contains all the free variables of t and T; there exist sorts S_{1}, …, S_{n} such that ⊢ A_{1}:S_{1}, x_{1}:A_{1} ⊢ A_{2}:S_{2}, x_{1}:A_{1}, x_{2}:A_{2} ⊢ A_{3}:S_{3}, …, and if T is not a sort then there exists a sort S s.t.: x_{1}:A_{1}, …, x_{n}:A_{n} ⊢ T:S. Reading a pre-judgement aloud Examples: ⊢ (λA: ∗ .λa:A.a):(ΠA: ∗ .Πa:A.A) I:∗, A:(Πi:I.∗) ⊢ (Πi:I.Ai):∗ More facts about CC: “classes” of terms, variations of the rules If we know the “class” of each variable we know the class of every term: (λa^{R-2}:A^{R-1}.b^{S-2})^{S-2} (f^{S-2}a^{R-2})^{S-2} (Πa^{R-2}:A^{R-1}.B^{S-1})^{S-1}

operator : kind : □
element :  set  : ∗
a, a′  :  A  :  ∗  Π_{∗∗},
b, fa′  :  B  :  ∗  λ_{∗∗},
f, (λa:A.b) : (Πa:A.B) :  ∗  app_{∗∗}
a, a′  :  A  : □  Π_{□∗},
b, fa′  :  B  :  ∗  λ_{□∗},
f, (λa:A.b) : (Πa:A.B) :  ∗  app_{□∗}
a, a′  :  A  :  ∗  Π_{∗□},
b, fa′  :  B  : □  λ_{∗□},
f, (λa:A.b) : (Πa:A.B) : □  app_{∗□}
a, a′  :  A  : □  Π_{□□},
b, fa′  :  B  : □  λ_{□□},
f, (λa:A.b) : (Πa:A.B) : □  app_{□□}

From CC with minimal contexts to ND and back Definition: a “good” derivation tree is one in which:

• each variable appears always with the same type

• whenever there are two subtrees “deriving the same term”, they are equal

Take a good tree with minimal contexts, for example,

{⊢ ∗:□ \atop I:∗ ⊢ I:∗} s_{□}

\begin{matrix}\begin{matrix}{⊢ ∗:□ \atop I:∗ ⊢ I:∗} [s_{□}]^{C2} & ⊢ ∗:□ \\ I:∗ ⊢ (Πi:I.∗):□ \end{matrix} & Π_{∗□} \\ I:∗, A:(Πi:I.∗) ⊢ A:(Πi:I.∗) \end{matrix} ; s_{□} \begin{matrix}{⊢ ∗:□ \atop I:∗ ⊢ I:∗} & [s_{□}]^{C1} \\ I:∗, i:I ⊢ i:I \end{matrix} ; [s_{∗}]^{2}

I:∗, A:(Πi:I.∗), i:I ⊢ Ai:∗ app^{∗□}; 1

I:∗, A:(Πi:I.∗) ⊢ (Πi:I.Ai):∗ Π^{∗∗}; 2

I:∗, A:(Πi:I.∗), f:(Πi:I.Ai) ⊢ f:(Πi:I.Ai) s^{∗}

erase its contexts, and put in the dictionary all the remaining typings:

{∗:□ \atop I:∗} s_{□} \begin{matrix}\begin{matrix}{∗:□ \atop I:∗} [s_{□}]^{C2} & ∗:□ \\ (Πi:I.∗):□ \end{matrix} & Π_{∗□} \\ A:(Πi:I.∗) \end{matrix} ; s_{□} \begin{matrix}{∗:□ \atop I:∗} & [s_{□}]^{C1} \\ i:I \end{matrix} ; [s_{∗}]^{2} Ai:∗ app^{∗□}; 1

(Πi:I.Ai):∗ Π^{∗∗}; 2

f:(Πi:I.Ai) s^{∗}

Dictionary: i : I : ∗ A : (Πi:I.∗) : □ Ai : ∗ f : (Πi:I.Ai) : ∗ From CC with minimal contexts to ND and back (2) ...now erase the typings too:

2002fmcs (typeset 2002jun17 23:37) Edrx http://angg.twu.net/

{∗ \atop I} s_{□} \begin{matrix}\begin{matrix}{∗ \atop I} [s_{□}]^{C2} & ∗ \\ Πi:I.∗ \end{matrix} & Π_{∗□} \\ A \end{matrix} ; s_{□} \begin{matrix}{∗ \atop I} & [s_{□}]^{C1} \\ i \end{matrix} ; [s_{∗}]^{2} Ai app^{∗□}; 1

Πi:I.Ai Π^{∗∗}; 2

f s^{∗}

Dictionary: i : I : ∗ A : (Πi:I.∗) : □ Ai : ∗ f : (Πi:I.Ai) : ∗

Fact: it is possible to reconstruct the original tree from this one. New variables are introduced only at the “s” rules. To help keep track of what’s happening, we mark discharges with ‘[·]^{n}’s and “contractions” with ‘[·]^{Cn}’s.

It is also possible to discard the dictionary and reconstruct it just from that last tree.

Next step (not shown): replace the terms in a tree with names for them in the GP notation; let the dictionary translate some terms as applications — example, b −−→ (a ↦ b)(a).

Representing propositions and proofs in CC Props is a sort; in CC, Props = ∗ (in other PTSs we may have Props ≠ ∗ and we may be able to formalize irrelevance of proofs)

prop[P] is P seen as a proposition. Naively, prop[P] is the set of proofs of P. prf[P] : prop[P] : Props (= ∗)

Dictionary:

prop[P [figure]Q] −−→ (Πprf[P]:prop[P].prop[Q])
prf[P [figure]Q] −−→ (prf[P] ↦ prf[Q])
prop[∀x.P (x)] −−→ (Πx:E[x].prop[P (x)])
prf[∀x.P (x)] −−→ (x ↦ prf[P (x)])

Terms for equality To speak “internally” about equality between members of the same set we need a package of terms, that will be added to contexts...

equality_{∗} is a package consisting of:

eq_{∗}  (eq_{∗}Aaa′) : Props
prop[a = a′] −−→ eq_{∗}Aaa′
refl_{∗} (refl_{∗}Aa) : prop[a = a]
prf[a = a] −−→ refl_{∗}Aa
sim_{∗} (sim_{∗}Aaa′) : prop[a = a′ [figure]a′ = a]
prf[a = a′ [figure]a′ = a] −−→ (sim_{∗}Aaa′)
trans_{∗} (trans_{∗}Aaa′a′′) : prop[a = a′ [figure](a′ = a′′ [figure]a = a′′)]

prf[a = a′ [figure](a′ = a′′ [figure]a = a′′)] −−→ (trans_{∗}Aaa′a′′)

f′s.r.equality_{∗∗} is a package of terms saying that all functions f:(Πa:A.B) “respect equality”. This is a bit trickier, as it involves the “conv” rule.

Note: a, a′, a′′:A:∗, B:∗ Protocategories The prefix “proto” will always mean “without the terms for equalities”. A protocategory C : Protocats_{SR} (where S, R are sorts — typically S = □, R = ∗) is a package containing

Objs_{C} : S
Hom_{C}  Hom_{C} AB : R
id_{C}  id_{C}A : Hom_{C} AA
∘_{C}  ∘_{C}ABC(a ↦ b)(b ↦ c) : Hom_{C} AC

(A, B, C : Objs_{C})

Notational trick: a ↦ b : E[a ↦ b], and the dictionary translates E[a ↦ b] −−→ Hom_{C} AB.

A protocategory comes without the ‘prf’ terms that say the ∘_{C} behaves well. A category is a protocategory plus such terms.

A very special example: Set as a □∗-protocategory Set : Protocats_{□∗} Objs_{Set} = ∗ : □ Hom_{Set} E[x]E[y] = E[x ↦ y] : ∗ Hom_{Set} := λX: ∗ .λY: ∗ .(Πx:X.Y) id_{Set}E[x] = x ↦ x id_{Set} := λX: ∗ .λx:X.x ∘_{Set}E[x]E[y]E[z](x ↦ y)(y ↦ z) = (y ↦ z) ∘ (x ↦ y) ∘_{Set} := λX: ∗ .λY: ∗ .λZ: ∗ .

λf:(Hom_{Set} XY).λg:(Hom_{Set} Y Z).

λx:X.g(fx)

A typical □∗-protocategory Objs_{C} : □ Hom_{C} : ΠO[a]:Objs_{C}.ΠO[b]:Objs_{C}.∗ O[a], O[b], O[c] : Objs_{C} like E[x], E[y], E[z] : Objs_{Set} = ∗ but \underline{we don’t have a semantics} for “a”, “b”, “c”!!! Just for O[a], O[b], O[c], (a ↦ b), (b ↦ c), (a ↦ c).

[figure: x; y; x; z; y; z; a; b; a; c; b; c]

in Set in C

New “operator” in the dictionary: Cat — Cat[x] −−→ Set, Cat[a] −−→ C (O[a]:Objs_{C})

x ↦ y : E[x ↦ y] = E[x] → E[y] a ↦ b : E[a ↦ b] = Hom_{C} O[a]O[b] System DNC: rules

\begin{matrix}O[a] & a ⇒ a^{F} \\ O[a^{F}] \end{matrix} (⇒ E_{O})  \begin{matrix}a′ ↦ a′′ & a ⇒ a^{F} \\ a′^{F} ↦ a′′^{F} \end{matrix} (⇒ E_{M})
\begin{aligned}O[a] & a →^{•} (a^{F} ↦ a^{G}) \\ & a^{F} ↦ a^{G} \end{aligned} (→^{•} E)

Several “ren” rules, e.g.,

{a ⇒ a^{F} \atop O[a ⇒ a^{F}]} ren  {a →^{•} (a^{F} ↦ a^{G}) \atop (a ⇒ a^{F}) ↦ (a ⇒ a^{G})} ren

Discharges are written in usual ND style:

\begin{matrix}Objs & C \\ O[a] \end{matrix} [s]^{1} … O[a^{F}] O[a] ↦ O[a^{F}] 1 ⇝ \begin{matrix}[O[a]]^{1} & … \\ O[a^{F}] \end{matrix} ; O[a] ↦ O[a^{F}] 1

but then we need to know that O[a]:Objs_{C} (dictionary!) and the trees may split into several...

System DNC: (⇒ I), example If we know the action of x ⇒ (a ↦ x) on objects, i.e.,

\begin{matrix}E[a] & {[O[x]]^{1} \atop E[x]} ren \\ E[a ↦ x] \end{matrix} O[a ↦ x] ren

O[x] ↦ O[a ↦ x] 1

then:

\begin{matrix}\begin{matrix}\begin{matrix}[a ↦ x′]^{1} & [x′ ↦ x′′]^{2} \\ a ↦ x′′ \end{matrix} ; (a ↦ x′) ↦ (a ↦ x′′) & 1 \\ (x′ ↦ x′′) ↦ ((a ↦ x′) ↦ (a ↦ x′′)) \end{matrix} & 2 \\ x ⇒ (a ↦ x) \end{matrix} ; “(⇒ I)”

Note that we are constructing a \underline{proto}-functor — we are leaving out the “prf” terms!

System DNC: (→^{•} I), example If we know x ⇒ (b ↦ x) and x ⇒ (a ↦ x), then the rule for creating

x →^{•} ((b ↦ x) ↦ (a ↦ x))

is essentially the same as the rule for creating O[x] ↦ ((b ↦ x) ↦ (a ↦ x))

— again, we leave out the “prf” terms, and we only build a \underline{proto}-natural transformation. Example:

\begin{matrix}\begin{matrix}a ↦ b & [b ↦ x]^{1} \\ a ↦ x \end{matrix} ; (b ↦ x) ↦ (a ↦ x) & 1 \\ x →^{•} ((b ↦ x) ↦ (a ↦ x)) \end{matrix} 2  \begin{aligned}a ↦ b & \begin{matrix}O[b] & [O[x]]^{2} \\ E[b ↦ x] \end{matrix} ; b ↦ x ; ^{[s]^{1}} \\ & a ↦ x \end{aligned} ; (b ↦ x) ↦ (a ↦ x) ; 1 ; x →^{•} ((b ↦ x) ↦ (a ↦ x)) ; 2

Future work Is DNC strongly normalizing? Problems with this question:

• Right now DNC is just a layer of syntax on top of CC

• We need to formalize better how the dictionary works

• Some rules (e.g. (⇒ E)) involve a certain amount of pattern-matching • Reductions (cut-elimination) may require non-trivial renamings

• Which names are valid? DNC terms are inherently ambiguous... DNC is not well-defined enough yet!!

What comes before studying SN for DNC We need to learn more about DNC’s ambiguities: If a DNC term α has a natural construction,

• is it essentially unique?

• does it lift from the “syntactical world” to the “real world”?

• coherence/parametricity Missing: rules for defining new categories DNC and GP are tools for expressing the (intuitive) skeletons of some proofs (more precisely, the T-parts of proofs). So, morally, we should be able to represent nicely in GP/DNC:

• SN proofs for CC

• Categorical models for CC and other type theories

• “Basic category theory” (everything that a categorist would say is trivial)

• A lot about fibrations

• And also:

– Topos logic (and a ND for it!)

– Terms involving infinitesimals and derivatives (my original motivation, years ago)

Notes for people downloading these slides In a very near future (before the end of June, I hope) I’m going to add notes about how I handwaved over these slides in the presentation, and, even more important, how to “pronounce” the DNC terms and diagrams... and also pointers to the literature, thanks to the people that discussed these ideas with me and helped me shape the presentation (Robert Seely, Jeff Egger, Robin Cockett), and a few other things. Now I have to hurry up and prepare the slides for my presentation at the CMS 2002, in Quebec city... it’s going to be only 15 mins long (this one was 45 mins) so I’ll have to use a different approach, with more motivation and less details... So: please check http://angg.twu.net/ again in a few weeks for a new version of this. Sorry for the mess! Edrx, 2002jun13