Table of Contents

Abstract . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 The “generic point” notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3 Functors and NTs in this notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 What is a functor? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5 Toy example: G ∘ F . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 Why DNC? Two conjectures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 Adjunctions as DNC diagrams . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 The proof of the (syntactic part) of the Yoneda Lemma in DNC . . . . . . . . . 9 The proof of the Yoneda Lemma in DNC (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 A crash course on the Calculus of Constructions . . . . . . . . . . . . . . . . . . . . . . . 11 A crash course on CC: (pre-)judgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 A crash course on CC: propositions and proofs . . . . . . . . . . . . . . . . . . . . . . . . . 18 A crash course on CC: the rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13 Fact: (abbreviated CC + dictionary) formalizes DNC . . . . . . . . . . . . . . . . . . 14 Fact: (abbreviated CC + dictionary) formalizes DNC (2) . . . . . . . . . . . . . . 15 Protocategories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 Protocategories: “O”, “Cat”, “↦” as morphism . . . . . . . . . . . . . . . . . . . . . . . 17

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.

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]

2002cms (typeset 2002jun17 23:33) Edrx http://angg.twu.net/

What is a functor? A functor F : A → B is a package containing:

F_{O} F_{O}A : Objs_{B}
F_{M} F_{M}A′A′′(A′ →^{f} A′′) : Hom_{B}(F_{O}(A′), F_{O}(A′′))

F_{M}A′A′′(A′ →^{f} A′′) = (F_{O}(A′) →^{F (f)} F_{O}(A′′))

and two “proofs”:

• that F respects composition, F_{M}(k ∘ h) = F_{M}(k) ∘ F_{M}(h)

• that F respects identities, F_{M}(id_{A}) = id_{F_{O}(A)}.

A \underline{proto}-functor only has F_{O} and F_{M}. The prefix “\underline{proto}” will always mean “without the terms for equalities”.

A category A is a package containing:

Objs_{A}
Hom_{A} Hom_{A} A′A′′
id_{A}  id_{A}A : Hom_{A} AA
∘_{A}  ∘_{A}A′A′′A′′′(A′ →^{h} A′′)(A′′ →^{k} A′′′) : Hom_{A} A′A′′′

plus three “proofs” that say that ∘_{A} is associative and respects id_{A}. A \underline{proto}-category only has Objs_{A}, Hom_{A}, id_{A}, ∘_{A}, Toy example: G ∘ F

\begin{matrix}\begin{matrix}[O[a]]^{1} & a ⇒ a^{F} \\ O[a^{F}] \end{matrix} & b ⇒ b^{G} \\ O[a^{F G}] \end{matrix} ; O[a] ↦ O[a^{F G}] ; 1  \begin{matrix}\begin{matrix}[A]^{1} & F \\ F (A) \end{matrix} & G \\ G(F (A)) \end{matrix} ; λA.G(F (A)) 1
\begin{matrix}\begin{matrix}[O[a]]^{1} & a ⇒ a^{F} \\ (a ⇒ a^{F})(O[a^{F}]) \end{matrix} & b ⇒ b^{G} \\ (b ⇒ b^{G})((a ⇒ a^{F})(O[a^{F}])) \end{matrix} ; λO[a].(b ⇒ b^{G})((a ⇒ a^{F})(O[a^{F}])) 1

(a ⇒ a^{F} G)_{O} := λO[a]:Objs_{A}.(b ⇒ b^{G})_{O}((a ⇒ a^{F})_{O}(O[a^{F}]))

\begin{matrix}\begin{matrix}[a′ ↦ a′′]^{1} & a ⇒ a^{F} \\ a′^{F} ↦ a′′^{F} \end{matrix} & b ⇒ b^{G} \\ a′^{F G} ↦ a′′^{F G} \end{matrix} ; a ⇒ a^{F G} ; (⇒ E); 1  \begin{matrix}\begin{matrix}h & F \\ F (h) \end{matrix} & G \\ G(F (h)) \end{matrix} ; λh.G(F (h))
\begin{matrix}\begin{matrix}[a′ ↦ a′′]^{1} & a ⇒ a^{F} \\ (a ⇒ a^{F})(a′ ↦ a′′) \end{matrix} & b ⇒ b^{G} \\ (b ⇒ b^{G})((a ⇒ a^{F})(a′ ↦ a′′)) \end{matrix} ; λ(a′ ↦ a′′).(b ⇒ b^{G})((a ⇒ a^{F})(a′ ↦ a′′)) 1

F_{M} := λO[a′]:Objs_{A}.λO[a′′]:Objs_{A}.

λ(a′ ↦ a′′):(Hom_{A} O[a′]O[a′′]).

(b ⇒ b^{G})_{M}((a ⇒ a^{F})_{O}O[a′])((a ⇒ a^{F})_{O}O[a′′]) ((a ⇒ a^{F})_{M}O[a′]O[a′′](a′ ↦ a′′))

\begin{matrix}\begin{matrix}\begin{matrix}a′ ↦ a′′ & a ⇒ a^{F} \\ a′^{F} ↦ a′′^{F} \end{matrix} & b ⇒ b^{G} \\ a′^{F G} ↦ a′′^{F G} \end{matrix} & \begin{matrix}\begin{matrix}a′′ ↦ a′′′ & a ⇒ a^{F} \\ a′′^{F} ↦ a′′′^{F} \end{matrix} & b ⇒ b^{G} \\ a′′^{F G} ↦ a′′′^{F G} \end{matrix} \\ a′^{F G} ↦ a′′′^{F G} \end{matrix}  \begin{matrix}\begin{matrix}\begin{matrix}h & F \\ F (h) \end{matrix} & G \\ G(F (h)) \end{matrix} & \begin{matrix}\begin{matrix}k & F \\ F (k) \end{matrix} & G \\ G(F (k)) \end{matrix} \\ G(F (k)) ∘ G(F (h)) \end{matrix}

\begin{matrix}\begin{matrix}\begin{matrix}a′ ↦ a′′ & a′′ ↦ a′′′ \\ a′ ↦ a′′′ \end{matrix} & a ⇒ a^{F} \\ a′^{F} ↦ a′′′^{F} \end{matrix} & b ⇒ b^{G} \\ a′^{F G} ↦ a′′′^{F G} \end{matrix}  \begin{matrix}\begin{matrix}\begin{matrix}h & k \\ k ∘ h \end{matrix} & F \\ F (k ∘ h) \end{matrix} & G \\ G(F (k ∘ h)) \end{matrix}

2002cms (typeset 2002jun17 23:33) Edrx http://angg.twu.net/

Why DNC? Two conjectures

(name → derivation → λ-term...)

Conjecture 1: the naturality conditions do come for free. Take a name for a functor — say, a ⇒ a^{F G}, with hyps. a ⇒ a^{F} and b ⇒ b^{G} — and a natural construction for a (proto) entity with that name. Then that construction can be lifted from the syntactical world to the real world — i.e., we can “prove” the missing “prf” terms.

Conjecture 2: given a name, we can effective obtain the natural entity with that name, or prove that it doesn’t exist, or that it exists but is not unique. That is, we have an algorithm for proof-search that does that; and maybe also some purely syntactical criteria that can say “no natural entity with that name can exist” or “there will be non-equivalent constructions”.

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})]

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

2002cms (typeset 2002jun17 23:33) 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

2002cms (typeset 2002jun17 23:33) Edrx http://angg.twu.net/

A crash course on the Calculus of Constructions A countable set of variables, e.g. {a, b, c, …, A, B, C, … }. Sorts: ∗, □. Axioms on sorts: ⊢ ∗:□. 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.

Example of a term, with a typing: (λX: ∗ .x:X.x):(ΠX: ∗ .Πx:X.X) (the polymorphic identity)

“λa:A.b”:

λ a function that expects a value
a for the variable a
:A (it must be a member of A)
.b and returns b

“Πa:A.B”:

Π the space of the functions that expect
a:A “a”s (members of A)
B and return for each one a member of B

We can have dependent types! See the example above.

A crash course on CC: (pre-)judgments “x_{1}:A_{1}, x_{2}:A_{2}, …, x_{n}:A_{n} ⊢ t:T ”: If we have chosen a value for x_{1} (a member of A_{1}), a value for x_{2} (a member of A_{2}), etc, then we know the value of t (a member of T).

Fact: “x_{1}:A_{1}(:S_{1}), …, x_{n}:A_{n}(:S_{n}) ⊢ t:T ”: Every variable is two levels below a sort. Every term is either a sort, or one or two levels below a sort.

operator : kind : □
element :  set  : ∗

If we know the “class” of each variable we know the class of every term. Trick: (λ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}

The rules of CC have “variations” for operating on different levels:

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_{□□}

A crash course on CC: the rules 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. A derivation in CC:

{⊢ ∗:□ \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^{□}

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} Fact: (abbreviated CC + dictionary) formalizes DNC 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) : ∗

...now erase the typings too:

{∗ \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. It is also possible to discard the dictionary and reconstruct it just from that last tree.

Fact: (abbreviated CC + dictionary) formalizes DNC (2)

{∗ \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) : ∗

Next step: 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).

{∗ \atop E[i]} s_{□}

\begin{matrix}\begin{matrix}{∗ \atop E[i]} [s_{□}]^{C2} & ∗ \\ E[i ↦ e∗] \end{matrix} & Π_{∗□} \\ i ↦ E[a_{i}] \end{matrix} ; s_{□} \begin{matrix}{∗ \atop E[i]} & [s_{□}]^{C1} \\ i \end{matrix} ; [s_{∗}]^{2}

E[a_{i}] app^{∗□}; 1

E[i ↦ a_{i}] Π^{∗∗}; 2

i ↦ a_{i} s^{∗}

Dictionary: i : E[i] : ∗ i ↦ E[a_{i}] : E[i ↦ e∗] : □

E[a_{i}] = (i ↦ E[a_{i}])(i) : ∗

i ↦ a_{i} : E[i ↦ a_{i}] : ∗

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.

We can split the tree at the “s” rules — “hypotheses” become entities obtained by “s” rules.

Protocategories (Again: the prefix “proto” always means “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 very special example: Set is a □∗-protocategory. Objs_{Set} = ∗ : □ Hom_{Set} := λX: ∗ .λY: ∗ .(Πx:X.Y) id_{Set} := λX: ∗ .λx:X.x ∘_{Set} := λX: ∗ .λY: ∗ .λZ: ∗ .

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

λx:X.g(fx)

Protocategories: “O”, “Cat”, “↦” as morphism 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] A crash course on CC: propositions and proofs prop[P] is P seen as a proposition. Naively, prop[P] is the set of proofs of P. prf[P] : prop[P] : ∗

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)])

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”.