Contents

1 Introduction 4 1.1 λ-calculus as a programming language . . . . . . . . . . . . . . . 4 1.2 Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.3 Real-world semantics . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.4 Skeletons of proofs . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.5 Category theory . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.6 What is “obvious”? . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.7 Why do we need category theory . . . . . . . . . . . . . . . . . . 5

2 System DNC: a system of natural deduction for categories 6 2.1 λC: The Calculus of Constructions . . . . . . . . . . . . . . . . . 6 2.2 A crash course on λC: (pre-)judgments . . . . . . . . . . . . . . . 7 2.3 A crash course on CC: the rules . . . . . . . . . . . . . . . . . . . 8 2.4 λC_{D}: λC in natural-deduction style . . . . . . . . . . . . . . . . . 9 2.5 λC_{D}: λC in natural-deduction style (2) . . . . . . . . . . . . . . 10 2.6 Subsystems of λC . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.7 Pure type systems . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.8 Logic in λC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

2.8.1 Prop as * . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.8.2 Irrelevance of proofs . . . . . . . . . . . . . . . . . . . . . 10 2.8.3 Leibniz Equality . . . . . . . . . . . . . . . . . . . . . . . 10 2.8.4 Subsets and subtypes . . . . . . . . . . . . . . . . . . . . 11 2.8.5 The calculus of constructions . . . . . . . . . . . . . . . . 11

2.9 DNC terms (and pseudoterms, and pseudopoints) . . . . . . . . . 11 2.10 Categories in λC . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.11 Encoding categories in λC . . . . . . . . . . . . . . . . . . . . . . 13

2.11.1 Protocategories, proto-NTs and other protothings …. 13 2.11.2 The rule (⇒I) . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.11.3 The syntactical world, the real world and the normaliza-

tion trick . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.11.4 A simple example: Hom . . . . . . . . . . . . . . . . . . . 14 2.11.5 A bigger example: the Yoneda lemma . . . . . . . . . . . 15 2.11.6 Typing the term of the Yoneda Lemma . . . . . . . . . . 16 2.11.7 Proving the Yoneda lemma syntactically . . . . . . . . . . 17

2.12 Basic categorical constructs . . . . . . . . . . . . . . . . . . . . . 19 2.12.1 Adjunctions . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.12.2 Limits . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.12.3 Cartesian-closed categories . . . . . . . . . . . . . . . . . 19 2.12.4 Toposes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.12.5 Fibrations . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.12.6 2-Categories . . . . . . . . . . . . . . . . . . . . . . . . . . 19

2.13 Some proofs in DNC . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.13.1 Cats and Fib_{I} are cartesian-closed . . . . . . . . . . . . . 19 2.13.2 Right adjoints preserve limits . . . . . . . . . . . . . . . . 19 2.13.3 Limits and colimits in ‘C^{I}’s can be calculated pointwise . 20 2.13.4 ‘Set^{I}’s are toposes . . . . . . . . . . . . . . . . . . . . . . 21 2.13.5 The fibred Yoneda lemma . . . . . . . . . . . . . . . . . . 26

3 Categorical models for type theories 27 3.1 The category of contexts . . . . . . . . . . . . . . . . . . . . . . . 27 3.2 Adjoints to substitution functors . . . . . . . . . . . . . . . . . . 27 3.3 Fibrations for F2 . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 3.4 Fibrations for P . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 3.5 Bifibrations and trifibrations . . . . . . . . . . . . . . . . . . . . 33 3.6 The Beck-Chevalley condition . . . . . . . . . . . . . . . . . . . . 34

4 A natural deduction system for topos logic 35

5 The syntactical world and the real world 35

6 Infinitesimals 35 6.1 Natural infinitesimals . . . . . . . . . . . . . . . . . . . . . . . . 35 6.2 The translation from SSA to standard . . . . . . . . . . . . . . . 36

6.2.1 The key theorem on natural infinitesimals . . . . . . . . . 36 6.2.2 An example of a calculation with infinitesimals . . . . . . 37 6.2.3 Another example: Hamiltonians . . . . . . . . . . . . . . 38

6.3 The Inverse Function Theorem and its friends . . . . . . . . . . . 38

7 Glossary 40 7.1 The notation of generic points and “spaces ofs” . . . . . . . . . . 40 7.2 Functors and natural transformations in Set . . . . . . . . . . . 40 7.3 Truth-values, witnesses, propositions, proofs . . . . . . . . . . . . 41 7.4 Connectives and quantifiers . . . . . . . . . . . . . . . . . . . . . 41 7.5 Categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 7.6 Functors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 7.7 Natural Transformations . . . . . . . . . . . . . . . . . . . . . . . 43 7.8 The opposite of a category . . . . . . . . . . . . . . . . . . . . . . 43 7.9 Categories of functors . . . . . . . . . . . . . . . . . . . . . . . . 43 7.10 The product of two categories . . . . . . . . . . . . . . . . . . . . 43 7.11 Hom and Yoneda . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 7.12 Adjunctions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 7.13 The “such that” bar and the “is well-defined” symbol . . . . . . 45 7.14 Arrow categories . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 7.15 Monics, subobjects and the classifier object . . . . . . . . . . . . 46 7.16 Fibrations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 7.17 Inverting the vertical structure of a fibration . . . . . . . . . . . 47 7.18 The 2-category Cats . . . . . . . . . . . . . . . . . . . . . . . . . 48 7.19 The 2-category of fibrations over a given base category . . . . . . 48 7.20 The category of contexts . . . . . . . . . . . . . . . . . . . . . . . 49 7.21 Internal categories . . . . . . . . . . . . . . . . . . . . . . . . . . 50 7.22 DNC notation for λ2 . . . . . . . . . . . . . . . . . . . . . . . . . 51 7.23 Encoding inductive types in λ2 . . . . . . . . . . . . . . . . . . . 51 7.24 Parametricity for λ2 . . . . . . . . . . . . . . . . . . . . . . . . . 52 7.25 Filter-quotients . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 7.26 Filter-quotients (old) . . . . . . . . . . . . . . . . . . . . . . . . . 53

8 The attic 55 8.1 Interpreting a derivation in λC categorically . . . . . . . . . . . . 55 8.2 Facts about λC (oct 2002) . . . . . . . . . . . . . . . . . . . . . . 61 8.3 Expressing preservation of limits in NDC . . . . . . . . . . . . . 63 8.4 Skeletons of proofs . . . . . . . . . . . . . . . . . . . . . . . . . . 65 8.5 Infinitesimals as sequences . . . . . . . . . . . . . . . . . . . . . . 65 8.6 Filters and ultrafilters . . . . . . . . . . . . . . . . . . . . . . . . 65 8.7 A glimpse of non-standard analysis . . . . . . . . . . . . . . . . . 66 8.8 Semi-standard analysis: NSA using filters . . . . . . . . . . . . . 66 8.9 Encoding inductive types . . . . . . . . . . . . . . . . . . . . . . 68 8.10 Categories in DNC . . . . . . . . . . . . . . . . . . . . . . . . . . 69 8.11 categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 8.12 products . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 8.13 How to interpret set theory in any topos . . . . . . . . . . . . . . 70 8.14 Falsifying some classical truths . . . . . . . . . . . . . . . . . . . 70 8.15 Set^{F} as a topos . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 8.16 Parametricity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 8.17 Parametricity for λC . . . . . . . . . . . . . . . . . . . . . . . . . 71 8.18 Sheaves . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71

8.18.1 Putting a topology on the sheaf of sections . . . . . . . . 71 8.19 Sheaves (Johnstone, pp.10–12) . . . . . . . . . . . . . . . . . . . 71 8.20 Geometric morphisms (on topological spaces) . . . . . . . . . . . 72 8.21 Grothendieck topologies . . . . . . . . . . . . . . . . . . . . . . . 73 8.22 A glimpse on Synthetic Differential Geometry . . . . . . . . . . . 73 8.23 Appendix: reading some trees and diagrams aloud . . . . . . . . 73 8.24 Appendix: Writing down the handwaving over diagrams . . . . . 75 8.25 Dependencies between chapters . . . . . . . . . . . . . . . . . . . 75

1 Introduction

1.1 λ-calculus as a programming language

order of evaluation termination strong normalization proving equality by β-reduction versus proving equality by building a proof-

term; Curry-Howard and doing “syntactical proofs” by building first the construction of the T-part; parametricity can make the P-parts come for free; how much category theory we can represent in the language for the T-parts.

[figure: (λx. + x x)((λy. − y2)5); +((λy. − y 2)5)((λy. − y 2)5); β; (λx. + x x)((λy. − y2)5); (λx. + x x)(− 5 2); β; +((λy. − y 2)5)((λy. − y 2)5); +((λy. − y 2)5)((λz. − z 2)5); α; +((λy. − y 2)5)((λz. − z 2)5); +((λy. − y 2)5)(− 5 2); β; +((λy. − y 2)5)((λz. − z 2)5); +(− 5 2)((λz. − z 2)5); β; (λx. + x x)(− 5 2); +(− 5 2)(− 5 2); β; +((λy. − y 2)5)(− 5 2); +(− 5 2)(− 5 2); β; +(− 5 2)((λz. − z 2)5); +(− 5 2)(− 5 2); β]

1.2 Typing

to ensure strong normalization to make it fit some real-world models model for λ→ mention that a topos is a model for λP (check the details)

1.3 Real-world semantics

RW semantics is the idea that is implicit when we say that we are encoding some RW objects in the λ-calculus.

We can only represent “constructive” objects! (but we are defining “constructive” as representable in the λ-calculus...) Constructive objects are well-behaved in several ways: we can compute with them - equality via normalization coherence - sometimes ∃! (constructive) guy of a certain type parametricity - constructive guys obey “free theorems” we can try to build them by proof-search (usually normal proofs)

1.4 Skeletons of proofs

Examples in λ→: Curry-Howard (note: sequents will be discussed later) adding terms to a tree of types the terms grow as the tree grows; λ-terms encode trees a language where we can say “the natural term of type A” a bit more than that: several names for (different) entities of the same type details, for λ→; example of a′ ↦ a′′ ↦ a′ and a′ ↦ a′′ ↦ a′′ mention that this extends to λ2; examples in λ2 in λ2 we have parametricity; all paths cross. in DNC we can ask: ”is there a natural construction for α”?

1.5 Category theory

two functorial diagrams in Set (fix a set E[b]...)

the ‘⇒’ operate in two levels interpreting these two functors in λP natural transformations a system of natural deduction for categories: ⇒I and →^{•}I (more definitions, other categories, etc, will come later) in a certain sense, with these tools a lot of category theory becomes “ob-

vious”; we can just give some statements in DNC, plus a few definitions and diagrams, and a computer or a slave can fill out all the missing details. And I feel - but this is a matter of taste - that the DNC notation carries the “intuition” of what’s going on.

1.6 What is “obvious”?

a computer or a slave can fill out the details example of how to do this: DNC term - x ⇒ (a ↦ x) → proof search → derivation that gives the RW semantics → still need to prove functorialities and naturalities → by duplication and normalization, or by parametricity bigger example: Yoneda - stands on some more basic functors. proving ↔s in adjunctions

1.7 Why do we need category theory

understanding these constructive worlds semi-standard and non-standard analysis toposes recycling skeletons of proofs: turning parts of skeletons into sequents and then into morphisms sublanguages correspond to different categorical models constructive proofs with infinitesimals getting rid of generic filter-infinitesimals parametricity for them (in the future); differential λ-calculus

2 System DNC: a system of natural deduction for categories

parte 1 / paper 1: System DNC: a system of natural deduction for categories. Apresento o λC do meu jeito, mostro a variação com contextos mínimos, reduzo pra uma espécie de dedução natural, separo a árvore (tem que ser uma árvore ”boa”) nas regras ”s”, monto o dicionário. Mostro a motivação para a minha notação para categorias, defino protocategorias, protofuntores e protoNTs, mostro o DNC. A parte lógica e a relação entre proto e não-proto vão ser descritas em outro paper.

2.1 λC: 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.

2.2 A crash course on λC: (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_{□□}

2.3 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}

A bigger tree: (the double lines represent places with hidden weakenings)

{⊢ ∗:□ \atop A:∗ ⊢ A:∗} ; A:∗, a:A ⊢ a:A

\begin{matrix}{⊢ ∗:□ \atop A:∗ ⊢ A:∗} & \begin{matrix}\begin{matrix}{⊢ ∗:□ \atop A:∗ ⊢ A:∗} & ⊢ ∗:□ \\ A:∗ ⊢ (Πa:A.∗):□ \end{matrix} ; A:∗, B:(Πa:A.∗) ⊢ B:(Πa:A.∗) & {⊢ ∗:□ \atop A:∗ ⊢ A:∗} ; A:∗, a:A ⊢ a:A \\ A:∗, B:(Πa:A.∗), a:A ⊢ Ba:∗ \end{matrix} \\ A:∗, B:(Πa:A.∗) ⊢ (Πa:A.Ba):∗ \end{matrix}

A:∗, B:(Πa:A.∗), f:(Πa:A.Ba) ⊢ f:(Πa:A.Ba)

A:∗, B:(Πa:A.∗), f:(Πa:A.Ba), a:A ⊢ fa:Ba

2.4 λC_{D}: λC in natural-deduction style

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.

2.5 λC_{D}: λC in natural-deduction style (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.

2.6 Subsystems of λC

2.7 Pure type systems

2.8 Logic in λC

2.8.1 Prop as *

2.8.2 Irrelevance of proofs

2.8.3 Leibniz Equality

[prf[P (a)]]^{1}

prf[P (a)] ↦ prf[P (a)] 1

P ↦ prf[P (a)] ↦ prf[P (a)] 2

prf[∀P.P (a) [figure]P (a)] ren

prf[a = a] ren

2002h (typeset 2002dec30 19:22) Edrx http://angg.twu.net/

[P]^{1} {prf[a = b] \atop prf[∀P.P (a) [figure]P (b)]} ren
prf[P (a) [figure]P (b)]

[P]^{1} {prf[b = c] \atop prf[∀P.P (b) [figure]P (c)]} ren
prf[P (b) [figure]P (c)]

prf[P (a) [figure]P (c)]

prf[∀P.P (a) [figure]P (c)] 1

prf[a = c] ren

prf[a = a]

λx.Prfs[x = a] {prf[a = b] \atop prf[∀P.P (a) [figure]P (b)]} ren

prf[(a = a) [figure](b = a)]

prf[b = a]

2.8.4 Subsets and subtypes

2.8.5 The calculus of constructions

2.9 DNC terms (and pseudoterms, and pseudopoints)

Terms may belong to several syntactic classes at the same time any term or subterm will belong to at least one of these classes: pseudopoint (pp) point (p) morphism (m) functor (F) natural transformation (NT) space of (E) object (O) category (C) When parsing a big term, some subterms will start having one class, and

then they will have to be converted to other classes (or “be reinterpreted”; discuss the “ren” rules).

The standard conversions:

pp → p when Cat[pp] is Set
p → pp by defining O[p] := E[p], Cat[p] := Set
m → p (a ↦ b) : E[a ↦ b]
F → pp O[a ⇒ a^{F}] := a ⇒ a^{F}, Cat[a ⇒ a^{F}] := Cat[a^{F}]^{Cat[a]}
NT → m a →^{•} (a^{F} ↦ a^{G}) ≡ (a ⇒ a^{F}) ↦ (a ⇒ a^{G})

Several other conversions are possible, but not so common: O → pp, m → pp in internal categories F → m in 2-categories E → pp in polymorphic models, and in certain fibrations; remember the

“mixed exponentials” E[a] ↦ a

Things like a^{F} will be considered “atomic terms” (or “atomic pre-terms”?) until I decide what to do with the superscript...

Note that in the metalanguage or in the interpretation a functor takes names of pseudopoints to names of pseudopoints — a ⇒ a^{F} takes ‘b’ and produces ‘b^{F} ’ by pattern matching — an morphisms can do the same: consider a ↦ f(a) (or even just a ↦ b) acting on points a_{0} and a_{1}.

(The matrix below, that shows the several syntactic classes associated to subterms of the term of the Yoneda lemma, is connected to what happens in the section 2.11.6; explain the connection).

(a ; x ⇒ x^{F}) →^{•} (a^{F} ↔ (x →^{•} ((a ↦ x) ↦ x^{F})))
pp 1 1 1 2 1  1  1 4  1 3 1  1
p  2  2  3  2  2
m  1  2  1  1
F  1
NT 1 1

O E C

Why using this language (maybe this discussion needs to be moved to the introduction!)

The effect of all that is that it becomes easy to generalize points to pseudpoints; then we need the passage ND→sequents to have semantics again (there are several ways to order the free variables, but they will be isomorphic to one another). Instead of starting by a very general situation (categories, pseudopoints, etc) as if the simple situation (points) would be just a particular case of it, we assume that there are several (infinite?) levels of generalization to go, and there is no natural choice for what is the right level of generalization to start; instead, we start on level 0, but we do our proofs in a way that carries on easily to more general levels (by recycling, i.e., reinterpreting the skeletons with a different dictionary).

2.10 Categories in λC

2.11 Encoding categories in λC

[figure: ^{Objs^{C}}; _{Hom_{C}}; _{Hom_{C}}; _{id_{C}}; _{Hom_{C}}; ∘_{C}; _{Hom_{C}}; _{eq_{C}}; _{id_{C}}; _{idL_{C}}; _{id_{C}}; _{idR_{C}}; ∘_{C}; _{idL_{C}}; ∘_{C}; _{idR_{C}}; ∘_{C}; _{assoc_{C}}; _{eq_{C}}; _{idL_{C}}; _{eq_{C}}; _{idR_{C}}; _{eq_{C}}; _{assoc_{C}}; ^{Objs^{C}}; Cat^{−−}[a]; Cat^{−−}[a]; Cat^{−}[a]; Cat^{−}[a]; Cat[a]]

idL_{C} = prf[∀O[a].∀O[b].∀(a↦b).a↦a↦b = a↦b] : Prfs[∀O[a].∀O[b].∀(a↦b).a↦a↦b = a↦b] = ΠO[a]:Objs_{C}.ΠO[b]:Objs_{C}.Π(a↦b):E[a↦b].Prfs[a↦a↦b = a↦b]

where E[a↦b] := Hom_{C} O[a]O[b] Prfs[a↦a↦b = a↦b] := eq_{C}O[a]O[b](a↦a↦b)(a↦b) (a↦a↦b) := ∘_{C}O[a]O[a]O[b](a↦a)(a↦b) (a↦a) := id_{C}O[a] and, similarly, idR_{C} = prf[∀O[a].∀O[b].∀(a↦b).a↦b↦b = a↦b] assoc_{C} = prf[∀O[a].∀O[b].∀O[c].∀O[d].

∀(a↦b).∀(b↦c).∀(c↦d).

((c↦d) ∘ (b↦c)) ∘ (a↦b) = (c↦d) ∘ ((b↦c) ∘ (a↦b))]

2.11.1 Protocategories, proto-NTs and other protothings

2.11.2 The rule (⇒I)

2.11.3 The syntactical world, the real world and the normalization trick

If we can show that the two trees below normalize to the same term/tree (for arbitrary morphisms a ↦ b and b ↦ c) then we will have shown that the functor CONTENTS 14 a ⇒ a^{F} respects composition:

\begin{matrix}\begin{matrix}a ↦ b & a ⇒ a^{F} \\ a^{F} ↦ b^{F} \end{matrix} & \begin{matrix}b ↦ c & a ⇒ a^{F} \\ b^{F} ↦ c^{F} \end{matrix} \\ a^{F} ↦ c^{F} \end{matrix} ≡ \begin{matrix}\begin{matrix}a ↦ b & b ↦ c \\ a ↦ c \end{matrix} & a ⇒ a^{F} \\ a^{F} ↦ c^{F} \end{matrix}

a ⇒ a^{F} respects identities:

\begin{matrix}O[a] & a ⇒ a^{F} \\ O[a^{F}] \end{matrix} ; a^{F} ↦ a^{F} ≡ \begin{matrix}{O[a] \atop a ↦ a} & a ⇒ a^{F} \\ a^{F} ↦ a^{F} \end{matrix}

a →^{•} (a^{F} ↦ a^{G}) obeys the condition on squares:

\begin{matrix}\begin{matrix}a ↦ b & a ⇒ a^{F} \\ a^{F} ↦ b^{F} \end{matrix} & \begin{aligned}O[b] & a →^{•} (a^{F} ↦ a^{G}) \\ & b^{F} ↦ b^{G} \end{aligned} \\ a^{F} ↦ b^{G} \end{matrix} ≡ \begin{matrix}\begin{aligned}O[a] & a →^{•} (a^{F} ↦ a^{G}) \\ & a^{F} ↦ a^{G} \end{aligned} & \begin{matrix}a ↦ b & a ⇒ a^{G} \\ a^{G} ↦ b^{G} \end{matrix} \\ a^{F} ↦ b^{G} \end{matrix}

A protoiso a ↔ b is an iso:

\begin{matrix}b ↦ a & a ↦ b \\ b ↦ b \end{matrix} ≡ {O[b] \atop b ↦ b}

\begin{matrix}b ↦ a & a ↦ b \\ b ↦ b \end{matrix} ≡ {O[b] \atop b ↦ b}

2.11.4 A simple example: Hom The sequent that we’ll be deriving is:

Objs_{C}:..., Hom_{C} :..., ∘_{C}:..., O[b]:Objs_{C} ⊢ (a ⇒^{−} (b ↦ a)):...

\begin{matrix}Objs & C \\ O[a] \end{matrix} ^{[s]^{1}} \begin{matrix}Objs & C \\ O[b] \end{matrix}

E[a ↦ b] Hom^{C}

O[a ↦ b]

O[a] ↦ O[a ↦ b] 1

(a ⇒ (b ↦ a))_{O}

2002h (typeset 2002dec30 19:22) Edrx http://angg.twu.net/

\begin{matrix}\begin{matrix}Objs & C \\ O[a′] \end{matrix} ^{[s]^{4}} & (a ⇒ (b ↦ a))_{O} \\ O[b ↦ a′] \end{matrix}

(E[b ↦ a′]) / (b ↦ a′) [s]^{1}

\begin{matrix}Objs & C \\ O[a′] \end{matrix} ^{[s]^{4}} \begin{matrix}Objs & C \\ O[a′′] \end{matrix} ^{[s]^{3}}

E[a′ ↦ a′′] Hom^{C}

a′ ↦ a′′ [s]^{2}

b ↦ a′′ ∘^{C}

(b ↦ a′) ↦ (b ↦ a′′) 1

(a′ ↦ a′′) ↦ ((b ↦ a′) ↦ (b ↦ a′′)) 2

O[a′′] ↦ ((a′ ↦ a′′) ↦ ((b ↦ a′) ↦ (b ↦ a′′))) 3

O[a′] ↦ (O[a′′] ↦ ((a′ ↦ a′′) ↦ ((b ↦ a′) ↦ (b ↦ a′′)))) 4

(a ⇒ (b ↦ a))_{M}

In DNC we write these trees in a shorter form:

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

O[a ↦ b]

a ⇒^{−−} (b ↦ a) 1

\begin{matrix}\begin{matrix}[b ↦ a′]^{1} & [a′ ↦ a′′]^{2} \\ b ↦ a′′ \end{matrix} & ∘_{C} \\ (b ↦ a′) ↦ (b ↦ a′′) \end{matrix} ; 1 ; a ⇒^{−} (b ↦ a) 2

Note: (b ↦ a′) ↦ (b ↦ a′′) has two (equivalent) types;

E[(b ↦ a′) ↦ (b ↦ a′′)] := Hom_{Set} O[b ↦ a′]O[b ↦ a′′]

and

E[(b ↦ a′) ↦ (b ↦ a′′)] := (a ⇒ (b ↦ a))_{O}(Hom_{Set} O[a′]O[a′′]).

(por abuso de linguagem a gente vai fingir que a regra que constrói o ⇒^{−} vai estar construindo o ⇒; duas interpretações pra isso: ou a construção dos prfs está implícita (“óbvia”), ou a gente está num universo sintático).

2.11.5 A bigger example: the Yoneda lemma

The term that corresponds to the Yoneda lemma is:

Y := (a; x ⇒ x^{F}) →^{•} (a^{F} ↔ (x →^{•} ((a ↦ x) ↦ x^{F})))

in order to construct it we need first to understand the space in which it will lie:

E[Y] := E[(a; x ⇒ x^{F}) →^{•} (a^{F} ↔ (x →^{•} ((a ↦ x) ↦ x^{F})))]

it will turn out that if we try to form E[Y] by “breaking its term in smaller pieces”, we will discover what is the context Γ that we need to derive it — that is, Γ ⊢ E[Y] should be derivable when translated to a judgement in λC — and also which will be the basic entries that we need to set in the dictionary; they will be that Cat[a] = Cat[x], Cat[a^{F}] = Cat[x^{F}] = Set, and of course we’ll need to have the category C := Cat[a] = Cat[x] between the hypotheses in the context Γ.

Apparently the context Γ will have to include the functors

\begin{aligned}& (a; x ⇒ x^{F}) ⇒ (x →^{•} ((a ↦ x) ↦ x^{F})) \\ and & (a; x ⇒ x^{F}) ⇒ a^{F} \end{aligned}

that are selected from the objects of certain categories of functors by ‘s’ rules (pay attention to the ‘s’s in the trees below!), but we’ll see that we have derivations for

\begin{aligned}& C ⊢ (a; x ⇒ x^{F}) ⇒ (x →^{•} ((a ↦ x) ↦ x^{F})) \\ and & C ⊢ (a; x ⇒ x^{F}) ⇒ a^{F} \end{aligned}

and so the derivation for the term of the Yoneda lemma (after building the space in which it lives, etc) will give

C ⊢ (a; x ⇒ x^{F}) →^{•} (a^{F} ↔ (x →^{•} ((a ↦ x) ↦ x^{F})))

2.11.6 Typing the term of the Yoneda Lemma

{C \atop Cat[a]} ren

{C \atop Cat[x]} ren {Set \atop Cat[x^{F}]} ren

Cat[x ⇒ x^{F}]

Cat[a; x ⇒ x^{F}]

{Set \atop Cat[a^{F}]} ren

Cat[(a; x ⇒ x^{F}) ⇒ a^{F}]

O[(a; x ⇒ x^{F}) ⇒ a^{F}] s

{C \atop Cat[a]} ren

{C \atop Cat[x]} ren {Set \atop Cat[x^{F}]} ren
Cat[x ⇒ x^{F}]

Cat[a; x ⇒ x^{F}] {Set \atop Cat[x →^{•} ((a ↦ x) ↦ x^{F})]} ren

Cat[(a; x ⇒ x^{F}) ⇒ (x →^{•} ((a ↦ x) ↦ x^{F}))]

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

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

...but E[x →^{•} ((a ↦ x) ↦ x^{F})] and E[a^{F}] are not arbitrary objects of Set, i.e., arbitrary sets; they are built as

\begin{matrix}O[a] & x ⇒ x^{F} \\ O[a^{F}] \end{matrix} ; E[a^{F}] and \begin{matrix}O[x ⇒ (a ↦ x)] & O[x ⇒ x^{F}] \\ E[(x ⇒ (a ↦ x)) ↦ (x ⇒ x^{F})] \end{matrix} ; E[x →^{•} ((a ↦ x) ↦ x^{F})] ren ,

[and something similar for x ⇒ (a ↦ x).] 2.11.7 Proving the Yoneda lemma syntactically

2002h (typeset 2002dec30 19:22) Edrx http://angg.twu.net/

A syntactical proof of (a; x ⇒ x^{F}) →^{•} (a^{F} ↔ (x →^{•} ((a → x) → x^{F}))) is just the third tree below; its double bars correspond to the first two trees, and we only didn’t draw everything as one big tree because it wouldn’t fit in the page very well.

{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} ; 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}O_{a} & {C \atop O_{x}} [so]^{2} \\ E[a ↦ x] \end{matrix} ; a ↦ x ; ^{[s]^{1}} {O[x ⇒ x^{F}] \atop x ⇒ x^{F}} ren
a^{F} ↦ x^{F}
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

2002h (typeset 2002dec30 19:22) Edrx http://angg.twu.net/

\begin{matrix}\begin{matrix}O_{a} & {C \atop O[x′]} [so]^{2} \\ a ↦ x′ \end{matrix} ; [sm]^{1} & \begin{matrix}{C \atop O[x′]} [so]^{2} & {C \atop O[x′′]} [so]^{2} \\ x′ ↦ x′′ \end{matrix} ; [sm]^{2} \\ a ↦ x′′ \end{matrix} ; (a ↦ x′) ↦ (a ↦ x′′) ; 1 ; x ⇒ (a ↦ x) ; 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 functors, we need this (modulo the ‘prf’ terms!):

\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}

\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}

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′′}) ; 2 ; (x →^{•} ((a′ ↦ x) ↦ x^{F′})) ↦ (x →^{•} ((a′′ ↦ x) ↦ x^{F′′})) ; 3 ; (a; x ⇒ x^{F}) →^{•} (x →^{•} ((a ↦ x) ↦ x^{F})) ; 4

2002h (typeset 2002dec30 19:22) Edrx http://angg.twu.net/

2.12 Basic categorical constructs

2.12.1 Adjunctions See p. 48

2.12.2 Limits 2.12.3 Cartesian-closed categories 2.12.4 Toposes 2.12.5 Fibrations See p. 47

2.12.6 2-Categories See p. 48

2.13 Some proofs in DNC

2.13.1 Cats and Fib_{I} are cartesian-closed 2.13.2 Right adjoints preserve limits

[figure: a; (i ⇒ a); (i ⇒ a); (i ⇒ a^{L}); (i ⇒ a^{L}); a^{L}; a^{L}; a; a; (i ⇒ b_{i}^{R})^{Lim}; (i ⇒ a); (i ⇒ b_{i}^{R}); (i ⇒ a^{L}); (i ⇒ b_{i}); a^{L}; (i ⇒ b_{i})^{Lim}; a; (i ⇒ b_{i})^{LimR}; (i ⇒ b_{i}^{R})^{Lim}; (i ⇒ b_{i}^{R}); (i ⇒ b_{i}^{R}); (i ⇒ b_{i}); (i ⇒ b_{i}); (i ⇒ b_{i})^{Lim}; (i ⇒ b_{i})^{Lim}; (i ⇒ b_{i})^{LimR}]

[figure: x; x, c; x, c; x, c; x, c; x, c; x, c; x; x; x; x; x; x; c ↦ a, b; x, c; a, b; x, c; x, c; a; b; x; x; c ↦ a; c ↦ b; x; (c ↦ a), (c ↦ b); c ↦ a, b; a, b; a, b; a; b; a; b; c ↦ a; c ↦ b; c ↦ a; c ↦ b; (c ↦ a), (c ↦ b)]

[figure: x; x ↦ a; x ↦ a; x ↦ a; x ↦ a; x ↦ a; x ↦ a; x; x; x; x; x; x; (b|c) ↦ a; x ↦ a; b|c; x ↦ a; x ↦ a; b; c; x; x; b ↦ a; c ↦ a; x; (b ↦ a), (c ↦ a); (b|c) ↦ a; b|c; b|c; b; c; b; c; b ↦ a; c ↦ a; b ↦ a; c ↦ a; (b ↦ a), (c ↦ a)]

[figure: (a, c)|(b, c); a, c; b, c; a, c; b, c; a; b; a; b; a|b; a|b; (a|b), c; (a, c)|(b, c); y; a, c; b, c; y; y; a; b; c ↦ y; c ↦ y; a|b; c ↦ y; (a|b), c; y; y; y; y; y; y; c ↦ y; c ↦ y; c ↦ y; c ↦ y; c ↦ y; c ↦ y; y]

2.13.3 Limits and colimits in ‘C^{I}’s can be calculated pointwise

If a category C has limits of J-shaped diagrams, then I ⇒ C also has limits of J-shaped diagrams; they can be “calculated pointwise” (or, more precisely, “objectwise”).

That is, we have a way to make sense of:

[figure: j ⇒ (i ⇒ a_{i}); i ⇒ a_{i}; j ⇒ (i ⇒ a_{i}); j ⇒ (i ⇒ b_{ij}); i ⇒ a_{i}; j ⇒ (i ⇒ b_{ij})^{Lim^{j}}; j ⇒ (i ⇒ b_{ij}); j ⇒ (i ⇒ b_{ij})^{Lim^{j}}]

we can slide the strange limit to inside the ‘j ⇒’, and define O[j ⇒ (i ⇒ b_{ij})^{Lim^{j}}] := O[i ⇒ (j ⇒ b_{ij})^{Lim^{j}}], and everything works. Let’s check that.

[figure: j ⇒ (i ⇒ a_{i}); (i; j) ⇒ a_{i}; (i; j) ⇒ a_{i}; i ⇒ a_{i}; j ⇒ (i ⇒ a_{i}); j ⇒ (i ⇒ b_{ij}); (i; j) ⇒ a_{i}; (i; j) ⇒ b_{ij}; i ⇒ a_{i}; i ⇒ (j ⇒ b_{ij})^{Lim^{j}}; j ⇒ (i ⇒ b_{ij}); (i; j) ⇒ b_{ij}; (i; j) ⇒ b_{ij}; i ⇒ (j ⇒ b_{ij})^{Lim^{j}}]

Here’s how to construct the functor ‘⇒’ in the adjunction:

\begin{matrix}{(i; j) ⇒ b_{ij} \atop i ⇒ (j ⇒ b_{ij})} & (j ⇒ b_{ij}) ⇒ (j ⇒ b_{ij})^{Lim^{j}} \\ i ⇒ (j ⇒ b_{ij})^{Lim^{j}} \end{matrix}

and here are the directions ‘←’ e ‘↦’ of the bijection:

[O[j]]^{1} \begin{aligned}[O[i]]^{1} & i →^{•} (a_{i} ↦ (j ⇒ b_{ij})^{Lim^{j}}) \\ & a_{i} ↦ (j ⇒ b_{ij})^{Lim^{j}} \end{aligned} ; (j ⇒ a_{i}) ↦ (j ⇒ b_{ij}) j →^{•} (a_{i} ↦ b_{ij})

ren

a_{i} ↦ b_{ij}

(i; j) →^{•} (a_{i} ↦ b_{ij}) 1

\begin{matrix}\begin{aligned}[O[i]]^{2} & [O[j]]^{1} & (i; j) →^{•} (a_{i} ↦ b_{ij}) \\ & a_{i} ↦ b_{ij} \end{aligned} & 1 \\ j →^{•} (a_{i} ↦ b_{ij}) \end{matrix} ; 1 ; (j ⇒ a_{i}) ↦ (j ⇒ b_{ij}) ; ren

a_{i} ↦ (j ⇒ b_{ij})^{Lim^{j}}

i →^{•} (a_{i} ↦ (j ⇒ b_{ij})^{Lim^{j}}) 2

Checking the naturalities has something to do with this diagram here:

2002h (typeset 2002dec30 19:22) Edrx http://angg.twu.net/

[figure: \begin{matrix}a_{i′} & ↦ & a_{i′′} \\ ↓ & & ↓ \\ a_{i′} & ↦ & a_{i′′} \end{matrix}; a_{i′} ↦ a_{i′′}; \begin{matrix}a_{i′} & ↦ & a_{i′′} \\ ↓ & & ↓ \\ a_{i′} & ↦ & a_{i′′} \end{matrix}; \begin{matrix}b_{i′j′} & ↦ & b_{i′′j′} \\ ↓ & & ↓ \\ b_{i′j′′} & ↦ & b_{i′′j′′} \end{matrix}; a_{i′} ↦ a_{i′′}; (j ⇒ b_{i′j})^{Lim^{j}} ↦ (j ⇒ b_{i′′j})^{Lim^{j}}; \begin{matrix}b_{i′j′} & ↦ & b_{i′′j′} \\ ↓ & & ↓ \\ b_{i′j′′} & ↦ & b_{i′′j′′} \end{matrix}; (j ⇒ b_{i′j})^{Lim^{j}} ↦ (j ⇒ b_{i′′j})^{Lim^{j}}]

We can also prove something similar for colimits:

[figure: j ⇒ (i ⇒ b_{ij}); (i; j) ⇒ b_{ij}; (i; j) ⇒ b_{ij}; i ⇒ (j ⇒ b_{ij})^{Colim^{j}}; j ⇒ (i ⇒ b_{ij}); j ⇒ (i ⇒ c_{i}); (i; j) ⇒ b_{ij}; (i; j) ⇒ c_{i}; i ⇒ (j ⇒ b_{ij})^{Colim^{j}}; i ⇒ c_{i}; j ⇒ (i ⇒ c_{i}); (i; j) ⇒ c_{i}; (i; j) ⇒ c_{i}; i ⇒ c_{i}]

Limits in Set^{C}

We want to prove that limits in Set^{C} can be calculated “pointwise”, i.e., that

((c ⇒ x_{c})^{op}; (c; i) ⇒ y_{ci}) →^{•} (((c; i) →^{•} (x_{c} → y_{ci})) ↔ (c →^{•} (x_{c} → lim_{i} y_{ci})))

\begin{aligned}\begin{matrix}[O_{c}]^{2} & [O_{i}]^{1} \\ O[c; i] \end{matrix} & [(c; i) →^{•} (x_{c} → y_{ci})]^{3} \\ & x_{c} → y_{ci} \end{aligned} ; i →^{•} (x_{c} → y_{ci}) ; 1 x_{c} → lim_{i} y_{ci} transp

c →^{•} (x_{c} → lim_{i} y_{ci}) 2

((c; i) →^{•} (x_{c} → y_{ci})) → (c →^{•} (x_{c} → lim_{i} y_{ci}))

3

[O_{i}]^{1} \begin{aligned}[O_{c}]^{1} & [c →^{•} (x_{c} → lim_{i} y_{ci})]^{2} \\ & x_{c} → lim_{i} y_{ci} \end{aligned} i →^{•} (x_{c} → y_{ci})

transp

x_{c} → y_{ci} 1

(c; i) →^{•} (x_{c} → y_{ci}) 1

(c →^{•} (x_{c} → lim_{i} y_{ci})) → ((c; i) →^{•} (x_{c} → y_{ci}))

3

2.13.4 ‘Set^{I}’s are toposes

We know that a Set^{I} inherits limits and colimits from Set; they can be calculated pointwise.

We still need to show that a Set^{I} has exponentials and a classifier object.

The exponential in ‘Set^{I}’ We have something that plays the role of the exponential:

[figure: i ⇒ a_{i}, b_{i}; i ⇒ a_{i}; i ⇒ a_{i}, b_{i}; i ⇒ c_{i}; i ⇒ a_{i}; i ⇒ (j →^{•} ((i ↦ j), b_{j} ↦ c_{j})); i ⇒ c_{i}; i ⇒ (j →^{•} ((i ↦ j), b_{j} ↦ c_{j}))]

First we need to show that (i ⇒ c_{i}) ⇒ (i ⇒ (j →^{•} ((i ↦ j), b_{j} ↦ c_{j}))) is really a functor. It depends on a functors, that is simply the product of j ⇒ (i ↦ j) and j ⇒ b_{j}:

\begin{matrix}\begin{matrix}O[i] & [O[j]]^{1} \\ E[i ↦ j] \end{matrix} & \begin{matrix}[O[j]]^{1} & i ⇒ b_{i} \\ E[b_{j}] \end{matrix} \\ E[(i ↦ j), b_{j}] \end{matrix} ; j ⇒^{−−} (i ↦ j), b_{j} ; 1

\begin{matrix}\begin{matrix}{[(i ↦ j′), b_{j′}]^{1} \atop i ↦ j′} & [j′ ↦ j′′]^{2} \\ i ↦ j′′ \end{matrix} & \begin{aligned}{[(i ↦ j′), b_{j′}]^{1} \atop b_{j′}} & \begin{matrix}[j′ ↦ j′′]^{2} & i ⇒ b_{i} \\ b_{j′} ↦ b_{j′′} \end{matrix} \\ & b_{j′′} \end{aligned} \\ (i ↦ j′′), b_{j′′} \end{matrix} ; (i ↦ j′), b_{j′} ↦ (i ↦ j′′), b_{j′′} ; 1 ; j ⇒ (i ↦ j), b_{j} ; 2

And here’s how to define the two actions of (i ⇒ c_{i}) ⇒ (i ⇒ (j →^{•} ((i ↦ j), b_{j} ↦ c_{j}))):

\begin{matrix}\begin{matrix}[O[i]]^{1} & i ⇒ b_{i} \\ j ⇒ (i ↦ j), b_{j} \end{matrix} & {i ⇒ c_{i} \atop j ⇒ c_{j}} ren \\ E[j →^{•} ((i ↦ j), b_{j} ↦ c_{j})] \end{matrix} ; i ⇒^{−−} (j →^{•} ((i ↦ j), b_{j} ↦ c_{j})) 1

\begin{aligned}\begin{matrix}\begin{matrix}[i′ ↦ i′′]^{4} & {[(i′′ ↦ j), b_{j}]^{1} \atop i′′ ↦ j} \\ i′ ↦ j \end{matrix} & b_{j} \\ (i′ ↦ j), b_{j} \end{matrix} & \begin{aligned}[O[j]]^{2} & [j →^{•} ((i′ ↦ j), b_{j} ↦ c_{j})]^{3} \\ & (i′ ↦ j), b_{j} ↦ c_{j} \end{aligned} \\ & c_{j} \end{aligned} ; (i′′ ↦ j), b_{j} ↦ c_{j} ; 1 ; j →^{•} ((i′′ ↦ j), b_{j} ↦ c_{j}) ; 2 ; (j →^{•} ((i′ ↦ j), b_{j} ↦ c_{j})) ↦ (j →^{•} ((i′′ ↦ j), b_{j} ↦ c_{j})) ; 3 ; i ⇒ (j →^{•} ((i ↦ j), b_{j} ↦ c_{j})) ; 3

2002h (typeset 2002dec30 19:22) Edrx http://angg.twu.net/

The ‘←’ side of the bijection:

\begin{aligned}[b_{i}]^{1} & \begin{aligned}{[O[i]]^{2} \atop i ↦ i} & \begin{aligned}[O[i]]^{2} & \begin{aligned}[a_{i}]^{1} & \begin{aligned}[O[i]]^{2} & i →^{•} (a_{i} ↦ (j →^{•} ((i ↦ j), b_{j} ↦ c_{j}))) \\ & a_{i} ↦ (j →^{•} ((i ↦ j), b_{j} ↦ c_{j})) \end{aligned} \\ & j →^{•} ((i ↦ j), b_{j} ↦ c_{j}) \end{aligned} \\ & (i ↦ i), b_{i} ↦ c_{i} \end{aligned} \\ & b_{i} ↦ c_{i} \end{aligned} \\ & c_{i} \end{aligned} ; a_{i}, b_{i} ↦ c_{i} ; 1 ; i →^{•} (a_{i}, b_{i} ↦ c_{i}) ; 2

The ‘↦’ side:

\begin{matrix}\begin{aligned}[a_{i}]^{3} & \begin{matrix}[i ↦ j]^{1} & i ⇒ a_{i} \\ a_{i} ↦ a_{j} \end{matrix} \\ & a_{j} \end{aligned} & \begin{aligned}[O[j]]^{2} & i →^{•} (a_{i}, b_{i} ↦ c_{i}) \\ & a_{j}, b_{j} ↦ c_{j} \end{aligned} \\ b_{j} ↦ c_{j} \end{matrix} ; (i ↦ j), b_{j} ↦ c_{j} ; 1 ; j →^{•} ((i ↦ j), b_{j} ↦ c_{j}) ; 2 ; a_{i} ↦ (j →^{•} ((i ↦ j), b_{j} ↦ c_{j})) ; 3 ; i →^{•} (a_{i} ↦ (j →^{•} ((i ↦ j), b_{j} ↦ c_{j}))) ; 4

The classifier in ‘Set^{I}’ Some new notation: an O[a|_{P}] is a subobject of O[a]; the motivation for that is that we want to have E[a|_{P (a)}] as the set of ‘a’s “such that P (a) is true”; by the way, I call this ‘|’ the “ ‘such that’ bar”.

Each O[a|_{P}] is associated to a specific (proto-)monic a|_{P} ↪ a.

Sub(O_{a}) is the category of subobjects of O_{a}. For any two objects of Sub(O_{a}), O[a|_{P}] and O[a|_{Q}], there is at most one morphism a|_{P} → a|_{Q} making the obvious diagram commute, and when that arrow exists it is a monic.

A sub(O_{a}) is a subobject of O_{a}, i.e., an object of Sub(O_{a}).

Sub(x ⇒ x^{F}) = Sub(O[x ⇒ x^{F}]) is the category of subfunctors of a certain functor, i.e., the category of subobjects of the functor when it is seen as an object of a category of functors. When Cat[x^{F}] = Set then each such subfunctor “corresponds” to a functor that takes each O[x] to a subset of the original E[x^{F}].

We define that

E[ω_{c}] := E[sub((c → \underline{d}) ⇒ ⊤), i.e.,

O[ω] := c ⇒ ω_{c} = c ⇒ sub((c → \underline{d}) ⇒ ⊤),

and we must check that everything works.

We will use ⊤ to denote both the terminal in Set (E[⊤] = {⊤}) and the terminal in C ⇒ Set (O[⊤] = c ⇒ ⊤). There is some ambiguity. Yuck.

Dismantling O[ω] = c ⇒ ω_{c}:

{C \atop O_{c}} [so]^{3}

\begin{matrix}[O_{c}]^{3} & {C \atop O_{d}} [so]^{1} \\ c → d \end{matrix} ; [sm]^{1} ; O[c → \underline{d}] ; ren E_{⊤}

(c → \underline{d}) ⇒ ⊤ 1

sub((c → \underline{d}) ⇒ ⊤) [ssub]^{2}

(c → \underline{d}) ⇒ ⊤|_{P (c→d)} ren

E[(c → \underline{d}) ⇒ ⊤|_{P (c→d)}] 2

c ⇒ ((c → \underline{d}) ⇒ ⊤|_{P (c→d)}) 3; sF

‘ssub’ is “select a subobject”; in the case, “select a subfunctor”. Note that the last step left a functor as a free variable.

Constructing O[ω] explicitly:

\begin{matrix}{[c′ → c′′]^{2} \atop (c′′ → \underline{d}) ⇒ (c′ → \underline{d})} & {[sub[(c′ → \underline{d}) ⇒ ⊤]]^{1} \atop (c′ → \underline{d}) ⇒ ⊤|_{P (c′→d)}} ren \\ (c′′ → \underline{d}) ⇒ ⊤|_{P (c′→d)} \end{matrix}

sub[(c′′ → \underline{d}) ⇒ ⊤] ren

sub[(c′ → \underline{d}) ⇒ ⊤] → sub[(c′′ → \underline{d}) ⇒ ⊤] 1

c ⇒ sub[(c → \underline{d}) ⇒ ⊤] 2

c ⇒ ω_{c} ren

O[ω] ren

The ‘true’ arrow (in the step marked with a (*) we are considering a functor as a subfunctor or itself:

\begin{matrix}\begin{matrix}{E[⊤] \atop ⊤ → ⊤} ; (c → \underline{d}) ⇒ ⊤ & 1 \\ sub((c → \underline{d}) ⇒ ⊤) \end{matrix} & (∗) \\ ⊤ ↪ sub((c → \underline{d}) ⇒ ⊤) \end{matrix}2

c →^{•} (⊤ ↪ sub((c → \underline{d}) ⇒ ⊤))

3

⊤ ↪ ω ren

2002h (typeset 2002dec30 19:22) Edrx http://angg.twu.net/

The classifier rule (that given a monic obtains its characteristic function): (Note: these are old deductions, from a time when the system was more

much imprecise than it is today... they need several corrections)

\begin{aligned}{[O[c → \underline{d}]]^{1} \atop O[d]} & {x|_{P} ↪ x \atop c →^{•} (x_{c}|_{P} ↪ x_{c})} ren \\ & x_{d}|_{P} ↪ x_{d} \end{aligned} \begin{aligned}[x_{c}]^{2} & \begin{matrix}{[O[c → \underline{d}]]^{1} \atop c → d} & {x|_{P} ↪ x \atop O[x]} ; c ⇒ x_{c}ren \\ x_{c} → x_{d} \end{matrix} \\ & x_{d} \end{aligned}

E[⊤|_{∃x_{d}|_{P}}] PB

O[c → \underline{d}] → E[⊤|_{∃x_{d}|_{P}}] 1

{(c → \underline{d}) ⇒ ⊤|_{∃x_{d}|_{P}} \atop sub((c → \underline{d}) ⇒ ⊤)} ren

x_{c} → sub((c → \underline{d}) ⇒ ⊤) 2

c →^{•} (x_{c} → sub((c → \underline{d}) ⇒ ⊤))

3

x → ω ren

Pullback with the ‘true’ arrow:

{[O[c]]^{2} \atop c → c} ; O[c → c] [x_{c}]^{1}

[O[c]]^{2} {x → ω_{S} \atop c →^{•} (x_{c} → sub((c → \underline{d}) ⇒ ⊤))} ren
x_{c} → sub((c → \underline{d}) ⇒ ⊤)

sub((c → \underline{d}) ⇒ ⊤)

(c → \underline{d}) →^{•} (⊤|Scd ↪ ⊤)

((⊤|Scc ↪ ⊤) / (((⊤ → ω_{S}) / (ω_{S})) / (x_{c} → ω_{S}) 1)) / ((x|_{S})_{c} ↪ x_{c})

c →^{•} ((x|_{S})_{c} ↪ x_{c}) 2

x|_{S} ↪ x ren

2.13.5 The fibred Yoneda lemma

[figure: (\underline{b} ↦ i); e′_{b}; (\underline{b} ↦ i); e′′_{b}; e′_{b}; e′′_{b}; (\underline{b} ↦ i); •; e′_{i}; e′′_{i}; e′_{b}; e′_{i}; e′′_{b}; e′′_{i}; (\underline{b} ↦ i); b; e′_{b}; b; e′′_{b}; b]

[figure: (fib_{b}[\underline{b} ↦ i] ↦ fib_{b}[e′_{b}]); e′_{i}; (fib_{b}[\underline{b} ↦ i] ↦ fib_{b}[e′_{b}]); (fib_{b}[\underline{b} ↦ i] ↦ fib_{b}[e′′_{b}]); e′_{i}; e′′_{i}; (fib_{b}[\underline{b} ↦ i] ↦ fib_{b}[e′′_{b}]); e′′_{i}]

3 Categorical models for type theories

parte 2: Using system DNC to represent categorical models for type theories in type theories. CCCs, fibrations, PLC, λP, Hyland/Pitts. How to go to the general case by changing the dictionary.

3.1 The category of contexts

See p. 49.

3.2 Adjoints to substitution functors

The functor from Sub(A) to Sub(A × B) (A, B sets, for example) has a left adjoint ∃ and a right adjoint ∀.

The weakening functor induced by Γ, a ↦ Γ in a “good” codomain fibration has a left adjoint Σ and a right adjoint Π.

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

2002h (typeset 2002dec30 19:22) Edrx http://angg.twu.net/

CONTENTS 28 The two adjoints to S_{w}, Σ_{w} ⊣ S_{w} and S_{w} ⊣ Π_{w}, can be constructed in λC:

[figure: (\begin{matrix}a:A, b:B(a), p:P (a, b) \\ ↓ \\ a:A, b:B(a) \end{matrix}); (\begin{matrix}a:A, (b, p):(Σb:B(a).P (a, b)) \\ ↓ \\ a:A \end{matrix}); Σ_{w}; _{(\begin{matrix}a:A, q:Q(a) \\ ↓ \\ a:A \end{matrix})}; _{(\begin{matrix}a:A, b:B(a), q:Q(a) \\ ↓ \\ a:A, b:B(a) \end{matrix})}; S_{w}; _{(\begin{matrix}a:A, b:B(a), r:R(a, b) \\ ↓ \\ a:A, b:B(a) \end{matrix})}; _{(\begin{matrix}a:A, (b ↦ r):(Πb:B(a).R(a, b)) \\ ↓ \\ a:A \end{matrix})}; Π_{w}; (\begin{matrix}a:A, b:B(a), p:P (a, b) \\ ↓ \\ a:A, b:B(a) \end{matrix}); _{(\begin{matrix}a:A, b:B(a), q:Q(a) \\ ↓ \\ a:A, b:B(a) \end{matrix})}; \begin{matrix}q:=f(a,b,p) \\ q:=f′(⟨b,p⟩) \end{matrix}; (\begin{matrix}a:A, (b, p):(Σb:B(a).P (a, b)) \\ ↓ \\ a:A \end{matrix}); _{(\begin{matrix}a:A, q:Q(a) \\ ↓ \\ a:A \end{matrix})}; \begin{matrix}q:=f(a,π_{1}((b,p)),π_{2}((b,p))) \\ q:=f′(a,(b,p)) \end{matrix}; _{(\begin{matrix}a:A, q:Q(a) \\ ↓ \\ a:A \end{matrix})}; _{(\begin{matrix}a:A, (b ↦ r):(Πb:B(a).R(a, b)) \\ ↓ \\ a:A \end{matrix})}; \begin{matrix}(b↦r):=g(a,q) \\ (b↦r):=λb.g′(a,b,q) \end{matrix}; _{(\begin{matrix}a:A, b:B(a), q:Q(a) \\ ↓ \\ a:A, b:B(a) \end{matrix})}; _{(\begin{matrix}a:A, b:B(a), r:R(a, b) \\ ↓ \\ a:A, b:B(a) \end{matrix})}; \begin{matrix}r:=(g(a,q))(b) \\ r:=g′(a,b,q) \end{matrix}]

The action of Σ_{w} on morphisms, in λC:

[figure: (\begin{matrix}a:A, b:B(a), p′:P′(a, b) \\ ↓ \\ a:A, b:B(a) \end{matrix}); (\begin{matrix}a:A, (b, p′):(Σb:B(a).P′(a, b)) \\ ↓ \\ a:A \end{matrix}); Σ_{w}; _{(\begin{matrix}a:A, b:B(a), p′′:P′′(a, b) \\ ↓ \\ a:A, b:B(a) \end{matrix})}; _{(\begin{matrix}a:A, (b, p′′):(Σb:B(a).P′′(a, b)) \\ ↓ \\ a:A \end{matrix})}; Σ_{w}; (\begin{matrix}a:A, b:B(a), p′:P′(a, b) \\ ↓ \\ a:A, b:B(a) \end{matrix}); _{(\begin{matrix}a:A, b:B(a), p′′:P′′(a, b) \\ ↓ \\ a:A, b:B(a) \end{matrix})}; p′′:=f(a,b,p′); (\begin{matrix}a:A, (b, p′):(Σb:B(a).P′(a, b)) \\ ↓ \\ a:A \end{matrix}); _{(\begin{matrix}a:A, (b, p′′):(Σb:B(a).P′′(a, b)) \\ ↓ \\ a:A \end{matrix})}; (b,p′′):=⟨π_{1}((b,p′)),f(a,b,π_{2}((b,p′)))⟩]

The action of Π_{w} on morphisms, in λC:

[figure: (\begin{matrix}a:A, b:B(a), r′:R′(a, b) \\ ↓ \\ a:A, b:B(a) \end{matrix}); (\begin{matrix}a:A, (b ↦ r′):(Πb:B(a).R′(a, b)) \\ ↓ \\ a:A \end{matrix}); Π_{w}; _{(\begin{matrix}a:A, b:B(a), r′′:R′′(a, b) \\ ↓ \\ a:A, b:B(a) \end{matrix})}; _{(\begin{matrix}a:A, (b ↦ r′′):(Πb:B(a).R′′(a, b)) \\ ↓ \\ a:A \end{matrix})}; Π_{w}; (\begin{matrix}a:A, b:B(a), r′:R′(a, b) \\ ↓ \\ a:A, b:B(a) \end{matrix}); _{(\begin{matrix}a:A, b:B(a), r′′:R′′(a, b) \\ ↓ \\ a:A, b:B(a) \end{matrix})}; r′′:=g(a,b,r′); (\begin{matrix}a:A, (b ↦ r′):(Πb:B(a).R′(a, b)) \\ ↓ \\ a:A \end{matrix}); _{(\begin{matrix}a:A, (b ↦ r′′):(Πb:B(a).R′′(a, b)) \\ ↓ \\ a:A \end{matrix})}; (b↦r′′):=λb.g(a,b,(b↦r′)(b))]

A more complete categorical explanation of the functor Π_{w}:

2002h (typeset 2002dec30 19:22) Edrx http://angg.twu.net/

(...)

A more complete categorical explanation of the functor Σ_{w}: (...) Equality as the left adjoint of a contraction functor (“Lawvere equality”,

sec. 4.1.7 of [J99]):

[figure: (\begin{matrix}Γ, x:σ; ⊤[Θ] \\ ↓ \\ Γ, x:σ \end{matrix}); (\begin{matrix}Γ, x:σ, y:σ; ⊤[Θ] \\ ↓ \\ Γ, x:σ, y:σ \end{matrix}); (\begin{matrix}Γ, x:σ; ⊤[Θ] \\ ↓ \\ Γ, x:σ \end{matrix}); _{(\begin{matrix}Γ, x:σ; ⊤[φ[y := x]] \\ ↓ \\ Γ, x:σ \end{matrix})}; (\begin{matrix}Γ, x:σ, y:σ; ⊤[Θ] \\ ↓ \\ Γ, x:σ, y:σ \end{matrix}); _{(\begin{matrix}Γ, x:σ, y:σ; ⊤[φ] \\ ↓ \\ Γ, x:σ, y:σ \end{matrix})}; _{(\begin{matrix}Γ, x:σ, y:σ; ⊤[φ] \\ ↓ \\ Γ, x:σ, y:σ \end{matrix})}; _{(\begin{matrix}Γ, x:σ; ⊤[φ[y := x]] \\ ↓ \\ Γ, x:σ \end{matrix})}; (y:=x)^{∗}; Γ, x:σ; Γ, x:σ, y:σ; y:=x]

Jacobs, sec. 4.6.1., def: a fibration p : E → B has subset types if the functor ⊤ below has a right adjoint (“{-}”). It has full subset types if P : E → B is full (being faithful is automatic).

[figure: (\begin{matrix}a|_{⊤} \\ ↓ \\ a \end{matrix}); (\begin{matrix}b|_{P} \\ ↓ \\ b \end{matrix} ); a; (\begin{matrix}a|_{⊤} \\ ↓ \\ a \end{matrix}); ⊤; (\begin{matrix}b|_{P} \\ ↓ \\ b \end{matrix} ); b|_{P}; \{−\}; a; b|_{P}]

counit ϵ_{X} : ⊤\{X\} → X  (\begin{matrix}b|_{P} \\ ↓ \\ b|_{P} \end{matrix} ) ↦ (\begin{matrix}b|_{P} \\ ↓ \\ b \end{matrix} )
π_{X} = p(ϵ_{X}) : {X} → pX  b|_{P} ↦ b
P : E → B^{→}  (\begin{matrix}b|_{P} \\ ↓ \\ b \end{matrix} ) ⇒ (\begin{matrix}b|_{P} \\ ↓ \\ b \end{matrix} )

Jacobs, sec. 4.8: the fibration of relations for p : E → B, Rel(E) → B, is defined by the following pullback of categories (a “change of base situation”):

[figure: ⌟; Rel(E); E; Rel(E); B; E; (B × B); p; B; (B × B); p; ⌟; ^{(\begin{matrix}b′, b′′|_{R} \\ ↓ \\ b′, b′′ \end{matrix})}; ^{(\begin{matrix}b′, b′′|_{R} \\ ↓ \\ b′, b′′ \end{matrix})}; ^{(\begin{matrix}b′, b′′|_{R} \\ ↓ \\ b′, b′′ \end{matrix})}; b; ^{(\begin{matrix}b′, b′′|_{R} \\ ↓ \\ b′, b′′ \end{matrix})}; b′, b′′; b; b′, b′′]

Cartesian lifitings in a fibration of relations:

[figure: ^{(\begin{matrix}a′, a′′|_{R(f(a′),f(a′′))} \\ ↓ \\ a′, a′′ \end{matrix})}; ^{(\begin{matrix}b′, b′′|_{R(b′,b′′)} \\ ↓ \\ b′, b′′ \end{matrix})}; □; ^{(\begin{matrix}a′, a′′|_{R(f(a′),f(a′′))} \\ ↓ \\ a′, a′′ \end{matrix})}; a; ^{(\begin{matrix}b′, b′′|_{R(b′,b′′)} \\ ↓ \\ b′, b′′ \end{matrix})}; b; a; b; b:=f(a)]

3.3 Fibrations for F2

Rules for PLC:

Structural rules: ax, s and weak as as usual; conv is not needed (I think). Rules about terms of class □-1:

\begin{matrix}κ:□ & μ:□ \\ (κ × μ) : □ \end{matrix}  1:□  ∗:□  {κ:□ \atop (κ → ∗):□}

Rules about terms of class □-2:

\begin{matrix}K:κ & M:μ \\ ⟨K, M⟩:(κ × μ) \end{matrix}  {ν:(κ × μ) \atop π_{1}ν:κ}  {ν:(κ × μ) \atop π_{2}ν:μ}  ·:1

\begin{aligned}K:κ & N:(κ → ∗) \\ & NK:∗ \end{aligned}  {Γ, K:κ ⊢ A:∗ \atop Γ ⊢ (λK:κ.A):(κ → ∗)}

Rules about terms of class ∗-1:

\begin{matrix}A:∗ & B:∗ \\ (A × B):∗ \end{matrix}  \begin{matrix}A:∗ & B:∗ \\ (A → B):∗ \end{matrix}  1:∗

{Γ, K:κ ⊢ A:∗ \atop Γ ⊢ (ΠK:κ.A):∗}  {Γ, K:κ ⊢ A:∗ \atop Γ ⊢ (ΣK:κ.A):∗}

Rules about terms of class ∗-2:

\begin{matrix}a:A & b:B \\ ⟨a, b⟩:(A × B) \end{matrix}  {p:(A × B) \atop π_{1}p:A}  {p:(A × B) \atop π_{2}p:B}  ·:1

\begin{aligned}a:A & f:(A → B) \\ & fa:B \end{aligned}  {Γ; a:A ⊢ b:B \atop Γ ⊢ (λa:A.b):(A → B)}

\begin{matrix}K′:κ & f:(ΠK:κ.A) \\ fK′:A[K := K′] \end{matrix}  {Γ, K:κ ⊢ a:A \atop Γ ⊢ (λK:κ.a) : (ΠK:κ.A)}

Note that we won’t have π_{1} for terms Σ_{□∗}! By the way, how do π_{1} and π_{2} appear categorically? Some systems, like

Luo’s ECC, don’t have π_{2}...

The base category (the category of operators) has binary products, a terminal (not shown) and an exponentiable object, the ∗:

[figure: κ; κ′; κ; κ′ × κ′′; κ; κ′′; κ′ × κ′′; κ′; κ′ × κ′′; κ′′; K:κ; K′:κ′; K:κ; K′, K′′:κ′ × κ′′; K:κ; K′′:κ′′; K′, K′′:κ′ × κ′′; K′:κ′; K′, K′′:κ′ × κ′′; K′′:κ′′]

[figure: κ′; κ′ × κ; κ′ × κ; ∗; κ′; κ → ∗; ∗; κ → ∗; K′:κ′; K′, K:κ′ × κ; K′, K:κ′ × κ; A:∗; \begin{matrix}A:=G(K′)(K) \\ A:=H(K′,K) \end{matrix}; K′:κ′; F:(κ → ∗); \begin{matrix}F:=G(K′) \\ F:=λK:κ.H(K′,K) \end{matrix}; A:∗; F:(κ → ∗)]

Arrows to ∗ correspond to types, that are objects in the fibers:

K:κ ↦ A:∗

An example of a constructible arrow like this:

(P, Q):(∗ × ∗) ↦ (P [figure](P ∧ Q)):∗

(E[p], E[q]):(∗ × ∗) ↦ E[p ↦ p, q]:∗

Note que ainda dá pra piorar bastante: posso usar os κs pra falar de “setas construtíveis a partir de certas setas dadas” (mas aí eu não tenho uma boa notação), e dá pra falar de funtores, como naturais e lists.

Morphisms in the base category induce “substitution functors” between the fibers:

Each fiber has products, exponentials, and a terminal (not shown); we have two special morphisms ∗ × ∗ → ∗ in the base category, called “∧” and “ [figure]” (or P, Q:(∗×∗) ↦ (P ∧Q):∗ and (P, Q):(∗×∗) ↦ (P [figure]Q):∗, or (E[p], E[q]):(∗×∗) ↦ E[p, q]:∗ and (E[p], E[q]):(∗ × ∗) ↦ E[p ↦ q]:∗), that give product objects and exponential objects. For any three morphisms κ → ∗, K:κ ↦ :∗, K ↦ E[p], K ↦ E[q], K ↦ E[r], we have, in the fiber over K,

[figure: P; Q; P; Q ∧ R; P; R; Q ∧ R; Q; Q ∧ R; R; (\begin{matrix}K; p \\ ↓ \\ K \end{matrix}); _{(\begin{matrix}K; q \\ ↓ \\ K \end{matrix})}; (\begin{matrix}K; p \\ ↓ \\ K \end{matrix}); _{(\begin{matrix}K; q, r \\ ↓ \\ K \end{matrix})}; (\begin{matrix}K; p \\ ↓ \\ K \end{matrix}); _{(\begin{matrix}K; k \\ ↓ \\ K \end{matrix})}; _{(\begin{matrix}K; q, r \\ ↓ \\ K \end{matrix})}; _{(\begin{matrix}K; q \\ ↓ \\ K \end{matrix})}; _{(\begin{matrix}K; q, r \\ ↓ \\ K \end{matrix})}; _{(\begin{matrix}K; k \\ ↓ \\ K \end{matrix})}]

For any projection morphism K′, K ↦ K′ in the base category we can think in the corresponding substitution functor as a “weakening”, that adds to the context the need for a K:κ, that is not used; we require that such weakening functors have left and right adjoints:

[figure: (\begin{matrix}K′, K; p \\ ↓ \\ K′, K \end{matrix}); (\begin{matrix}K′; K, p \\ ↓ \\ K′ \end{matrix}); Σ_{w}; (\begin{matrix}K′, K; p \\ ↓ \\ K′, K \end{matrix}); _{(\begin{matrix}K′, K; q \\ ↓ \\ K′, K \end{matrix})}; (\begin{matrix}K′; K, p \\ ↓ \\ K′ \end{matrix}); _{(\begin{matrix}K′; q \\ ↓ \\ K′ \end{matrix})}; _{(\begin{matrix}K′; q \\ ↓ \\ K′ \end{matrix})}; _{(\begin{matrix}K′, K; q \\ ↓ \\ K′, K \end{matrix})}; S_{w}; _{(\begin{matrix}K′, K; q \\ ↓ \\ K′, K \end{matrix})}; _{(\begin{matrix}K′, K; r \\ ↓ \\ K′, K \end{matrix})}; _{(\begin{matrix}K′; q \\ ↓ \\ K′ \end{matrix})}; _{(\begin{matrix}K′; (K ↦ r) \\ ↓ \\ K′ \end{matrix})}; _{(\begin{matrix}K′, K; r \\ ↓ \\ K′, K \end{matrix})}; _{(\begin{matrix}K′; (K ↦ r) \\ ↓ \\ K′ \end{matrix})}; Π_{w}; K′, K; K′; w; K′; :∗; E[q]:=Q(K′); K′, K; :∗; K′, K; :∗; \begin{matrix}E[p]:=P (K′,K) \\ E[r]:=R(K′,K) \end{matrix}]

Note that “all members of a K are independent”; all products involved are “independent”. We can have things like A, F: ∗ ×(∗ → ∗), and we can mention types like F A, but only in the right (“type”) side.

Substituion: (what does this have to do with cartesian morphisms?)

[figure: (\begin{matrix}K′:κ′; p:P (K′) \\ ↓ \\ K′:κ′ \end{matrix}); (\begin{matrix}K:κ; p:P (F (K)) \\ ↓ \\ K:κ \end{matrix}); F^{∗}; (\begin{matrix}K:κ; p:P (F (K)) \\ ↓ \\ K:κ \end{matrix}); _{(\begin{matrix}K:κ; q:Q(F (K)) \\ ↓ \\ K:κ \end{matrix})}; (\begin{matrix}K′:κ′; p:P (K′) \\ ↓ \\ K′:κ′ \end{matrix}); _{(\begin{matrix}K′:κ′; q:Q(K′) \\ ↓ \\ K′:κ′ \end{matrix})}; _{(\begin{matrix}K′:κ′; q:Q(K′) \\ ↓ \\ K′:κ′ \end{matrix})}; _{(\begin{matrix}K:κ; q:Q(F (K)) \\ ↓ \\ K:κ \end{matrix})}; F^{∗}; K:κ; K′:κ′; K′:=F (K); K′:κ′; :∗; E[r]:=P (K′); K′:κ′; :∗; E[p]:=Q(K′)]

2002h (typeset 2002dec30 19:22) Edrx http://angg.twu.net/

CONTENTS 33

3.4 Fibrations for P 3.5 Bifibrations and trifibrations

Cod : Set^{→} → Set is a fibration:

[figure: a_{i}; b_{j}; ∃!; a_{i}; c_{k}; ∀; b_{j}; c_{k}; □; b_{j}; c_{k}; i; j; i; k; j; k; x, y, z; a; x, y; b; ∃!; x, y, z; a; x; b; ∀; x, y; b; x; b; □; x, y; b; x; b; x, y, z; x, y; x, y, z; x; x, y; x]

Cod : Set^{→} → Set is a cofibration:

[figure: a_{i}; b_{j}; co□; a_{i}; c_{k}; ∀; b_{j}; c_{k}; ∃!; a_{i}; b_{j}; i; j; i; k; j; k; x, y, z; b; x, y; z, b; co□; x, y, z; b; x; c; ∀; x, y; z, b; x; c; ∃!; x, y, z; b; x, y; z, b; x, y, z; x, y; x, y, z; x; x, y; x]

Cod : Set^{→} → Set is an opfibration:

[figure: a_{i}^{v}; b_{j}^{v}; co□; a_{i}^{v}; c_{k}^{v}; ∀; b_{j}^{v}; c_{k}^{v}; ∃!; a_{i}^{v}; b_{j}^{v}; i; j; i; k; j; k; (x, y, z; b)^{v}; (x, y; z ↦ b)^{v}; co□; (x, y, z; b)^{v}; (x; c)^{v}; ∀; (x, y; z ↦ b)^{v}; (x; c)^{v}; ∃!; (x, y, z; b)^{v}; (x, y; z ↦ b)^{v}; x, y, z; x, y; x, y, z; x; x, y; x]

Translating this to elementary terms:

[figure: i; j; i; k; j; k; a_{i}; c_{i}; ∀; a_{i}; b_{i}; b_{i}; b_{j}; □; b_{i}; b_{j}; b_{i}; c_{i}; b_{j}; c_{j}; ∃!; c_{i}; c_{j}; □; c_{j}; c_{k}; □; c_{i}; c_{j}; c_{j}; c_{k}; x, y, z; x, y; x, y, z; x; x, y; x; x, y, z; b; x, y, z; c; ∀; x, y, z; b; x, y, z; z ↦ b; x, y, z; z ↦ b; x, y; z ↦ b; □; x, y, z; z ↦ b; x, y; z ↦ b; x, y, z; z ↦ b; x, y, z; c; x, y; z ↦ b; x, y; c; ∃!; x, y, z; c; x, y; c; □; x, y; c; x; c; □; x, y, z; c; x, y; c]

3.6 The Beck-Chevalley condition

[figure: x, y; a; x, y, z; a; S_{g′}; x, y, z; a; x, z; y, a; Σ_{f′}; x, y; a; x; y, a; Σ_{f}; x; y, a; x, z; y, a; S_{g}; x, z; y, a; x, z; y, a; x, y; a; •; x, y, z; x, y; g′; x, y; x; f; x, y, z; x; h; x, y, z; x, z; f′; x, z; x; g]

[figure: x, y; a; x, y; a; id; x, y; a; x; y, a; Σ_{f}; x; y, a; x, y; a; S_{f}; x, y; a; x, y, z; a; S_{g′}; x; y, a; x, y, z; a; S_{h}; x; y, a; x, z; y, a; S_{g}; x, z; y, a; x, y, z; a; S_{f′}; x, y, z; a; x, z; y, a; Σ_{f′}; x, z; y, a; x, z; y, a; id; •; •; •; •]

{(x, y; a)^{Σ_{f}} ↦ (x, y; a)^{Σ_{f}} \atop (x, y; a) ↦ (x, y; a)^{Σ_{f} S_{f}}} ; (x, y; a)^{S_{g′}} ↦ (x, y; a)^{Σ_{f} S_{f} S_{g′}} ; (x, y; a)^{S_{g′}} ↦ (x, y; a)^{Σ_{f} S_{g}S_{f′}} ; (x, y; a)^{S_{g′} Σ_{f′}} ↦ (x, y; a)^{Σ_{f} S_{g}}  {(x; y, a) ↦ (x; y, a) \atop (x, y; a) ↦ (x, y; a)} ; (x, y, z; a) ↦ (x, y, z; a) ; (x, y, z; a) ↦ (x, y, z; a) ; (x, z; y, a) ↦ (x, z; y, a)

2002h (typeset 2002dec30 19:22) Edrx http://angg.twu.net/

4 A natural deduction system for topos logic

parte 3: A natural deduction system for topos logic. Set as a topos, subobject fibrations, Bell/LST for subobject fibrations, dependent types.

5 The syntactical world and the real world

parte 4: Moving constructions in System DNC from the syntactical world to real world. Representing logic in λC. Parametricity in λC. (...)

6 Infinitesimals

In the example of the (1 + a/n)^{n}, each passage f(a + o) = f(a) + o′ or similar corresponds to construct the value of f(a)+o′ (that depends on o) and to prove that f(a + o) = f(a) + o′.

Show how to adapt the dictionary to support filter-infinitesimals Show (briefly, with a few examples) how that can be adapted to make a

language that deals with multi-functions Discuss the geometric morphism between Set^{𝕀} and Set Discuss the logical morphism from Set^{𝕀} to Set^{F} Derive a transfer theorem from this Show how to lift a proof in Set^{F} — that is a quotient of Set^{𝕀} — back to

one in Set^{𝕀}, by taking representatives; most operations (all?) allow a natural choice of the representative to take

Show how to change the F to introduce or discharge a natural infinitesimal; there is a fibration involved

6.1 Natural infinitesimals

The definition of infinitesimal that appeared in section extends naturally to topological spaces. Fix a “base point” x_{0} ∈ X, and let’s declare that it plays the role of the zero point in X — so that instead of having to say “y ∈ X is infinitely close to x_{0}” we will be allowed to say just “y is an infinitesimal”. We will say that a pre-hiper-x x (that is, 𝕚 ↦ x_{𝕚}) is an infinitesimal when for every neighbourhood V of x_{0} we have that x_{𝕚} ∈ V is F-true, i.e., that for every V ∈ V_{x_{0}} we have that x_{𝕚} ∈ V is true in a big set of indices.

If 𝕀 = X is a topological space and x_{0} is a point of X, then the “identity prehiper-x” 𝕚 →^{id} x is an infinitesimal if F is taken to be the filter of neighbourhoods of x_{0} in X. This is trivial to see: for any V ∈ V_{x_{0}} ⊂ P(X) the set of indices where x_{𝕚} ∈ V is exactly V ⊂ 𝕀, which, being a neigbourhood of x_{0}, is a big set by definition.

If X is Hausdorff then we can also choose 𝕀 = X\{ x_{0} } and F = V_{x_{0}}^{∗}, and the identity-pre-hiper-x will still be infinitely close to x_{0}.

The identity pre-hiper-x in either of these two cases, F = V_{x_{0}} or V_{x_{0}}^{∗}, will be called the natural infinitesimal on X — or the “natural point infinitesly close to x_{0}” if we need to be more explicit.

If X is a normed vector space then a common way to add a point at the infinity to X (obtaining a topological space X^{∗}) is to define that the neighbouhoods of ∞ ∈ X^{∗} are the sets of the form { ∞ }∪A, where A ⊂ X contains some B_{K} := { x ∈ X | |x| > K }; then if we choose 𝕀 = X and F = V_{∞}^{∗} the identity pre-hiper-x becomes a point infinitely close to ∞. This gives rise, in the case 𝕀 = ℝ and F = V_{∞}^{∗}, to what we could call the “natural infinite (pre-)hiperreal”, and in the case 𝕀 = ℕ and F = V_{∞}^{∗} (lifting the restriction that X must be a vector space) to the “natural infinite (pre-)hipernatural”.

Every infinitesimal on X with index set 𝕀′ factors uniquely through the natural infinitesimal on X in a unique way, that is, there is a unique function 𝕚′ → 𝕚, continuous in a certain sense, such that 𝕚′ → 𝕚 →^{id} x is the original infinitesimal, but this won’t interest us much now; what is really important is the connection between infinitesimal, natural infinitesimals and continuous functions that is the subject of the next section.

6.2 The translation from SSA to standard

6.2.1 The key theorem on natural infinitesimals

One of the most famous basic theorems of non-standard analysis says that a standard function f is continuous at a standard point x_{0} iff^{1} it takes every hyperpoint infinitely close to x_{0} to a hyperpoint infinitely close to f(x_{0}); in SSA this idea appears in two flavours, and one of them uses natural infinitesimals.

In all of this section f : X → Y and x_{0} ∈ X are standard, and “p.i.c.” is “point infinitely close”. The key theorem is:

(i) f is continuous at x_{0}

⇔ (ii) f takes every p.i.c. to x_{0} to a p.i.c. to f(x_{0}) (∀𝕀, ∀F)

⇔ (iii) f takes the natural p.i.c. to x_{0}, x_{1}, to a p.i.c. to f(x_{0}).

Proof:

(i) ⇒ (ii): f(x_{1}) is a p.i.c. to f(x_{0}) ⇔ ∀V standard neighbourhood of f(x_{0}) we have (f(x_{1}) ∈ V)_{/F} = ⊤; but f(x_{1}) ∈ V is true exactly on the inverse of V by f, that is a neighbourhood of x_{0} as f is continuous at x_{0}.

(i) ⇒ (iii): a particular case of (i) ⇒ (ii).

¬(i) ⇒ ¬(iii): If f is not continuous at x_{0} then there exists a neighbourhood V of f(x_{0}) such that f^{−1}(V) is not a neighbourhood of x_{0}; f(x_{1}) ∈ V is true exactly in f^{−1}(V) ⊂ 𝕀, that is not a neighbourhood of x_{0}, and so (f(x_{1}) ∈ V)_{/F} ≠ ⊤.

¬(i) ⇒ ¬(ii): use the natural infinitesimal as counterexample (recycle ¬(i) ⇒ ¬(iii)).

And adapting the key theorem to limits we get: lim_{x→x_{0}} f(x) = a ⇔ f takes the natural p.i.c. to x_{0} (now using punctured neighbourhoods) to

1one of the directions of the “iff” depends on using a U that is non-trivial enough.

2002h (typeset 2002dec30 19:22) Edrx http://angg.twu.net/

a p.i.c. to a.

6.2.2 An example of a calculation with infinitesimals

As an example of how to use the key theorem we show how that lim_{n→∞}(1 + \frac{x}{n})^{n} = e^{x}, and how to translate the demonstration back to something standard.

The idea of the proof is to replace n by the natural infinite hyper-natural, ω = (1, 2, 3, …), and to see that the difference between (1 + \frac{x}{ω})^{ω} and e^{x} is an infinitesimal; every equality below must be seen as being valid in a big set of indices, i.e., for every 𝕚 above a certain k. Some steps require Taylor’s formula.

log(1 + \frac{x}{ω})^{ω} = ω log(1 + \frac{x}{ω})
= ω (log 1 + ((log′ 1) + o_{1}) \frac{x}{ω})
= ω (0 + (1 + o_{1}) \frac{x}{ω})
= ω (1 + o_{1}) \frac{x}{ω}
= (1 + o_{1}) x
(1 + \frac{x}{ω})^{ω} = e^{((1+o_{1}) x)}
= e^{(x+o_{1}x)}
= e^{(x+o_{2})}
= e^{x} + o_{3}.

Each time a new symbol was introduced we were meaning that it was coming with an implicit quantifier sentence attached (each “...” means “such that the corresponding ‘=’ is F-true”):

∀ω p.i.c. to ∞ in ℕ ∃o_{1} p.i.c. to 0 in ℝ... ∀o_{1} p.i.c. to 0 in ℝ ∃o_{2} p.i.c. to 0 in ℝ... ∀o_{2} p.i.p. 0 em ℝ ∃o_{3} p.i.p. 0 em ℝ... The passage to standard is done by a simple “dictionary trick”: ω = ω(𝕚) (identity) o_{1} = o_{1}(𝕚) o_{2} = o_{2}(𝕚) o_{3} = o_{3}(𝕚) Where: lim_{𝕚→∞}ω(𝕚) = ∞ lim_{𝕚→∞}o_{1}(𝕚) = 0 lim_{𝕚→∞}o_{2}(𝕚) = 0 lim_{𝕚→∞}o_{3}(𝕚) = 0 6.2.3 Another example: Hamiltonians

For example, this — a calculation using “differentials” that will sound perfectly natural to a physicist and perfectly mystical to most mathematicians.

Start with a function τ → q and a function t, q, r → L; r is meant to be the derivative q_{t}, but not in all contexts; so we introduce a new variable τ, with τ → t being the identity and r being equal to q_{τ} when the composite τ → t → t, q, r makes sense; when we forget that the function τ → t exist there will be no restriction on t → q, r, and we won’t consider that there is an arrow t → τ, as that would spoil some naturality considerations.

We introduce two new variables,

p := L_{r},

H := p r − L;

and a change of variables t, q, r ↔ t′, q′, p′; the primes will be used to let us talk of partial derivatives like L_{q} and L_{q′} making clear which variables of (t, q, r) and (t′, q′, p′) are not changing.

If we know ⟨1⟩(t, q, r) we know ⟨1⟩p, ⟨1⟩L, ⟨1⟩H, ⟨1⟩L_{r}, etc.; moreover,

dH = dp r + p dr − dL
= r dp + L_{r}dr − L_{t}dt − L_{q}dq − L_{r}dr
= r dp − L_{t}dt − L_{q}dq,

is true if all ‘=’s are interpreted are being equivalences up to order 1, and so H_{t′} = −L_{t} = p, H_{q′} = −L_{q}, H_{p′} = r. [There are many details missing.]

6.3 The Inverse Function Theorem and its friends

If x → y is a smooth function from ℝ^{n} → ℝ^{n}, with invertible derivative in the point x_{0}, then the inverse function theorem says that there is a smooth function y → x that is a local inverse of x → y:

\begin{aligned}x_{0} & x → y \\ & y → x \end{aligned}

Two important corollaries of this can be seen as being just constructions using this rule: the local form of immersions (t → x, y is an immersion, and t → x is invertible) and the implicit function theorem (x, y → f, and we want a function x → y that keeps f constant = f_{0}, where f_{0} = f(x_{0}, y_{0})).

\begin{matrix}\begin{aligned}t & {t → x, y \atop t → x} \\ & x → t \end{aligned}IFT & t → x, y \\ x → y \end{matrix}  \begin{aligned}\begin{aligned}x, y & x, y → f \\ & f \end{aligned} & \begin{matrix}x, y & x, y → f \\ f → (x → y) \end{matrix} IFT \\ & x → y \end{aligned}

2002h (typeset 2002dec30 19:22) Edrx http://angg.twu.net/

Just as a curiosity, here are the normal forms for two deductions above:

\begin{matrix}\begin{aligned}[x]^{2} & \begin{aligned}t & \begin{aligned}[t]^{1} & t → x, y \\ & x, y \end{aligned} ; x ; t → x ; 1 \\ & x → t \end{aligned} ; T F I \\ & t \end{aligned} & t → x, y \\ x, y \end{matrix} ; y ; x → y ; 2

\begin{aligned}\begin{aligned}x, y & x, y → f \\ & f \end{aligned} & \begin{aligned}{x, y \atop y} & \begin{aligned}\begin{matrix}[x]^{2} & [y]^{1} \\ x, y \end{matrix} & x, y → f \\ & f \end{aligned} ; y → f ; 1 \\ & f → y \end{aligned} ; T F I \\ & y \end{aligned} ; x → y ; 2

2002h (typeset 2002dec30 19:22) Edrx http://angg.twu.net/

7 Glossary

7.1 The notation of generic points and “spaces ofs”

E[x] ≡ X:Sets  the space (or set) of ‘x’s
x:E[x]  an x
x′:E[x]  another x

E[x↦y] := (E[x] → E[y]):Sets the space of the functions that expect ‘x’s and return ‘y’s

(x↦y):E[x↦y]  a function that expects an ‘x’ and returns a ‘y’
(x↦y)(x)  function application
y := (x↦y)(x)  a definition (by a natural construction) for y
{E[x, y] := \atop (E[x] × E[y]):Sets} the space of the pairs formed by an ‘x’ and a ‘y’
(x, y):E[x, y]  a pair
x := π_{1}(x, y)  first projection
y := π_{2}(x, y)  second projection
(x↦y) := λx:X.y  lambda

\begin{aligned}x & x↦y \\ & y \end{aligned}

(definition by) natural construction;

seeing trees as terms

7.2 Functors and natural transformations in Set

x ⇒ x, y  the functor that takes each E[x] to E[x, y]

x ⇒^{−−} x, y the proto-proto-functor associated to x ⇒ x, y; just the action of x ⇒ x, y on objects, i.e., E[x]↦E[x, y]

x ⇒^{−} x, y the protofunctor associated to x ⇒ x, y: x ⇒^{−−} x, y plus the action on morphisms

x →^{•}^{−} (x, y↦x, z) a proto-natural transformation from x ⇒^{−−} x, y to x ⇒^{−−} x, z, i.e., an operation E[x]↦(x, y↦x, z)

x →^{•} (x, y↦x, z) a natural transformation: a x →^{•}^{−} (x, y↦x, z) plus a proof that it obeys an equation on squares

7.3 Truth-values, witnesses, propositions, proofs

Ω the classifier object; the set/class/sort of truth-values

ω:Ω  a truth-value

ω[P]:Ω the truth-value of P; the set of witnesses that P is true

⊤[P]:ω[P]  a witness that P is true

PI the axiom of proof-irrelevance for Ω: ∀ω[P]:Ω.∀⊤[P]:ω[P].∀⊤[P]′:ω[P].(⊤[P] = ⊤[P]′)

Props  the class/sort of propositions

Prfs[P]:Props the proposition P, regarded as the set of its proofs

prf[P]:Prfs[P]  a proof of P
prf[P]′:Prfs[P]  another proof of P
Props ≡ Ω  the sorts Props and Ω will be collapsed
Prfs ≡ ω, prf ≡ ⊤  same

7.4 Connectives and quantifiers

Prfs[P [figure]Q] := Prfs[P] → Prfs[Q]

the space of the proofs that P implies Q

prf[P [figure]Q] ≡ (prf[P]↦prf[Q])

a proof of P implies Q

Prfs[∀x.P (x)] := Σx:E[x].Prfs[P (x)]

the space of the proofs that ∀x(∈ E[x]).P (x)

{prf[∀x.P (x)] ≡ \atop (x↦prf[P (x)])}  a proof of ∀x(∈ E[x]).P (x)

Prfs[P ∧ Q] := Prfs[P] × Prfs[Q]

the space of the proofs that P ∧ Q

prf[P ∧ Q] ≡ (prf[P], prf[Q]) a proof of P ∧ Q

7.5 Categories

C  a (small) category
Objs_{C}  the class of objects of C (a sort)
O[a]:Objs_{C}  an object of C (the “‘objects of ‘a’s”)

a:O[a] THIS IS USUALLY NOT ALLOWED! a is just a “pseudo-point” of O[a] — just a syntactical device.

O[b], O[c] : Objs_{C}  two other objects of C

E[a↦b] := Hom_{C} O[a]O[b] the space (a set) of all morphisms in C from O[a] to O[b]

(a↦b):E[a↦b]  a morphism from O[a] to O[b]
O[a] → O[b]  another way of writing Hom_{C} O[a]O[b]
(a↦a) := id_{C}O[a]  the identity morphism for O[a]
Cat[a] ≡ C  the category where O[a] lives

Cat^{−−}[a] = C^{−−} the proto-proto-category associated to C: just Objs_{C}

(a↦c) := (a↦b↦c) := ; (b↦c) ∘_{C} (a↦b) := ; ∘_{C} O[a]O[b]O[c] ; (a↦b)(b↦c) composition in C

Cat^{−}[a] ≡ C^{−} the protocategory associated to C: Objs_{C} plus Hom_{C}, id_{C} and ∘_{C}

ω[(a↦^{f}c) = (a↦^{g}c)] := Eq_{C}O[a]O[b] (a↦^{f}c)(a↦^{g}c) comparison of morphisms in the same hom-set is done by using a term Eq_{C}; Eq_{C} is usually the Leibniz equality

Cat[a] ≡ C a category C is encoded as a protocategory C^{−} plus an Eq_{C} and terms for the “non-syntactical equations”, assoc_{C}, idL_{C} and idR_{C}

7.6 Functors

a ⇒ a^{F}  a functor from Cat[a] to Cat[a^{F}]

O[a^{F}] := (a ⇒ a^{F})_{O}(O[a]) the image of the object O[a] by the (action on objects of the) functor a ⇒ a^{F}

(a′^{F} ↦a′′^{F}) := (a ⇒ a^{F})_{M}(a′↦a′′) the image of the morphism a′↦a′′ by the (action on morphisms of the) functor a ⇒ a^{F}

a ⇒^{−−} a^{F} the proto-proto-functor associated to a ⇒ a^{F}; just (a ⇒ a^{F})_{O}

a ⇒^{−} a^{F} the protofunctor associated to a ⇒ a^{F}; a ⇒^{−−} a^{F} plus (a ⇒ a^{F})_{M}

a ⇒ a^{F} a functor a ⇒ a^{F} is a protofunctor a ⇒^{−} a^{F} plus terms respids_{C} and respcomp_{C}, that assert that a ⇒^{−} a^{F} respects identities and composition

7.7 Natural Transformations

a →^{•} (a^{F} ↦a^{G})  a natural transformation from a ⇒ a^{F} to a ⇒ a^{G}

a →^{•}^{−} (a^{F} ↦a^{G}) the proto-natural transformation associated to a →^{•} (a^{F} ↦a^{G}); just an operation O[a]↦(a^{F} ↦a^{G}), without the proof of the condition on squares

a ↔ b  an iso between O[a] and O[b]

a ↔^{−} b a protoiso; just an a↦b and a b↦a, without the proof that their composites are identities

a →^{•} (a^{F} ↔ a^{G})  a natural isomorphism

7.8 The opposite of a category

Cat[a^{op}] := Cat[a]^{op} opposite (or dual) category
O[a^{op}] := O[a]  the objects are the same as in Cat[a]
(a^{op}↦b^{op}) := (b↦a) but the arrows are reversed

7.9 Categories of functors

Cat[a ⇒ b] := Cat[b]^{Cat[a]} the category whose objects are the functors from Cat[a] to Cat[b]

O[a ⇒ a^{F}]  the functor a ⇒ a^{F}, seen as an object of Cat[a ⇒ a^{F}]
(a ⇒ a^{F})↦(a ⇒ a^{G}) a natural transformation a →^{•} (a^{F} ↦a^{G}) in disguise

7.10 The product of two categories

Cat[a; b] := Cat[a] × Cat[b]

the product of the categories Cat[a] and Cat[b]

O[a; b] := (O[a], O[b]) an object of Cat[a; b] is a pair made of an object of Cat[a] and an object of Cat[b]

(a′; b′)↦(a′′; b′′)  a pair of morphisms (a′↦a′′), (b′↦b′′)

7.11 Hom and Yoneda

b ⇒ (a↦b)  Hom_{Cat[a]}(O[a], −), a functor from Cat[a] to Set

a^{op} ⇒ (a↦b)

Hom_{Cat[b]}(−, O[b]), a contravariant functor from Cat[a] to Set

a ⇒_{f&f} a^{F} or [figure: a; a^{F}; a; b; a^{F}; b^{F}; b; b^{F}] “a ⇒ a^{F} is full and faithful”; a ⇒ a^{F} plus a proof that its action on morphisms is bijective in each hom-set, i.e.,

(a^{op}; b) →^{•} ((a↦b) ↔ (a^{F} ↦b^{F})).

[figure: x; (a↦x); x; x^{F}; (a↦x); x^{F}; x; •; a^{F}] The Yoneda lemma,

(a^{op}; x ⇒ x^{F}) →^{•} ((x →^{•} ((a↦x)↦x^{F})) ↔ a^{F}),

in diagrammatic form. Note that the diagram is a bit misleading: the points of E[a^{F}] are in bijection with the natural transformations x →^{•} ((a↦x)↦x^{F}), not with the morphisms (a↦x)↦x^{F}.

[figure: x; (a↦x); x; (b↦x); (a↦x); (b↦x); x; •; a^{op}; b^{op}; a^{op}; (a↦x); b^{op}; (b↦x)] The Yoneda embedding, a^{op} ⇒_{f&f} (x ⇒ (a↦x)), i.e.,

(a^{op}; b) →^{•} ((a↦b) ↔ (x →^{•} ((x↦a)↦(x↦b)))),

in diagrammatic form

7.12 Adjunctions

[figure: a^{L}; a; a^{L}; b; a; b^{R}; b; b^{R}] an adjunction L ⊣ R, i.e., (a ⇒ a^{L}) ⊣ (b ⇒ b^{R}).

It can be written as a natural isomorphism as

(a^{op}; b) →^{•} ((a^{L}↦b) ↔ (a↦b^{R})).

a →^{•} (a↦a^{LR})  the unit of the adjunction L ⊣ R
b →^{•} (b^{RL}↦b)  the counit of the adjunction L ⊣ R

[figure: x; x; x; x; x; a; b; x; a, b; a; b; a, b] binary products in a category, described via an adjunction.

[figure: a, b; a, b; a, b; a, b; a, b; a; b; a, b; a, b; a; b; a, b] the projections a, b↦a and a, b↦b coming from the

counit, (a^{op}; b) →^{•} ((a, b; a, b)↦(a; b)). Note: the unit x →^{•} (x↦x, x) gives the diagonal maps.

[figure: i ⇒ x; x; i ⇒ x; i ⇒ a_{i}; x; (i ⇒ a_{i})^{Lim}; i ⇒ a_{i}; (i ⇒ a_{i})^{Lim}] the functor (i ⇒ a_{i}) ⇒ (i ⇒ a_{i})^{Lim}, that gives a “limit” for each diagram of shape Cat[i] in a category Cat[a_{i}], can be seen as the right adjoint to the “constant” functor.

[figure: \begin{aligned}& & x \\ & & ↓ \\ x & → & x \end{aligned}; x; \begin{aligned}& & x \\ & & ↓ \\ x & → & x \end{aligned}; \begin{aligned}& & a \\ & & ↓ \\ b & → & c \end{aligned}; x; (a, b)|_{c}; \begin{aligned}& & a \\ & & ↓ \\ b & → & c \end{aligned}; (a, b)|_{c}]  a particular case of limit: pullbacks.

[figure: a, b; a; a, b; c; a; b↦c; c; b↦c] exponentiation by O[b] is defined by taking a right adjoint to a ⇒ a, b

7.13 The “such that” bar and the “is well-defined” symbol

E[a|_{P (a)}] ≡ {a ∈ A|P (a)} := Σa:A.⊤[P (a)] comprehension: the space of the ‘a’s such that P (a) is true

a|_{P (a)}  an a such that P (a) is true

wd(α)

“α is well-defined”; an abbreviation for α_{1} = α_{2} = … = α_{n}, where α_{1}, α_{2}, …, α_{n} are natural constructions for α

7.14 Arrow categories

{Cat[b↦\underline{c}] ≡ \atop Cat[a]\O[b]}  the category of arrows under O[b]

O[b↦\underline{c}] := (O[c], b↦c) an object of Cat[b↦\underline{c}] is pair formed by an object O[c] and an arrow b↦c

(b↦\underline{c′})↦(b↦\underline{c′′}) := (c′↦c′′)|_{wd(b↦c′′)} a morphism from O[b↦\underline{c′}] to O[b↦\underline{c′′}] is an arrow c′↦c′′ making the obvious triangle commute

{Cat[\underline{a}↦b] ≡ \atop Cat[a]/O[b]}  the category of arrows over O[b]

O[\underline{a}↦b] := (O[a], a↦b) an object of Cat[\underline{a}↦b] is pair formed by an object O[a] and an arrow a↦b

(\underline{a′}↦b)↦(\underline{a′′}↦b) := (a′↦a′′)|_{wd(a′↦b)} a morphism from O[\underline{a′}↦b] to O[\underline{a′′}↦b] is an arrow a′↦a′′ making the obvious triangle commute

{Cat[\underline{a}↦\underline{b}] ≡ \atop Cat[a]^{•→•}}  the category of arrows of Cat[a]

O[\underline{a}↦\underline{b}] := (O[a], O[b], a↦b) an object of Cat[\underline{a}↦\underline{b}] is triple formed by two objects of Cat[a] and an arrow between them

(\underline{a′}↦\underline{b′})↦(\underline{a′′}↦\underline{b′′}) := ((a′↦a′′), (b′↦b′′))|_{wd(a′↦b′′)} a morphism from O[\underline{a′}↦\underline{b′}] to O[\underline{a′′}↦\underline{b′′}] is a pair

of arrows a′↦a′′ and b′↦b′′ making the obvious square commute

7.15 Monics, subobjects and the classifier object

x ↪ y  an injective function, or a monic in Set
b ↪ c  a monic arrow in a category

Sub(Cat[b])

≡ Cat[\underline{b′} ↪ b] the category of subobjects of O[b], i.e., the category of monic arrows with codomain O[b]

(\underline{b′} ↪ b)↦(\underline{b′′} ↪ b) ≡ (\underline{b′} ↪ b) ↪ (\underline{b′′} ↪ b) if there is an arrow b′↦b′′ making the obvious triangle commute, it will be unique and monic (every category of subobjects is a preorder)

⊤ ↪ ω ≡ true:E[⊤↦ω] the “true” arrow from the terminal object O[⊤] to the classifier object O[ω]; in Set we have O[⊤] = E[⊤] = {⊤} and O[ω] = E[ω] = {⊤, Ⅎ} and ⊤ ↪ ω is the canonical inclusion

(b↦ω[P (b)])↦ O[\underline{b|_{P} (b)} ↪ b] the operation (pullback with ⊤ ↪ ω) that takes an arrow that gives for any b the truth-value of P (b), and returns the “set of ‘b’s such that P (b) is true” — a subobject of O[b]

(O[\underline{b′} ↪ b)↦ (b↦ω[b ∈ \{b′\}]) the “classifier rule”: for any b′ ↪ b there is a (unique) arrow b↦ω that makes the obvious square a pullback

7.16 Fibrations

\begin{matrix}E \\ ↓ \\ B \end{matrix} or \begin{matrix}a_{i} \\ ⇓ \\ i \end{matrix} or a_{i} ⇒ i  a fibration
O[i]:Objs_{Cat[i]}  an object of the base category
O[a_{i}]:Objs_{Cat[a_{i}]}  an object of the total category
O[a_{i}]  an object over O[i]
O[b_{i}], O[a′_{i}]  other objects over O[i]

a_{i}↦b_{i} a “vertical morphism” over O[i]: a morphism whose image by a_{i} ⇒ i is the identity on O[i]

Cat[a_{i}] if O[i] is free: the total category if O[i] is known: the fiber over O[i]

b_{j}↦c_{k}  a morphism over j↦k

cart(b_{j}↦c_{k}) the universal property that says that b_{j}↦c_{k} is cartesian:

a_{i}^{op} →^{•} ((a_{i}↦b_{j}) ↔ ((i↦j), (a_{i}↦c_{k}))|_{wd(i↦k)}).

Note that the ‘↦’ direction of the NT is automatic.

b_{j}↦^{□}c_{k} a “horizontal morphism over j↦k”, i.e., a cartesian morphism over j↦k

((j↦k), O[c_{k}])↦ (O[c_{j}], (c_{j}↦^{□}c_{k})) a cleavage for a_{i} ⇒ i: an operation that chooses for any j↦k and any O[c_{k}] a “cartesian lifiting” c_{j}↦c_{k} for j↦k

7.17 Inverting the vertical structure of a fibration

a_{i}^{vop} ⇒ i the fibration obtained from a_{i} ⇒ i by flipping the vertical arrows and keeping the horizontal arrows unchanged

O[a_{i}^{vop}] := O[a_{i}] the objects of Cat[a_{i}^{vop}] are the same as the objects of Cat[a_{i}]

a_{i}^{vop}↦b_{i}^{vop} := b_{i}↦a_{i} vertical morphisms (i.e., morphisms in a fiber over an O[i]) are flipped; Cat[a_{i}^{vop}] = Cat[a_{i}]^{op}

b_{i}^{vop}↦^{□}b_{j}^{vop} := b_{i}↦^{□}b_{j} the horizontal morphisms of Cat[a_{i}^{vop}] — i.e., the cartesian liftings of an i↦j on an O[b_{j}] = O[b_{j}^{vop}] — are defined as being the same as in the original total category

(a_{i}^{vop}↦b_{j}^{vop}) :=

(a_{i}^{vop}↦b_{i}^{vop}↦^{□}b_{j}^{vop}) morphisms in the total category Cat[a_{i}^{vop}] are expressed as composites of vertical morphisms and horizontal morphisms; note that this composition is purely formal, as

(a_{i}^{vop}↦b_{i}^{vop}↦^{□}b_{j}^{vop}) = (a_{i} ← b_{i}↦^{□}b_{j}).

Two such “composites” are considered equal, i.e., (a_{i}^{vop}↦b_{i}^{vop}↦^{□}b_{j}^{vop}) = (a_{i}^{vop}↦b′_{i}^{vop}↦^{□}b_{j}^{vop}), if there is a vertical iso b_{i}^{vop} ↔ b′_{i}^{vop}(= b_{i} ↔ b′_{i}) making the obvious diagram commute.

opfib(a_{i} ⇒ i) the functor a_{i} ⇒ i is an “opfibration”, i.e., a_{i}^{vop} ⇒ i is a fibration

(a_{i} ⇒ i)|_{opfib}  a functor a_{i} ⇒ i plus a proof that it is an opfibration

7.18 The 2-category Cats

O[cat[a]]:Cats, O[cat[a]] := Cat[a] a category Cat[a] can be regarded as an object of the 2-category of categories

{cat[a]↦cat[b] := \atop a ⇒ b}  a morphism in Cats is a functor

E[cat[a]↦cat[b]] :=

Objs[Cat[a] ⇒ Cat[b]] the hom-sets in Cats are the classes of objects of categories of functors

O[cat[a], cat[b]] := Cat[a] × Cat[b] the product of two categories Cat[a] and Cat[b], seen as an object of Cats, plays the role of the product of the two objects O[cat[a]] and O[cat[b]

O[cat[a]↦cat[b]] := Cat[a]↦Cat[b] an exponential object in Cats corresponds to the exponential of two categories, i.e., the category of functors between them

7.19 The 2-category of fibrations over a given base category

O[fib_{i}[a_{i}]] a fibration a_{i} ⇒ i, regarded as an object of the category of fibrations over Cat[i]

fib_{i}[a_{i}]↦fib_{i}[b_{i}] ≡ (a_{i} ⇒ b_{i})|_{cart_{i}} a morphism from O[fib_{i}[a_{i}]] to O[fib_{i}[b_{i}]] is a functor a_{i} ⇒ b_{i} that is cartesian over Cat[i], i.e., it makes the obvious triangle of functors commute and it carries cartesian morphisms in Cat[a_{i}] to cartesian morphisms in Cat[b_{i}]

E[fib_{i}[a_{i}]↦fib_{i}[b_{i}]] ≡ Objs[Cat[ (a_{i} ⇒ b_{i})|_{cart_{i}}]] Cat[fib_{i}[a_{i}]] is a 2-category, so an hom-set in it corresponds to the class of objects of a category of functors cartesian over Cat[i]

O[fib_{i}[a_{i}], fib_{i}[b_{i}]] := (a_{i}; b_{i}) ⇒ i the product of two objects O[fib_{i}[a_{i}]] and O[fib_{i}[b_{i}]] is given by the the pullback of the functors a_{i} ⇒ i and b_{i} ⇒ i

O[fib_{i}[a_{i}]↦fib_{i}[b_{i}]] the exponential of two objects is given by a construction (page ...) that resembles the construction of exponentials in a category Set^{C}

7.20 The category of contexts

x, y, z a context; it corresponds to x:X(), y:Y (x), z:Z(x, y), where X(), Y (x) and Z(x, y) are terms that can only have as free variables the ones listed inside parentheses. The idea is that X(), Y (x) and Z(x, y) can be recovered by looking for the dictionary entries for E[x], E[y] and E[z].

Cat[x, y, z] ≡ Ctxt the “category of contexts”; its objects are the wellformed contexts like x:X(), y:Y (x), z:Z(x, y) (that we usually write in contracted form, as x, y, z), and morphisms between two contexts are “procedures for obtaining the value of each variable in the second context from the values of the variables in the first context”. Intuitively, O[x, y, z] is “the space of all possible values for the triple (x, y, z)”.

x, (y, z) a packed version of the context x, y, z: it corresponds to x:X(), (y, z):(Σy:Y (x).Z(x, y)).

x, y, z ↦^{w:=f(x,y,z)}x, y, w the morphism that represents x:X(), y:Y (x), z:Z(x, y) ⊢

f(x, y, z):W (x, y). Note that W (x, y) can’t depend on z.

x, y, z↦x, y, f(x, y, z) the same as above; the name of the last variable of a context is never used (except for obtaining its ‘E’), so we allow writing a term in its place.

x, y, z↦x, y a “display morphism”, i.e., one that with the right packing corresponds to a first projection. If Z(x, y) is a member of the sort △ then x, y, z↦x, y represents x:X(), y:Y (x) ⊢ Z(x, y):△.

O[x, y; z] the morphism x, y, z↦x, y, seen as an object of Ctxt^{→}. We usually see Ctxt^{→} as being fibred over Ctxt by Cod : Ctxt^{→} → Ctxt, i.e., by (a; b) ⇒ a, so O[x, y; z] is also an object of the fiber over O[x, y].

7.21 Internal categories

Cat[\underline{a}] the internal category where O[\underline{a}] lives; it is a diagram in a category — in C, say.

O[O[\underline{a}]]:Objs_{C}  the object of objects of Cat[\underline{a}]
{O[O[\underline{b}]] := O[O[\underline{c}]] := \atop O[O[\underline{a}]]} other names for the same object of objects
O[\underline{a}↦\underline{b}] : Objs_{C}  the object of morphisms of Cat[\underline{a}]
O[\underline{a}]↦(\underline{a}↦\underline{a})  the identity arrow (“i”)
(\underline{b}↦\underline{c})↦O[\underline{b}]  the domain arrow (“d_{0}”)
(\underline{b}↦\underline{c})↦O[\underline{c}]  the codomain arrow (“d_{1}”)

O[\underline{a}↦\underline{b}↦\underline{c}] := O[(\underline{a}↦\underline{b}), (\underline{b}↦\underline{c})|_{O[\underline{b}]}] the object of composable arrows of Cat[\underline{a}] is defined by pullback

(\underline{a}↦\underline{b}↦\underline{c})↦(\underline{a}↦\underline{b})  first projection of the pullback “d̂_{0}”
(\underline{a}↦\underline{b}↦\underline{c})↦(\underline{b}↦\underline{c})  second projection of the pullback “d̂_{1}”
(\underline{a}↦\underline{b}↦\underline{c})↦(\underline{a}↦\underline{c})  the composition arrow (“c”)

Cat[\underline{a}] := O[\underline{a}] [figure] (\underline{b}↦\underline{c}) [figure] (\underline{d}↦\underline{e}↦\underline{f}) an internal category Cat[\underline{a}] in C is a diagram in C with three objects and six morphisms obeying certain conditions

Cat[\underline{a^{F}}]  another internal category in C

\underline{a} ⇒ \underline{a^{F}} a functor from Cat[\underline{a}] to Cat[\underline{a^{F}}] is a pair of morphisms of C, O[\underline{a}]↦O[\underline{a^{F}}] and (\underline{b}↦\underline{c})↦(\underline{b^{F}} ↦\underline{c^{F}}) that induce an (\underline{a}↦\underline{b}↦\underline{c})↦(\underline{a^{F}} ↦\underline{b^{F}} ↦\underline{c^{F}}) by pullback and such that these morphisms commute with the ones in the definition of Cat[\underline{a}] and Cat[\underline{a^{F}}]

\underline{a} →^{•} (\underline{a^{F}} ↦\underline{a^{G}}) a natural transformation between \underline{a} ⇒ \underline{a^{F}} and \underline{a} ⇒ \underline{a^{G}} is a morphism O[\underline{a}] →^{•} (\underline{a^{F}} ↦\underline{a^{G}}) obeying the obvious commutativity conditions

O[cat[\underline{a}]] the internal category Cat[\underline{a}] regarded as an object of the 2-category of internal categories in C

cat[\underline{a}]↦cat[\underline{a^{F}}]  \underline{a} ⇒ \underline{a^{F}} in disguise
(\underline{a} ⇒ \underline{a^{F}})↦(\underline{a} ⇒ \underline{a^{G}}) \underline{a} →^{•} (\underline{a^{F}} ↦\underline{a^{G}}) in disguise

7.22 DNC notation for λ2

a↦b↦c := a↦(b↦c) in this section something like a↦b↦c means a curried function of two arguments, not the composite of a↦b and b↦c

E[a]:∗ a generic member of *; we can use E[a] as a name for a variable or for a term, and we have E[E[a]] = ∗.

E[a↦b]:∗ a non-generic member of *; E[E[a↦b]] = ∗, but not every member of the * is a space of functions, so using E[a↦b] in a situation like λE[a↦b]: ∗ . ... would be misleading, and we forbid that. E[a↦b] can only stand for a term, not for a variable.

E[α]: ∗ E[β]:∗ α and β are names of “expressions of class *-2” — for example α := (E[a]↦a)↦b, β := c. E[α] and E[β] are terms of class *-1.

E[α↦β] :=

E[α] → E[β] E[E[a]↦β] :=

ΠE[a]: ∗ .E[β] the rules that translate each E[α] to a term involving only E[a]’s, E[b]’s, and the ∗. Example: E[(E[a]↦a)↦(b↦c)] becomes (ΠE[a]: ∗ .E[a]) → (E[b] → E[c]), i.e., (ΠA: ∗ .A) → (B → C).

α:E[α] the meaning of an α:E[α] will depend on the context; α can be a variable or a specific term. For example, in (a↦a↦a):E[a↦a↦a] the (a↦a↦a) can be λa:E[a].λa′:E[a].a, or λa:E[a].λa′:E[a].a′, or a variable, or something like fb, etc.

7.23 Encoding inductive types in λ2

E[α, β] :=

E[E[x]↦(α↦β↦x)↦x] E[α|β] :=

E[E[x]↦(α↦x)↦(β↦x)↦x] E[E[a], α] :=

E[E[x]↦(E[a]↦α↦x)↦x] E[⊤] :=

E[E[x]↦x↦x] E[⊥] :=

E[E[x]↦x] E[α^{List}] :=

E[E[x]↦x↦(α↦x↦x)↦x] ...

7.24 Parametricity for λ2

( \begin{matrix}α′ \\ α′′ \end{matrix})  a pair made of an α′ and an α′′.
( \begin{matrix}α′ ↦β′ \\ α′′↦β′′ \end{matrix})( \begin{matrix}α′ \\ α′′ \end{matrix})  two function applications; the result is ( \begin{matrix}(α′ ↦β′ )α′ \\ (α′′↦β′′)α′′ \end{matrix}).

( \begin{matrix}α′ \\ α′′ \end{matrix} ↦ω) a relation: a function that expects an α′ and an α′′ and returns a truth-value. An ( \begin{matrix}α′ \\ α′′ \end{matrix} ↦ω) is an (α′↦α′′↦ω) in disguise.

( \begin{matrix}α′ \\ α′′ \end{matrix} ↦ω)( \begin{matrix}α′ \\ α′′ \end{matrix})  (α′↦α′′↦ω)α′α′′ in disguise.

( \begin{matrix}α′ \\ α′′ \end{matrix} ↦ω) if α′ and α′′ come from a single α by priming and double-priming in the right way, then ( \begin{matrix}α′ \\ α′′ \end{matrix} ↦ω) denotes the parametricity relation associated to E[α]. If FV(E[α]) = \{E[a], E[b], E[c]\} then FV( \begin{matrix}α′ \\ α′′ \end{matrix} ↦ω) =

\{( \begin{matrix}E[a′ ] \\ E[a′′] \end{matrix} ), ( \begin{matrix}a′ \\ a′′ \end{matrix} ↦ω), ( \begin{matrix}E[b′ ] \\ E[b′′] \end{matrix} ), ( \begin{matrix}b′ \\ b′′ \end{matrix} ↦ω), ( \begin{matrix}E[c′ ] \\ E[c′′] \end{matrix} ), ( \begin{matrix}c′ \\ c′′ \end{matrix} ↦ω)\}.

The rules that build ( \begin{matrix}α′ \\ α′′ \end{matrix} ↦ω)’s inductively are:

( \begin{matrix}α′ ↦β \\ α′′↦β \end{matrix} ↦ω) := λ( \begin{matrix}α′ ↦β′ \\ α′′↦β′′ \end{matrix}).∀( \begin{matrix}α′ \\ α′ \end{matrix}).

( \begin{matrix}α′ \\ α′′ \end{matrix} ↦ω)( \begin{matrix}α′ \\ α′′ \end{matrix}) [figure]( \begin{matrix}β′ \\ β′′ \end{matrix} ↦ω)(( \begin{matrix}α′ ↦β′ \\ α′′↦β′′ \end{matrix})( \begin{matrix}α′ \\ α′′ \end{matrix})),

( \begin{matrix}E[a′ ]↦β \\ E[a′′]↦β \end{matrix} ↦ω) := λ( \begin{matrix}E[a′ ]↦β \\ E[a′′]↦β \end{matrix}).∀( \begin{matrix}E[a′ ] \\ E[a′′] \end{matrix} ).∀( \begin{matrix}a′ \\ a′′ \end{matrix} ↦ω).

( \begin{matrix}β′ \\ β′′ \end{matrix} ↦ω)(( \begin{matrix}E[a′ ]↦β \\ E[a′′]↦β \end{matrix})( \begin{matrix}E[a′ ] \\ E[a′′] \end{matrix} )).

7.25 Filter-quotients

𝕀 = E[i]  the index set
𝕀 = Cat[i^{D}]  the index set, seen as a discrete category
O[a] := (i^{D} ⇒ a_{i})  an object of Set^{𝕀}

O[⊤] := (i^{D} ⇒ ⊤) the terminal in Set^{𝕀}. Note that there’s an abuse of language here, as we also use O[⊤] (and E[⊤]) to denote the terminal in Set

F ⊂ P(𝕀)  a filter on 𝕀
U ⊂ P(𝕀)  an ultrafilter on 𝕀; this is a particular case of the above
F, F′, F_{1}, F_{2}, U, V ∈ F some F-big subsets of 𝕀
{O[⊤|_{U}] := \atop i^{D} ⇒ ⊤|_{i∈U}}  a subobject of the terminal in Set^{𝕀}, with F-big support

O[a|_{U}] := O[a, ⊤|_{U}] := i^{D} ⇒ (a_{i}, ⊤|_{i∈U}) restricting an object O[a] of Set^{𝕀} to a certain F-big support by taking its product with the subobject of the terminal with that support, O[⊤|_{U}]. A subobject of this type is called an F-subobject of the original object O[a].

{a|_{U} ↪ a, \atop a|_{U∩V} ↪ a|_{U}}  canonical inclusions between F-subobjects of O[a]

[figure: a|_{U∩V}; b|_{V}; b|_{V}; c; a|_{U∩V}; a|_{U}; b|_{V}; b; a|_{U}; b; a|_{U}; a] an F-partial function (i.e., morphism) from O[a] to O[b], an F-partial function from O[b] to O[c], and the way to obtain their composite

Cat[a_{F}] the category that has the same objects as Cat[a] = Set^{𝕀} but whose morphisms are the F-partial functions of Cat[a]

Cat[a_{/F}] the smallest quotient of Cat[a] — or of Cat[a_{F}] — that makes each canonical inclusion between F-subobjects become an iso; two F-partial functions \begin{matrix}a_{U} & ↦ & b \\ ↓ \\ a \end{matrix} and

\begin{matrix}a_{V} & ↦ & b \\ ↓ \\ a \end{matrix} will identified in Cat[a_{/F}] iff there is an F-

subobject O[a_{W}] of O[a_{U}] and O[a_{V}] such that the two natural ways of obtaining the restriction a|_{W} ↦b yield the same result

7.26 Filter-quotients (old)

𝕀 = O[i]  the index set
F ⊂ P(𝕀)  a filter on 𝕀
U ⊂ P(𝕀)  an ultrafilter on 𝕀; this is a particular case of the above
F ↪ Sub(O[i])  F can be seen as a full subcategory of Sub(O[i])
F, F′, F_{1}, F_{2} ∈ F  some F-big subsets of 𝕀

O[i|_{F}]:Objs_{F} ; O[i|_{F}] := ; E[i|_{i∈F}] = F  seeing an F-big set as an object of the category F

i|_{F′} ↪ i|_{F}  such an inclusion exists iff F′ ⊂ F

O[i|_{F_{1}∧F_{2}}] := F_{1} ∩ F_{2} the intersection of two F-big sets; this corresponds to the categorical product of O[i|_{F_{1}}] and O[i|_{F_{2}}].

F, (i|_{F} ↦a_{i})  a pre-hyperpoint

a ⇒ (i|_{F}^{op} ⇒ (i|_{F} ↪ a_{i})) the functor that takes each O[a] to its diagram of prehyperpoints

a ⇒ (i|_{F}^{op} ⇒ (i|_{F} ↪ a_{i}))^{Colim} the functor that takes each O[a] to its object of hyperpoints

F, (i|_{F} ↦a_{i})↦ (i, a↦ω) the operation that represents pre-hyperpoints as partial functions

F, (i|_{F} ↦a_{i})↦ ((i, a↦ω)↦ω) the operation that represents hyperpoints as equivalence classes of partial functions

a ⇒ ((i, a↦ω)↦ω) the operation a ⇒ (i|_{F}^{op} ⇒ (i|_{F} ↪ a_{i}))^{Colim} induces a partial equivalence relation on O[(i, a↦ww)↦ω] that covers only those ‘i, a↦ω’s that are the graphs of partial functions F, (i|_{F} ↦a_{i}) with F-big domains. Sometimes we don’t care if a graph has garbage outside an F-big set; see page .

i/F↦a_{i} a pre-hyperpoint or a hyperpoint; depending on the context this will be formalized using any of the representations above: as an F, (i|_{F} ↦a_{i}), as an i, a↦ω, or as an (i, a↦ω)↦ω.

(a; i|_{F}^{op}) →^{•} ((i|_{F} ↦a_{i})↦ (i/F↦a_{i})) the quotient that takes pre-hyperpoints with a given domain, O[i|_{F}], to hyperpoints

i/F ↦(a_{i}↦b_{i})  an internal morphism (in the NSA sense)

8 The attic

8.1 Interpreting a derivation in λC categorically

\begin{aligned}\begin{matrix}{∗ \atop A} ^{[s]^{2}} & {∗ \atop B} s \\ A × B \end{matrix} ; a, b ; ^{[s]^{1}} ; b & & \begin{matrix}{∗ \atop B} s & {∗ \atop C} s \\ B → C \end{matrix} ; b ↦ c ; s \\ & c \end{aligned} ; a, b ↦ c ; 1 ; E[a] ↦ a, b ↦ c ; 2  \begin{matrix}\begin{matrix}{∗ \atop A} ^{[s]^{2}} & {∗ \atop B} s \\ A × B \end{matrix} ; p ; ^{[s]^{1}} ; π_{2}p & \begin{matrix}{∗ \atop B} s & {∗ \atop C} s \\ B → C \end{matrix} ; f ; s \\ f(π_{2}p) \end{matrix} ; λp : A × B.f(π_{2}p) ; 1 ; λA : ∗.λp : A × B.f(π_{2}p) ; 2

\begin{matrix}{B:∗ ⊢ B:∗ \atop B:∗, C:∗ ⊢ B:∗} & {C:∗ ⊢ C:∗ \atop B:∗, C:∗ ⊢ C:∗} \\ B:∗, C:∗ ⊢ ⟨B, C⟩: ∗ ×∗ \end{matrix} ; B:∗, C:∗ ⊢ B → C:∗ ; B:∗, C:∗; f:(B → C) ⊢ f:(B → C) ; A:∗, B:∗, C:∗; f:(B → C) ⊢ f:(B → C) ; A:∗, B:∗, C:∗; p:(A × B), f:(B → C) ⊢ f:(B → C)

\begin{matrix}{A:∗ ⊢ A:∗ \atop A:∗, B:∗ ⊢ A:∗} & {B:∗ ⊢ B:∗ \atop A:∗, B:∗ ⊢ B:∗} \\ A:∗, B:∗ ⊢ ⟨A, B⟩: ∗ ×∗ \end{matrix} ; A:∗, B:∗ ⊢ A × B:∗ ; A:∗, B:∗; p:(A × B) ⊢ p:(A × B) ; A:∗, B:∗, C:∗; p:(A × B) ⊢ p:(A × B) ; A:∗, B:∗, C:∗; p:(A × B) ⊢ π_{2}p:B ; A:∗, B:∗, C:∗; p:(A × B), f:(B → C) ⊢ π_{2}p:B

{A:∗, B:∗, C:∗; p:(A × B), f:(B → C) ⊢ ⟨π_{2}p, f⟩:B × (B → C) \atop A:∗, B:∗, C:∗; p:(A × B), f:(B → C) ⊢ f(π_{2}p):C} ; A:∗, B:∗, C:∗; f:(B → C) ⊢ (λp:(A × B).f(π_{2}p)):A × B → C ; B:∗, C:∗; f:(B → C) ⊢ (λA: ∗ .λp:(A × B).f(π_{2}p)):(ΠA: ∗ .A × B → C)

2002h (typeset 2002dec30 19:22) Edrx http://angg.twu.net/

[figure: A:∗, B:∗; A:∗, B:∗; A:∗, B:∗; A:∗, B:∗, A × B : ∗; A:∗, B:∗; A:∗; A:∗, B:∗; ⟨A, B⟩: ∗ ×∗; A:∗, B:∗; B:∗; ⟨A, B⟩: ∗ ×∗; A:∗; ⟨A, B⟩: ∗ ×∗; B:∗; ⟨A, B⟩: ∗ ×∗; A × B:∗; A:∗, B:∗, A × B : ∗; A:∗, B:∗; A:∗, B:∗, A × B : ∗; A × B:∗]

[figure: (\begin{matrix}A:∗, B:∗; p:A × B \\ ↓ \\ A:∗, B:∗ \end{matrix}); (\begin{matrix}A:∗, B:∗, P:∗; p:P \\ ↓ \\ A:∗, B:∗, P:∗ \end{matrix} ); \begin{matrix}P:=A×B \\ □ \end{matrix}; (\begin{matrix}A:∗, B:∗; p:A × B \\ ↓ \\ A:∗, B:∗ \end{matrix}); A:∗, B:∗; (\begin{matrix}A:∗, B:∗, P:∗; p:P \\ ↓ \\ A:∗, B:∗, P:∗ \end{matrix} ); A:∗, B:∗, P:∗; A:∗, B:∗; A:∗, B:∗, P:∗; P:=A×B]

a:A [figure: a:=π_{1}p]p:A × B [figure: b:=π_{2}p] b:B

[figure: A:∗, B:∗, C:∗; p:A × B; A:∗, B:∗; p:A × B; A:∗, B:∗, C:∗; p:A × B; A:∗, B:∗, C:∗; π_{2}p:B; π_{2}; A:∗, B:∗; p:A × B; A:∗, B:∗; π_{2}p:B; π_{2}; A:∗, B:∗, C:∗; π_{2}p:B; A:∗, B:∗; π_{2}p:B; A:∗, B:∗, C:∗; A:∗, B:∗]

[figure: A:∗, B:∗, C:∗; f:B → C; B:∗, C:∗; f:B → C; □; B:∗, C:∗; f:B → C; B:∗, C:∗, F:∗; f:F; \begin{matrix}F:=B→C \\ □ \end{matrix}; A:∗, B:∗, C:∗; f:B → C; A:∗, B:∗, C:∗; B:∗, C:∗; f:B → C; B:∗, C:∗; B:∗, C:∗, F:∗; f:F; B:∗, C:∗, F:∗; A:∗, B:∗, C:∗; B:∗, C:∗; B:∗, C:∗; B:∗, C:∗, F:∗; F:=B→C]

2002h (typeset 2002dec30 19:22) Edrx http://angg.twu.net/

[figure: p:A × B, f:B → C; p:A × B; p:A × B, f:B → C; ⟨π_{2}p, f⟩:B × (B → C); p:A × B, f:B → C; f:B → C; p:A × B; π_{2}p:B; ⟨π_{2}p, f⟩:B × (B → C); π_{2}p:B; ⟨π_{2}p, f⟩:B × (B → C); f:B → C; ⟨π_{2}p, f⟩:B × (B → C); f(π_{2}p):C]

Idéias que surgiram na apresentação pro Luiz Carlos, por Nicolau e pro Hermann: definir o DNC básico, i.e., com poucas extensões (o suficiente para o lema de Yoneda) - ops, eu sei que o truque principal é que o dicionário faz todo o trabalho (mas isso nem é tão verdade assim) - e de que modo eu defino as regras ou diretrizes pra criação do dicionário? Será que eu crio uma semântica não-determinística - nós podemos ter vários caminhos para dar um significado para um termo, mas nós escolhemos uma árvore para seguir...

\begin{matrix}\begin{aligned}{[a′, b]^{1} \atop a′} & [a′ ↦ a′′]^{2} \\ & a′′ \end{aligned} & {[a′, b]^{1} \atop b} \\ a′′, b \end{matrix} ; a′, b ↦ a′′, b ; 1 ; a ⇒ a, b

Adding the logic

Proofs as hypotheses

Witnesses as hypotheses

Irrelevance of proofs

Example: prf[a = b], prf[b = c] ⊢ prf[a = c]

Fato: dependência entre os tipos das variáveis (dem: indução a partir das folhas da árvore).

convenções de notação: A(), B(a), etc; γ:Γ; a:A como seqüência. Fatos sobre contextos (principalmente sobre ordem das hipóteses): definição de ordem de dependência: c:C depende diretamente de b:B se

b ∈ F V (C); a relação de “depende” é o fecho transitivo dessa. Exemplo em arvorezinha.

troca de dois caras que aparecem seguidos e são independentes um sistema com regras aparentemente mais fortes para o weakening, o “s” e a

abstração (e mais uma de exchange!) deriva exatamente os mesmos judgements que o sistema original

como se livrar de hipóteses das quais ninguém depende: empurre-as pra direita, e depois veja que elas só podem ter aparecido por weakening.

definir contextos mínimos e como minimalizar contextos. mostrar como fazer uma dedução com contextos mínimos e depois fazer um

grande weakening.

o Hyland/Pitts define contextos em árvore. definir (formalmente) as regras do sistema com contextos mínimos. se a:A, b:B, c:C ⊢ t:T é derivável então ⊢ A:s, a:A ⊢ B:s, a:A, b:B ⊢ C:s,

a:A, b:B, c:C ⊢ ∗:□ são deriváveis Fatos sobre classificação: toda variável está dois níveis abaixo de um sort. A demonstração é em duas

partes, com um brinde sobre a conclusão.

toda variável declarada numa hipótese está dois níveis abaixo de um sort (i.e., tem um sort associado). Dem: olhar pras regras que introduzem novas hipóteses.

intoduzir o truque das anotações de sort. Dar um exemplo com todas as anotações, inclusive as do app.

toda variável declarada num λ ou Π está dois níveis abaixo de um sort. as sorts associadas não dependem da derivação. brinde: se o T da conclusão não é um sort (mesmo que ele seja equivalente

a um sort!), então ele está um nível abaixo de um sort.

Fatos sobre o conv: graças à normalização forte nós podemos falar *do* tipo de um cara, ao

invés de *um* tipo prum cara.

conv para lados esquerdos: se ... ⊢ t:T e t →_{β} t′, então ... ⊢ t′:T — mas note que t′ pode ter menos dependências do que t. Fazer uma referência à discussão que diz que a árvore de reduções não envolve termos externos, e que ela continua sendo finita se a gente destipa os termos.

definir uma regra grande de conv operando ao mesmo tempo sobre todos os typings de hipóteses e sobre o t e o T do lado direito.

como deixar os convs implícitos: listar todos os convs que uma derivação usa e pôr a lista numa das partes do dicionário.

dizer onde é que os exemplos de conv vão aparecer. Fatos sobre subsistemas do λC como é que eu posso rearrumar os contextos em λ→, λ2 e λω λ→ e λ2 não precisam de conv (?) e λω só precisa de um conv restrito termos nesses sistemas têm formas simplinhas e eu posso criar uma lin-

guagem alternativa (“DNC notation”?) pra descrever tipos Transformando o λC na dedução natural que a gente quer: condição técnica: todas as declarações de uma mesma variável têm que ter

tipos beta-equivalentes.

reconstruindo o contexto a partir de uma dedução sem contextos (no sistema com contextos mínimos, todos os weakening implícitos, e módulo exchanges)

dando um sumiço nos typings, pondo-os num dicionário, e reconstruindo-os (módulo β-equivalência!) a partir de uma dedução sem eles e do dicionário.

introduzindo nomes novos, cada um com várias definições beta-equivalentes comparação disso com o caso dos a ↦ b ↦ d e a ↦ c ↦ d num diagrama Fatos sobre Σ-types regras normalização forte pares não tem tipos bem-definidos, e quando a gente usa o dicionário ele vai

ter que ter os tipos que a gente escolheu pra esses caras como tipar o <, >, o Σ, o π_{1} e o π_{2} estendendo a notação DNC com as vírgulas

8.2 Facts about λC (oct 2002)

Fact 1 - condition on the free variables.

In a (valid) judgement

x_{1} : A_{1}, x_{2} : A_{2}, x_{3} : A_{3}, …, x_{n} : A_{n} ⊢ t : T

we have that F V (A_{1}) = emptyset, F V (A_{2}) ⊆ {x_{1}}, F V (A_{3}) ⊆ {x_{1}, x_{2}}, … F V (A_{n}) ⊆ {x_{1}, x_{2}, …, x_{n−1}}, F V (t) ⊆ {x_{1}, x_{2}, …, x_{n}}, F V (T) ⊆ {x_{1}, x_{2}, …, x_{n}}. Another way to express this is to write judgements this way (let’s use an

example with n = 3):

a : A(), b : B(a), c : C(a, b) ⊢ t(a, b, c) : T (a, b, c)

where A(), B(a), C(a, b), t(a, b, c), T (a, b, c) stand for terms that can only have as free variables the letters listed inside parentheses.

Fact 2 - we don’t need a rule for exchange. (We’ll use an example with n=4.) If the following is a judgement,

a:A(), b:B(a), c:C(a), d:D(a, b, c) ⊢ t(a, b, c, d):T (a, b, c, d),

that is, if b is not a free variable of C(a), then the following is also a judgement:

a:A(), c:C(a), b:B(a), d:D(a, b, c) ⊢ t(a, b, c, d):T (a, b, c, d);

That is: we have an algorithm that will transform a derivation of the first judgement into a derivation of the second; and that can be done for any case (n not necessarily 4, etc) where we have a pair of “independent” variables in a context.

[Another notation:]

γ : Γ, b:B(γ), c:C(γ), δ:Δ(γ, b, c) ⊢ t(γ, b, c, δ):T (γ, b, c, δ)

Fact 3a - each variable is two levels below a sort. (Example with n = 3.) For any judgement J like:

a:A(), b:B(a), c:C(a, b) ⊢ t(a, b, c):T (a, b, c)

we can get (algorithmically, by manipulating its derivation) sorts S_{A}, S_{B} and S_{C} and derivations for

⊢ A():S_{A}, a:A() ⊢ B(a):S_{B}, a:A(), b:B(a) ⊢ C(a, b) : S_{C}. Sometimes we will commit a slight abuse of language and write the sorts

inside the judgement J:

a:A():S_{A}, b:B(a):S_{B}, c:C(a, b):S_{C}| − t(a, b, c):T (a, b, c)

[Or: in some texts we find the sorts written inside the judgement, but we are going to have another way, the “sort annotations” — see the fact 4, below.]

Fact 3b - the sorts S_{A}, S_{B} and S_{C} above can obtained from the judgement J alone; we don’t need to look at a specific derivation of J to obtain them.

This is an easy corollary of the following stronger fact:

Fact 4 - stratification. There is a way to add a “sort annotation” to each subterm that appears in

a judgment J, such that each subterm will be in one of the six classes, □, □ − 1, □ − 2, ∗, ∗ − 1, ∗ − 2, and every time that we have x:X the class of x will be “one level below” the class of X; all of these classes are disjoint except for that

The technique for doing that is to add a “sort annotation” to every variable and every Π, λ or application that appears in J.

A^{S−1}:S a^{S−2}:A^{S−1} (Π_{RS}a^{R−2}:A^{R−1}.B^{S−1})^{S−1} (λ_{RS}a^{R−2}:A^{R−1}.b^{S−2})^{S−2} (app_{RS}f^{S−2}a^{R−2})^{S−2}

8.3 Expressing preservation of limits in NDC

Motivation for the term for limits:

((b, c)|_{d} → b; (b, c)|_{d} → d) is a pullback for (b → d; c → d) iff

a^{op} →^{•} ((a → (b, c)|_{d}) → (a → b; a → c)|_{wd(a→d)}) is in fact a

a^{op} →^{•} ((a → (b, c)|_{d}) ↔ (a → b; a → c)|_{wd(a→d)}).

As an adjunction:

\begin{aligned}\begin{aligned}& & a \\ & & ↓ \\ a & → & a \end{aligned} & ⇐ & a \\ ↓ & ↔ & ↓ \\ \begin{aligned}& & c \\ & & ↓ \\ b & → & d \end{aligned} & ⇒ & (b, c)|_{d} \end{aligned}

(a^{op}; \begin{matrix}& & c \\ & & ↓ \\ b & → & d \end{matrix}) →^{•} (( \begin{matrix}& & a \\ & & ↓ \\ a & → & a \end{matrix} → \begin{matrix}& & c \\ & & ↓ \\ b & → & d \end{matrix}) ↔ (a → (b, c)|_{d}))

(a^{op}; i ⇒ b_{i}) →^{•} (((i ⇒ a) → (i ⇒ b_{i})) ↔ (a → (i ⇒ b_{i})^{Lim})

(a^{op}; i ⇒ b_{i}) →^{•} ((i →^{•} (a → b_{i})) ↔ (a → lim_{i} b_{i}))

O[lim_{i} b_{i}] := O[(i ⇒ b_{i})^{Lim}]

The term for a limit:

(a^{op}; i ⇒ b_{i}) →^{•} ((i →^{•} (a → b_{i})) ↔ (a → lim_{i} b_{i}))

The fact that there is still a bijection of hom-sets after applying F:

(a^{op}; i ⇒ b_{i}) →^{•} ((i →^{•} (a^{F} → b_{i}^{F})) ↔ (a^{F} → (lim_{i} b_{i})^{F}))

A stronger fact (“F preserves limits”):

((a^{F})^{op}; i ⇒ b_{i}) →^{•} ((i →^{•} (a^{F} → b_{i}^{F})) ↔ (a^{F} → (lim_{i} b_{i})^{F}))

If the target category of F has limits then this is equivalent to (i ⇒ b_{i}) →^{•} ((lim_{i} b_{i})^{F} ↔ (lim_{i} b_{i}^{F}))... demonstration?

Theorem: if F is the R of an adjunction (that is, if it has a left adjoint L) then it automatically preserves limits.

An example, before the proof: consider the adjunction (a ⇒ a, b) ⊣ (c ⇒ (b → c)) between two functors from Set to Set; a ⇒ a, b does not preserve products, as in general a′, a′′, b ↮ a′, b, a′′, b, and c ⇒ (b → c) does not preserve coproducts, as generally (b → (c′ ⨿ c′′)) ↮ ((b → c′) ⨿ (b → c′′)); but we always have (a′ ⨿ a′′), b ↔ (a′, b) ⨿ (a′′, b) and (b → c′, c′′) ↔ ((b → c′), (b → c′′)).

In this case the proof will go like this (I need to explain!):

\begin{aligned}i ⇒ x & ⇒ & i ⇒ (x, b) & ⇐ & x, b & ⇐ & x^{R} \\ ↓ & ↔ & ↓ & ↔ & ↓ & ↔ & ↓ \\ i ⇒ (b → c_{i}) & ⇐ & i ⇒ c_{i} & ⇒ & c_{1}, c_{2} & ⇒ & b → (c_{1}, c_{2}) \end{aligned}

And the general proof is:

\begin{aligned}i ⇒ a^{R} & ⇒ & i ⇒ a^{RL} & ⇐ & a^{RL} & ⇐ & a^{R} \\ ↓ & ↔ & ↓ & ↔ & ↓ & ↔ & ↓ \\ i ⇒ b_{i}^{R} & ⇐ & i ⇒ b_{i} & ⇒ & lim_{i} b_{i} & ⇒ & (lim_{i} b_{i})^{R} \end{aligned}

Writing that proof as a big term (using composition of arrows in the natural transformation):

((a^{R})^{op}; i ⇒ b_{i}) →^{•} ( (i →^{•} (a^{R} → b_{i}^{R})) ↔

(i →^{•} (a^{RL} → b_{i})) ↔

(a^{RL} → lim_{i} b_{i}) ↔ (a^{R} → (lim_{i} b_{i})^{R})

A particular case, plus something: in a cartesian (bi)closed category,

(a^{op}; b; c) →^{•} ((a → b, c) ↔ (a → b), (a → c))

(a^{op}; b^{op}; c) →^{•} ((a ⨿ b → c) ↔ (a → c), (b → c))

(a^{op}; b^{op}; c) →^{•} ((a, b → c) ↔ (a → (b → c)))

a^{op} →^{•} ((a → ⊤) ↔ ⊤)

a →^{•} ((⊥ → a) ↔ ⊤)

and “F preserves the cartesian-closed structure” means:

((a^{F})^{op}; b; c) →^{•} ((a^{F} → (b, c)^{F}) ↔ (a^{F} → b^{F}), (a^{F} → c^{F}))

(a^{op}; b^{op}; c^{F}) →^{•} (((a ⨿ b)^{F} → c^{F}) ↔ (a^{F} → c^{F}), (b^{F} → c^{F}))

((a^{F})^{op}; b^{op}; c) →^{•} ((a^{F} , b^{F} → c^{F}) ↔ (a^{F} → (b → c)^{F})) (?)

(a^{F})^{op} →^{•} ((a^{F} → ⊤^{F}) ↔ ⊤)

a^{F} →^{•} ((⊥^{F} → a^{F}) ↔ ⊤)

A functor R that has a left adjoint preserves limits. Here’s how to express that: We state that the constant functor b ⇒ (i ⇒ b) has a left adjoint, (i ⇒

a_{i}) ⇒ (i ⇒ a_{i})^{Lim}, with:

((i ⇒ a_{i})^{op}; b) →^{•} ((i ⇒ a_{i})^{Lim} → b) ↔

\begin{aligned}c ⇒ a & ⇐ & a & c ⇒ a^{F} & ⇐ & a^{F} \\ ↓ & ↔ & ↓ & ↓ & ↔ & ↓ \\ c ⇒ b_{c} & ⇒ & lim_{c} b_{c} & c ⇒ b_{c}^{F} & (⇒) & (lim_{c} b_{c})^{F} \end{aligned}

8.4 Skeletons of proofs

8.5 Infinitesimals as sequences

Semi-standard analysis: introduction

Both in Calculus and in Categories the most natural way to present several important ideas is via types — it is often the case that there is essentially a single natural way to build an object of a certain type. If we change our mathematical language in such a way that it will let us denote objects by their types (and not only by their constructions), then several concepts become much clearer, and several demonstrations can become much shorter.

We will now discuss the “Calculus” side of this idea. We will start by showing a way to introduce infinitesimals into the language and get rid of them afterwards^{2}; later on we will get into a muddier terrain and turn to a search for a language that has a natural deduction system and that is able to represent some constructions with derivatives and infinitesimals, via a sort of Curry-Howard isomorphism.

Cheap Non-Standard Analysis

The naïve idea that infinitesimals can be regarded as sequences of reals tending to zero needs just a few fixes to be made to work. Take the category Set as being our “standard universe”, and choose an index set 𝕀. We denote by Set^{𝕀} the “universe of 𝕀-sequences”; its objects are 𝕀-sequences of objects of Set, its morphisms from (𝕚 ↦ A_{𝕚}) to (𝕚 ↦ B_{𝕚}) are 𝕀-sequences of morphisms 𝕚 ↦ (A_{𝕚} → B_{𝕚}), and so on. Let’s start by supposing that 𝕀 = ℕ, just to make things simpler; the 𝕀-sequences will then be sequences in the usual sense of the term, and we can use the more familiar concepts and terminology.

8.6 Filters and ultrafilters

Set^{𝕀} is still too different from a sort of “Set with infinitesimals added”, so we take another step: we identify sequences that have the same “tails”, or, equivalently, sequences that coincide at all but a finite number of indices — that is, on a “cofinite” set of indices). Let’s do that in a more general way: we have a certain set F ⊂ P(𝕀) of “big” subsets of 𝕀, and two 𝕀-sequences (𝕚 ↦ a_{𝕚}) and (𝕚 ↦ b_{𝕚}) will be declared F-equivalent iff they coincide at an F-big set, that is, if { 𝕚 | a_{𝕚} = b_{𝕚}} ∈ F. It turns out that the conditions that F must obey to make F-equivalence an equivalence relation are exactly those that make F a filter: to have a ∼_{F} a we must have that 𝕀 ∈ F, i.e., that “the whole is big”; to have transitivity we must have that “anything bigger than the intersection of two big sets is still big”. Note that when F is the trivial filter, F = P(𝕀), all sequences are equivalent, and so we’ll generally want to have F non-trivial; two conditions equivalent to F being non-trivial are: 1) ∅ ∉ F, and 2) no complement of an F-big set is an F-big set. We’ll call a subset of 𝕀 F-small (or just small) when it is the complement of an (F-)big set; subsets of 𝕀 that are neither (F-)big nor (F-)small will be called (F-)medium.

2I have never found in the literature any reference to filter-infinitesimals or to anything similar to the translation using natural infinitesimals, but I won’t dare saying it’s something new.

2002h (typeset 2002dec30 19:22) Edrx http://angg.twu.net/

In non-trivial filters the small sets play a role dual to that of the big sets: the void set is small, the whole set is not small, and anything smaller than the union of two small sets is still small; in non-trivial filters big and small sets come in pairs, and we get from a small set the to associated big set (and vice-versa) by taking complements. Non-trivial filters that divide all sets of P(𝕀) into pairs of big and small sets without leaving any medium sets are called ultrafilters; we will denote ultrafilters by names with U, like U, U_{1}, U_{2}, …, and filters by names with calligraphic capitals, mainly with F; the letter U is reserved for ultrafilters, and so “every ‘U’ is an ‘F’, but few ‘F’s are ‘U’s”... Also concerning names, we will denote the filter of the cofinite sets of ℕ by N, and if a is a point of a topological space (X, O_{X}) (this O_{X} is a topology, not a filter!) then the set of neighbourhoods of a in (X, O_{X}), written V_{a}, is called the filter of neighbourhoods of a, and we write V_{a}^{∗} for the filter of punctured neighbourhoods of a, the set of subsets of X\{a} that become neighbourhoods of a when we add {a} to them; V_{a}^{∗} is a trivial filter if and only if {a} is open in X.

8.7 A glimpse of non-standard analysis

We will denote the quotient of Set^{𝕀} by the equivalence relation induced by F by Set^{F}, instead of using the longer notation Set^{𝕀}/F. Non-standard analysis is concerned with the ‘Set^{U}’s, that are called the non-standard universes; every Set^{U} obeys a logic very close to that of the standard universe: it has exactly two truth values (that is, the morphisms 𝕚 → (1 → ω) of Set^{𝕀} fall in exactly two classes after the quotient /F), all first-order sentences with all quantifiers bounded and all whose constants are standard evaluate to the same truth value in Set as in Set^{U} (by the “transfer theorem”), and unless U is principal^{3} all infinite sets of Set gain “infinite” elements with the passage to Set^{U} (by the “concurrence theorem”).

8.8 Semi-standard analysis: NSA using filters

In contrast the ‘Set^{F}’s are much stranger. They generally have many other truth values “between” ⊤ (= (⊤, ⊤, ⊤, …)) and Ⅎ (= (Ⅎ, Ⅎ, Ⅎ, …)) — for example in Set^{N} it is easy to see that (⊤, Ⅎ, ⊤, Ⅎ, ⊤, Ⅎ, …) coincides with either ⊤ or Ⅎ only in medium sets of indices — and we will have to obtain other definitions for the quantifiers ∀ and ∃ to suit this, as the usual (“external”) definitions give operations that can return only ⊤ or Ⅎ, and that won’t be very useful; the new (“internal”) definitions will be able to return any truth value and will end up being better behaved... and it is not at all easy to obtain an analogue of the transfer theorem for the ‘Set^{F}’s.

3that is, if there is an element i_{0} ∈ 𝕀 such that the U-big subsets of 𝕀 are exactly those that contain i_{0}

2002h (typeset 2002dec30 19:22) Edrx http://angg.twu.net/

The surprising thing is that we can do quite a lot in a Set^{F} without knowing much about its logic, just by doing calculations with infinitesimals “in the way we think they should work” and later translating these calculations back to the standard universe and checking that they were indeed correct. We need just a few definitions more and a simple theorem to get to our first example.

A pre-hiper-a is a function from 𝕀 to A, i.e., an 𝕚 → a (an “𝕚-sequence” of ‘a’s). For example a pre-hiper-truth-value is an 𝕚-sequence whose values can be only ⊤ and Ⅎ.

A hiper-a is a pre-hiper-a modulo the equivalence relation /F.

A pre-hiper-real 𝕚 → 𝕣 is said to infinitesimal, or infinitely close to 0 in ℝ, if for every open set U ⊂ ℝ containing 0 we have that 𝕚 → 𝕣 is inside U for a big set of indices, i.e., if the sequence of truth-values given by 𝕚 ↦ (𝕣_{𝕚} ∈ U) is F-equivalent to ⊤. For example, (1, \frac{1}{2}, \frac{1}{3}, \frac{1}{4}, …) is an infinitesimal in Set^{N}.

A pre-hiperpoint is called standard if it is a constant sequence.

The constant mapping takes points of Set into pre-hiperpoints of Set^{𝕀}, and the quotient mapping from Set^{𝕀} to Set^{F} takes pre-hiperpoints into hiperpoints. Using the quotient mapping we can let Set^{F} inherit several definitions from Set^{𝕀} in the obvious way: for example a hiperpoint is called standard (resp. infinitesimal) if it is the image by the quotient mapping of a standard (resp. infinitesimal) pre-hiperpoint.

Parenthesis: a digression on foundations

Note that if we take an 𝕚-sequence of ‘a’s and we change its values in a small set of indices to values that are not ‘a’s then we would still be in the same equivalence class; at some moment we will have to lay down solid foundations and decide if a hiper-a will be only a class of pre-hiper-‘a’s or if it will contain also other stranger 𝕚-sequences; this decision will only be important much later, when we will have to deal with pre-hiper-‘a’s in which each a_{𝕚} will be an element of an A_{𝕚}, where the 𝕚-sequence of ‘A_{𝕚}’s won’t be required to be constant.

Pre-hiperpoints and hiperpoints are the notions in Set^{𝕀} and in Set^{F} (respectively) corresponding to the notion of point in Set; we chose the name Set for the standard universe to reinforce the idea that it is a category and that it makes no sense to talk simply about “points” in Set; each “point” of set is in fact a point of a set in Set (i.e., of an object of the category Set), and the only reason why we avoid mentioning the ambient set of every point explicitly is to avoid clutter.

The transfer theorem between Set and Set^{U} only works for sentences that use only bounded quantifiers (i.e., where all quantifiers appear like “∀x∈X …”, and no one like just “∀x …”). Bounded quantifiers are easy to understand categorically: for example take a function (a “proposition”) P : X × Y → Ω (i.e., x, y →^{P} τ); ∀_{x}P is a function from Y to Ω, and this ∀_{x} can be seen as a function (x, y → τ) →^{∀_{x}} (y → τ), and the same for ∃_{x}; it is by following this point of view that we get the “internal” ‘∀’s and ‘∃’s in Set^{𝕀} and Set^{F}.

The reader with some experience in topos theory will recognize that Set, Set^{𝕀} and Set^{F} are topoi — in fact boolean topoi— and that the right way to interpret the connectives and quantifiers internally in them is by borrowing CONTENTS 68

the definitions from the Mitchell-Bénabou language; but none of our simple examples will need any topos theory. Topos theory would certainly be useful to get a version that works between Set and Set^{F} of the famous transfer theorem of NSA; this may even have already been done, but I still don’t know enough to be able to tell.

8.9 Encoding inductive types

### ### Lists ### # # Constructors: # nil A : List A # cons A a d : List A # where # a : A # d : List A # # Reductions: # (nil A) B fnil fcons = fnil # (cons A a d) B fnil fcons = fcons a (d B fnil fcons) # where # fnil : B # fcons : A→(B→B) # are the “components” of a “destructor”: # f : (List A)→B

nil = λA: ∗ .λB: ∗ .λfnil:B.λfcons:(A → (B → B)).fnil cons = λA: ∗ .λa:A.λd:(ListA).

λB: ∗ .λfnil:B.λfcons:(A → (B → B)).(d B fnil fcons)

List = λA: ∗ .ΠB: ∗ .Πfnil:B.Πfcons:(A → (B → B)).B ### ### Lists ### # # Constructors: # nil A : List A # cons A a d : List A # where # a : A # d : List A # # Reductions: # (nil A) B fnil fcons = fnil # (cons A a d) B fnil fcons = fcons a (d B fnil fcons) # where # fnil : B # fcons : A→(B→B) # are the ”components” of a ”destructor”: # f : (List A)→B

nil = λA : ∗.λB : ∗.λfnil : B.λfcons : (A− > (B− > B)).fnil cons = λA : ∗.λa : A.λd : (ListA). λB : ∗.λfnil : B.λfcons : (A− > (B− > B)).(dBfnilfcons)

List = λA : ∗.ΠB : ∗.Πfnil : B.Πfcons : (A− > (B− > B)).B

### ### Pairs (products) ### # # Constructors: # pair A B a b : Pair A B # where # a : A # b : B # # Reductions: # (pair A B a b) C fcur = fcur a b # where # fcur : A→(B→C) # is the only “component” of the “destructor” # f : (Pair A B)→C

pair = λA : ∗.λB : ∗.λX : ∗.λa : A.λb : B.λfcur : (A− > (B− > X)).(fcurab) Pair = λA : ∗.λB : ∗.ΠX : ∗.Πfcur : (A− > (B− > X)).X

# Extras: # pi1 A B p = p A (λa : A.λb : B.a) # pi2 A B p = p B (λa : A.λb : B.b) # where

CONTENTS 69

# p : Pair A B

pi1 = λA : ∗.λB : ∗.λp : (P airAB).(pA(λa : A.λb : B.a)) pi2 = λA : ∗.λB : ∗.λp : (P airAB).(pB(λa : A.λb : B.b))

### ### Copairs (disjoint unions) ### # # Constructors: # in1 A B a : CoPair A B # in2 A B b : CoPair A B # where: # a : A # b : B # # Reductions: # (in1 A B a) C f g = f a # (in2 A B b) C f g = g b # where # f : A→C # g : B→C # are the ”components” of a ”destructor”: # h : (CoPair A B)→C

in1 = λA : ∗.λB : ∗.λa : A.λX : ∗.λf : (A → X).λg : (B → X).(fa) in2 = λA : ∗.λB : ∗.λb : B.λX : ∗.λf : (A → X).λg : (B → X).(gb)

CoPair = λA : ∗.λB : ∗.ΠX : ∗.Πf : (A → X).Πg : (B → X).X

# Extras: # coprod A B C f g : (CoPair A B)→C # with reduction # (coprod A B C f g) s = s C f g # i.e., # (coprod A B C f g) (in1 A B a) = f a # (coprod A B C f g) (in2 A B b) = g b # where # s : CoPair A B

coprod = λA : ∗.λB : ∗.λC : ∗.λf : (A → C).λg : (B → C).λs : (CoP airAB).(sCfg)

8.10 Categories in DNC

8.11 categories

Cat[a] = C means O[a] ∈ Objs_{C} O[a], O[b], O[c] ∈ Objs_{C} E[a ↦ b] := Hom_{C}(O[a], O[b]) so that (a ↦ b): Hom_{C}(O[a], O[b]) a ↦ b ↦ c := ∘_{C}(b ↦ c)(a ↦ b) or whatever a ↦ a := id_{C}O[a] diagrams, double defs: a ↦ d := a ↦ b ↦ d = a ↦ c ↦ d commutative things, well-defined things no comparison between objects; isomorphisms

8.12 products

O[b, c], (b, c ↦ b), (b, c ↦ c) is a product when (diagram)

π_{1} and π_{2} for a, a ↦ a, or a′, a′′ ↦ a′, etc a DNC operation for the factorization a, b ↦ c, d and (a ↦ c), (b ↦ d) two products for the same guys are isomorphic

discussion about ∀∃ and functions; we will stress the function explicitly

Tipos de “=” e “:=”:

E[a ↦ b] := Hom_{C}(O[a], O[b]) é uma definição

Hom_{C}(O[a], O[b]) = Hom_{C} O[a]O[b]

diz como interpretar algo do mundo real em DNC

(f ∘ g) ∘ h = f ∘ (g ∘ h) é uma igualdade

Prfs[f = g] blablabla

8.13 How to interpret set theory in any topos

8.14 Falsifying some classical truths

8.15 Set^{F} as a topos

Between Set and Set^{𝕀} we have a geometric morphism.

From Set^{𝕀} to Set^{F} we have a logical functor that doesn’t (seem to) have adjoints.

But there’s a way to transfer proofs from the (right) Set^{F} to Set!

A proof is a construction of a value a or of a witness ⊤[P].

Obs: an infinitesimal is a hyperpoint plus a proof of its infinitesimality — and this proof is a hybrid: for each standard neighbourhood blablablah is Ftrue.

8.16 Parametricity

Inductive definition for F-normal names: for any letter a, and for any F-normal names b and c, a, b ↦ c, E[a] ↦ b are F-normal names.

Theorem: in System F the types are formed using only Π and * — no λ, no application. More formally: T is a System F type iff Γ ⊢ T:∗ is derivable in F; if A is an uppercase letters (A:∗, B:∗) and T and U are types, then A, T → U and ΠA: ∗ .T are types. Moreover, the minimal context Γ in Γ ⊢ T:∗ is A:∗, B:∗, …, C:∗, where A, B, … C are the free variables of T.

Theorem: there is a natural bijection between F-normal names and types of F. Example: ΠX: ∗ .((A → X) → (B → X) → X) corresponds to E[E[x] ↦ ((a ↦ x) ↦ (b ↦ x) ↦ x)].

[Note: in this section we use the Haskellian convention for arrows: A → B → C means A → (B → C), a ↦ b ↦ c means a ↦ (b ↦ c).]

Big theorem (parametricity): for any F-type E[t] there is a relation R_{E[t]}, built inductively from the structure of t, such that for any term t:E[t] we have that R_{E[t]}tt holds (when the “free relation variables” of R_{E[t]} are set to certain values — this is be described later).

Big theorem (free theorems): if for each of the “free relation variables” of an R_{E[t]}, say a′ ↦ a′′ ↦ ω, we set it to the relation corresponding to the graph of a function a′ ↦ a′′, we get something that does not depend on the symbol ω anymore, and that may be interpreted in F; and that “something” will correspond to a statement about β-equivalence of terms.

Describe the duplication, using the long notation and the short one.

8.17 Parametricity for λC

8.18 Sheaves

8.18.1 Putting a topology on the sheaf of sections

Trick: every time that x and U appear in the same term, it will be implicit that x ∈ U.

We need to define a topology on E[x, f_{x}]; that is, for each subset E[(x, f_{x})|_{A}] of E[x, f_{x}], we need to decide if it will be “open” or “not open”. Here’s the rule: build this diagram:

[figure: (x, U, f_{U})|_{A}; x, U, f_{U}; x, U, f_{U}; U, f_{U}; (x, U, f_{U})|_{A}; (x, f_{x})|_{A}; x, U, f_{U}; x, U, f_{x}; U, f_{U}; U; x, U, f_{x}; x, U; x, U; U; x, U, f_{x}; x, f_{x}; x, U; x; (x, f_{x})|_{A}; x, f_{x}; x, f_{x}; x]

Now for each value of (U, f_{U}), look at its inverse image in E[(x, U, f_{U})|_{A}], and at the image of that set in E[x] — it will be a subset of U, consisting of all the ‘x’s for which the germ f_{x} is “A-good”. If for every (U, f_{U}) this set of “A-good ‘x’s” is open, then the E[(x, f_{x})|_{A}] is open.

8.19 Sheaves (Johnstone, pp.10–12)

esp/(X, O_{X}) [figure: L; Γ] Set^{O_{X}^{op}} : [figure: (X′^{op} ⇒ a_{X′}); ^{(\begin{matrix}x, a_{x} \\ ↓ \\ x \end{matrix})}; L; _{(\begin{matrix}x, b_{x} \\ ↓ \\ x \end{matrix})}; (X′^{op} ⇒ (x′ ↦ x′, b_{x′})); Γ; (X′^{op} ⇒ a_{X′}); (X′^{op} ⇒ (x′ ↦ x′, b_{x′})); ^{(\begin{matrix}x, a_{x} \\ ↓ \\ x \end{matrix})}; _{(\begin{matrix}x, b_{x} \\ ↓ \\ x \end{matrix})}]

Shv(X, O_{X}) [figure: ΓL; inc] Set^{O_{X}^{op}} : [figure: (X′^{op} ⇒ p_{X′}); (X′^{op} ⇒_{sh} (x′ ↦ x′, p_{x′})); ΓL; (X′^{op} ⇒_{sh} (x′ ↦ x′, p_{x′})); (X′^{op} ⇒_{sh} s_{X′}); (X′^{op} ⇒ p_{X′}); (X′^{op} ⇒ s_{X′}); (X′^{op} ⇒_{sh} s_{X′}); (X′^{op} ⇒ s_{X′}); inclusion] Shv(X, O_{X}) [figure: f^{∗}; f_{∗}] Shv(Y, O_{Y}) : [figure: (Y′ ⇒_{sh} b_{Y′}); (X′^{op} ⇒_{sh} (x′ ↦ x′, b_{f(x′)})); f^{∗}; (X′^{op} ⇒_{sh} (x′ ↦ x′, b_{f(x′)})); (X′^{op} ⇒_{sh} a_{X′}); (Y′ ⇒_{sh} b_{Y′}); (Y′ ⇒_{sh} a_{f^{−1}(Y′)}); (X′^{op} ⇒_{sh} a_{X′}); (Y′ ⇒_{sh} a_{f^{−1}(Y′)}); f_{∗}; (X, O_{X}); (Y, O_{Y}); f]

8.20 Geometric morphisms (on topological spaces)

Prop: if f : X → Y is an open mapping between two topological spaces, then it induces an adjunction (X′ ⇒ X′^{A}) ⇒ (Y′ ⇒ Y′^{f^{−1}A}) ⊣ (Y′ ⇒ Y′^{B}) ⇒ (X′ ⇒ X′^{fB}).

[figure: (X′ ⇒ X′^{A}); (Y′ ⇒ Y′^{f^{−1}A}); (Y′ ⇒ Y′^{B}); (X′ ⇒ X′^{fB}); (Y′ ⇒ Y′^{f^{−1}A}); (Y′ ⇒ Y′^{B}); (X′ ⇒ X′^{A}); (X′ ⇒ X′^{fB})]

Demonstration (T-part only): we will build the adjunction from the unit and the counit (as natural transformations), and the two functors; the two sides of the bijection will be obtained by the trick below:

[figure: a; a^{L}; b; b^{R}; a^{L}; b; \begin{matrix}a^{L}↦b \\ a^{L}↦b^{RL}↦b \end{matrix}; a; b^{R}; \begin{matrix}a↦a^{LR}↦b^{R} \\ a↦b^{R} \end{matrix}]

X and Y are topological spaces, and we have X′ ⊂ f^{−1}(f(X′)) and f(f^{−1}(Y′)) ⊂ Y′ for any subsets X′ ⊂ X and Y′ ⊂ Y; also, f is open, so we have natural transformations X′ →^{•} (X′ ↪ X′^{ff^{−1}}) and Y′ →^{•} (Y′^{f^{−1}f} ↪ Y′)... note that now X′ are Y′ are open sets of X and Y, seen as objects of O_{X} and O_{Y}.

[figure: X′; _{X′_{f}}; _{X′_{f}}; _{X′_{ff^{−1}}}; Y′; _{Y′_{f^{−1}}}; _{Y′_{f^{−1}}}; Y′^{f^{−1}f}; X′; _{X′_{ff^{−1}}}; Y′^{f^{−1}f}; Y′]

\begin{matrix}X′ →^{•} (X′ ↪ X′^{ff^{−1}}) & X′ ⇒ X′^{A} \\ X′ →^{•} (X′^{A} ↦ X′^{ff^{−1}A}) \end{matrix}  \begin{matrix}Y′ →^{•} (Y′^{f^{−1}f} ↪ Y′) & Y′ ⇒ Y′^{B} \\ Y′ →^{•} (Y′^{f^{−1}fB} ↦ Y′^{B}) \end{matrix}

and here is something to convince us that the functors in the adjunction have the right variances:

\begin{aligned}a ⇒ a^{F} & [b →^{•} (b^{G′} ↦ b^{G′′})]^{1} & c ⇒ c^{H} \\ & a →^{•} (a^{F G′H} ↦ a^{F G′′H}) \end{aligned} ; (b ⇒ b^{G}) ⇒ (a ⇒ a^{F GH}) ; 1

8.21 Grothendieck topologies

Let C be a (small) category. Def: C^{∼} := Set^{C^{op}}.

The Yoneda functor Y : C → C^{∼} (i.e., c ⇒ (d^{op} ⇒ (d ↦ c))) embeds C into C^{∼}.

A sieve S on C is a subfunctor of YC: (d^{op} ⇒ (d ↦ c)|_{S}) ↪ (d^{op} ⇒ (d ↦ c)).

For each object C of C we can speak of the category of sieves on C; it is a preorder, ordered by inclusion. It has products (I need to check that...) and a terminal, the “maximal sieve” d^{op} ⇒ (d ↦ c)|_{⊤}.

A morphism d ↦ c in C induces a “pullback functor” (d ↦ c)^{∗} : Sub(e^{op} ⇒ (e ↦ c)) → Sub(e^{op} ⇒ (e ↦ d)):

[figure: (e^{op} ⇒ (e ↦ c)|_{R}); \begin{matrix}(e^{op} ⇒ (e ↦ d)|_{(d↦c)^{∗}(R)}) := \\ (e^{op} ⇒ (e ↦ d)|_{(e↦d↦c)∈R}) \end{matrix}; (d↦c)^{∗}; d; c]

A Grothendieck topology J on C is an operation that assigns to each object C of C a full subcategory J(C) of Sub(YC) (the category of the “J-covering sieves on C), respecting three conditions:

(i) for each C the maximal sieve on C is in J(C);

(ii) for each d ↦ c the functor (d ↦ c)^{∗} takes each object of J(C) to an object in J(D);

(iii) ∀C.∀R:J(C).∀S:YC.

((∀D.∀(d ↦ c)|_{R}.(d ↦ c)^{∗}(S)∈J(D)) [figure]S∈J(C)). Due to (ii) a Grothendieck topology can be seen as a functor c^{op} ⇒ (d^{op} ⇒

(d ↦ c)|_{S})|_{S∈J(C)}.

8.22 A glimpse on Synthetic Differential Geometry

8.23 Appendix: reading some trees and diagrams aloud

a:A, b:B(a) ⊢ … A:∗, B:∗, R:(A × B → Ω), b:{ b ∈ B | R(a, b) } ⊢ …

\begin{matrix}A:∗ & B:∗ \\ A × B:∗ \end{matrix} ; p:A × B s  \begin{matrix}A:∗ ⊢ A:∗ & B:∗ ⊢ B:∗ \\ A:∗, B:∗ ⊢ A × B:∗ \end{matrix} ; A:∗, B:∗, p:A × B ⊢ p:A × B

\begin{aligned}⊤[P]:... & \begin{matrix}ω[P] : Ω & ω[Q] : Ω \\ ω[P [figure]Q] : Ω \end{matrix} ; ⊤[P [figure]Q]:E[⊤[P [figure]Q]] \\ & ⊤[Q] \end{aligned}

We can think on a logical natural deduction as being a functional natural deduction over a system with dependent types, where entities like ω[P], ω[Q], ω[P [figure]Q], … are related by certain logical rules (seen in a functional way).

Note that we do not “suppose ω[P [figure]Q]”, like we suppose ω[P] and ω[Q]; ω[P [figure]Q] is built from ω[P] and ω[Q].

Natural deduction Sequent calculus Adding the quantifiers Proofs, witnesses, subsets, worlds, The “s” rule; contraction The pronounciation (including witnesses) comes mainly from set theory, a

bit from λ-calculus; but PinS-T, so we need the “right set theory”... Give an idea of term models (as an extreme case of realisability), motivate categorical models.

8.24 Appendix: Writing down the handwaving over diagrams

8.25 Dependencies between chapters

[figure: λ→; skel- etons; skel- etons; sequents; sequents; ‘⟨, ⟩’, ‘↦’, ; and ‘cur’ as ; functors and ; adjoints; ‘⟨, ⟩’, ‘↦’, ; and ‘cur’ as ; functors and ; adjoints; fibrations; fibrations; PLC; PLC; λC in cats: ; Hyland/ ; Pitts; fibrations; λC in cats: ; Hyland/ ; Pitts; sequents; CCCs; CCCs; ‘⟨, ⟩’, ‘↦’, ; and ‘cur’ as ; functors and ; adjoints; λ→; CCCs; λ→; λC; λC; □∗; □∗; PLC; □∗; HM; HM; ML/ Haskell; □∗; paramet- ricity; paramet- ricity; functors for free; λC; λC in cats: ; Hyland/ ; Pitts; λC; Logic ; in λC; Logic ; in λC; paramet- ricity; Logic ; in λC; Cats in ; λC+Prop; Cats in ; λC+Prop; functors for free; Logic ; in λC; λC+Prop; λC+Prop; Cats in ; λC+Prop]

Saldo de hoje (2002sep27) da apresentação pro Luiz Carlos e pro Nicolau: definir pre-termos; dar exemplos de pre-termos patológicos (λa:a.a, λa:□.□);

enfatizar que num pre-judgement eu não posso ter variáveis repetidas; sublinhar todas as meta-variáveis que representam ou variáveis ou pré-termos, pra indicar que elas moram na meta-linguagem – aliás, ó que bacana, aí eu posso sublinhar em separado o B(a) e o c em B(a)c; definir o que é um “typing” (um prejudgement é uma seqüência de typings de variáveis, turnstile, typing de um pre-termo); explicar que o λC é standard (ver p.ex. o Barendregt) mas o λC com cara de dedução natural é meu; dois sentidos para seqüentes: com regras pro antecedente, ou só com contextos explícitos; reescrever a leitura em voz alta de λa:A.b e Πa:A.B com cada caracter tendo uma pronúncia separada; adicionar as regras pro Σ, mas explicar que elas não vão importar muito no início; pôr um “fantasma” pra parte direita do meu diagrama, falando do λC com cara de dedução natural; adicionar a observação de que se cada variável aparece com um só tipo, então o app pode nos forçar a mudar nomes de variáveis

c:C(a, b)

(fd):A

(λa:A.λb:B(a).c)(fd):(Πb′:B(fd).c)

e repara que é em casos tipo esse – em que o (fd) não está em forma betanormal – que eu posso precisar da regra conv.

[figure: D; J × Π_{f}(B); h; J × Π_{f}(B); Π_{f}(B); p; D; C; J × Π_{f}(B); B; ϵ; Π_{f}(B); I; f_{#}(b); C; B; g; B; J; b; J; I; f; i, j, (j ↦ b); i, j, (j ↦ b); i, j, (j ↦ b); i, (j ↦ b); i, j, (j ↦ b); i, j, b, c; i, j, (j ↦ b); i, j, b; i, (j ↦ b); i; i, j, b, c; i, j, b; i, j, b; i, j; i, j; i]

Esquema pro colóquio do Bernardo

O que a gente quer: simplificar vários assuntos, conseguir ler vários livros interessantes, salvar as pessoas que estejam fora da cultura oral... o problema do “é óbvio” (não é óbvio pra mim); programas de computador; software livre e informação livre; salvar o mundo. 11 de maio.

Conectar algumas linguagens: tipos (lógica, λ-cálculo), categorias, esqueletos — intuição.

λ-cálculo simplesmente tipado, isomorfismo de Curry-Howard.

\begin{matrix}\begin{matrix}[a : A]^{1} & b : B \\ ⟨a, b⟩ : A × B \end{matrix} & f : A × B → C \\ f(⟨a, b⟩) : C \end{matrix} ; λa:A.f(⟨a, b⟩) : A → C ; 1  \begin{aligned}\begin{matrix}[A]^{1} & B \\ A ∧ B \end{matrix} & A ∧ B → C \\ & C \end{aligned} ; A → C ; 1

isso visto como proposições, e como composição de demonstrações linguagem de esqueletos; dicionário; E e ↦

\begin{aligned}\begin{matrix}[a]^{1} & b \\ a, b \end{matrix} & a, b ↦ c \\ & c \end{aligned} ; a ↦ c ; 1

como encontrar uma “construção natural para um cara de um certo tipo”? Exemplo: a, b ↦ b, a

Repare que os “termos” crescem na versão λ-cálculo, mas não na com tipos, ou na dos esqueletos.

Passando pra seqüentes; vendo tudo como funções. Não importa que conjuntos nós escolhemos como sendo A, B, C...

Um pouquinho mais sobre λ-cálculo: um diagrama de reduções, e a que que isso corresponde sobre árvores que são deduções.

Trailer: identidade polimórfica, demonstrações construtivas, outra lógica, aplicação e abstração em ML e Haskell (Hindley-Milner).

Todas as regras do Calculus of Constructions; subsistemas. Polymorphism is not set-theoretic; Polymorphism is set-theoretic, constructively. Exemplos das adjunções do Π e do Σ.

Voltando: agora tudo acontece entre funções, e os pontos podem ser meras figuras de linguagem...

Categorias — primeiro na notação usual. Set é uma categoria; categorias construídas na marra, a partir de um conjunto de objetos e um de morfismos. Associatividade, comutatividade (no meu sentido) e colagem de células comutativas. O que eu vinha fazendo antes, com a notação de contextos — a:A ↦ b:B, b := f(a). Notação com ‘O’ e ‘Cat’; porque essa notação é boa: pequenas coerências. Umas categorias simples e engraçadas: op, e produto.

Uma CCC é uma categoria com produtos finitos e exponenciais; um topos é uma CCC com um objeto classificador; numa CCC eu sei interpretar λ-cálculo; num topos eu sei interpretar teoria dos conjuntos. Se algo não for conseqüência direta dos axiomas, então eu devo ter um modelo que “falsifique” esse algo; e eu tenho toposes interessantíssimos, bem fáceis de descrever — categorias de funtores (presheaves).

Dois exemplos de funtores: x ⇒ (a ↦ x) e x ⇒ (a, x); c ⇒ c^{F}. Porque a notação c ⇒ c^{F} — o diagraminha que comuta, para funtores. A generalização: O e Cat. Transformações naturais. Exemplo genérico: c →^{•} (c^{F} ↦ c^{G}). Quais diagramas comutam quando eu uso TNs. Quando eu mostrar funtores e TNs explicitamente eu só vou mostrar as construções, e não vou provar as identidades chatas! Minha figura detalhada para essa adjunção, com todas as construções.

Diagramas de produtos; o funtor produto; o funtor exponencial, como adjunta à direita dele. Meus dois jeitos de falar do que é a adjunta — um termão linear, e o diagrama quadrado. Os dois funtores, em λ-cálculo.

Transformações lineares e funtores: mudança de nível, isso pede um λ-cálculo mais malandro. Theorems for free!

Aqui a coisa bifurca várias vezes... direções possíveis: Yonedas, e provas sobre a naturalidade desses caras; toposes; modelos categóricos para teorias de tipos. Algumas coisas que eu posso mostrar quase rápido: o modelo para PLC, usando fibrações (explicar pullbacks antes); um topos como uma fibração.

Esquema velho pro colóquio do Bernardo Pequeníssima introdução ao λ-cálculo tipado significado do λ representação de termos por tabelinhas (no caso em que os tipos todos correspondem a conjuntos finitos) e se a gente não sabe os conjuntos correspondentes aos tipos? queremos capturar o comportamento do caso geral usando regras sintáticas exemplo de um mapa de reduções (minha tese de mestrado) alfa-equivalência beta-redução primeiro vislumbre da notação curta: E[a, b ↦ b, a] = (A × B) → (B × A)

Deduções naturais - notação de tipos, notação de termos, minha notação Outra visão: cálculo proposicional, com a mesma estrutura P, Prfs[P], ω[P], ⊤[P], prf[P] turnstiles e seqüentes Isomorfismo de Curry-Howard porquê isomorfismo? mostrar os posets entre árvores (as setas são as reduções)

uma linguagem só de setas: categorias regras de DN na nova linguagem

primeiro funtor: Hom(A, −) funtores são pacotes com duas coisas notação curta: como obter o x ⇒ (a ↦ x) natural? o que é uma categoria produtos, etc um sistema de dedução natural pra esses caras (um vislumbre)

passando pra uma categoria qualquer: tome uma subcategoria de Set proíba falar de pontos, mas dê nomes às setas como em λ-cálculo, pode até ser que eu tenha só tabelas e sintaxe — f∘g = h,

por exemplo.

mas vamos ter outros casos! meu truque, com “:=”s nas setas O[], Cat[] Uma categoria engraçada: funtores entre duas categorias, com TNs grande slogan: uma CCC é uma categoria em que se pode interpretar xxx,

um topos é isso com set theory.

Yonedinha: (x →^{•} ((a ↦ x) → (b ↦ x))) ↔ (b → a) Yonedão: ... árvores correspondentes será que o nome desses caras ”é” esses caras? “é óbvio que”

CONTENTS 79

Part of a construction that appears in MM...

\begin{matrix}[V^{op} →^{•} (⊤|_{V ∈S′′} ↪ ⊤|_{V ∈S′})]^{2} & [V^{op} →^{•} (⊤|_{V ∈S′} ↦ p^{V})]^{1} \\ V^{op} →^{•} (⊤|_{V ∈S′′} ↦ p^{V}) \end{matrix}

(V^{op} →^{•} (⊤|_{V ∈S′} ↦ p^{V}) ↦ (V^{op} →^{•} (⊤|_{V ∈S′′} ↦ p^{V})) 1

(V^{op} ⇒ ⊤|_{V ∈S})^{op} ⇒ (V^{op} →^{•} (⊤|_{V ∈S} ↦ p^{V})) 2

{[O[V^{op} ⇒ ⊤|_{V ∈S}]]^{2} \atop V^{op} →^{•} (⊤|_{V ∈S} ↪ ⊤|_{V ⊂⋃S})} [V^{op} →^{•} (⊤|_{V ⊂⋃S↦p^{V}})]^{1}

V^{op} →^{•} (⊤|_{V ∈S} ↦ p^{V})

(V^{op} →^{•} (⊤|_{V ⊂⋃S} ↦ p^{V})) ↦ (V^{op} →^{•} (⊤|_{V ∈S} ↦ p^{V}))

1

(V^{op} ⇒ ⊤|_{V ∈S}) →^{•} ((V^{op} →^{•} (⊤|_{V ⊂⋃S↦p^{V}})) ↦ (V^{op} →^{•} (⊤|_{V ∈S} ↦ p^{V})))

2