/
Doctrine.lagda.md
293 lines (236 loc) · 9.93 KB
/
Doctrine.lagda.md
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
<!--
```agda
open import Cat.Displayed.Cocartesian
open import Cat.Diagram.Limit.Finite
open import Cat.Displayed.Cartesian
open import Cat.Diagram.Pullback
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Displayed.Fibre
open import Cat.Displayed.Base
open import Cat.Prelude
open import Order.Base
import Cat.Displayed.Reasoning as Disp
import Cat.Reasoning as Cat
import Order.Reasoning
```
-->
```agda
module Cat.Displayed.Doctrine {o ℓ} (B : Precategory o ℓ) where
```
<!--
```agda
open Cat B
```
-->
# Regular hyperdoctrines {defines="regular-hyperdoctrine"}
A **regular hyperdoctrine** is a generalisation of the defining features
of the [[poset of subobjects]] of a [[regular category]]; More
abstractly, it axiomatises exactly what is necessary to interpret
first-order (regular) logic _over_ a [[finitely complete category]].
There is quite a lot of data involved, so we'll present it in stages.
::: warning
While the _raison d'être_ of regular hyperdoctrines is the
interpretation of regular logic, that is far too much stuff for Agda to
handle if it were placed in this module. **The interpretation of logic
lives at [[logic in a hyperdoctrine]]**.
:::
```agda
record Regular-hyperdoctrine o' ℓ' : Type (o ⊔ ℓ ⊔ lsuc (o' ⊔ ℓ')) where
```
To start with, fix a category $\cB$, which we think of as the _category
of contexts_ of our logic --- though keep in mind the definition works
over a completely arbitrary category. The heart of a regular
hyperdoctrine is a [[displayed category]] $\bP \liesover \cB$, which, a
priori, assigns to every object $\Gamma : \cB$ a category $\bP(\Gamma)$
of **predicates** over it, where the set $\hom(\phi, \psi)$ for $\phi,
\psi : \bP(\Gamma)$ interprets the **entailment** relation between
predicates; we therefore write $\phi \vdash_\Gamma \psi$.
```agda
field
ℙ : Displayed B o' ℓ'
module ℙ = Displayed ℙ
```
However, having an entire _category_ of predicates is hard to make
well-behaved: that would lend itself more to an interpretation of
dependent type theory, rather than the first-order logic we are
concerned with. Therefore, we impose the following three restrictions on
$\bP$:
```agda
field
has-is-set : ∀ Γ → is-set ℙ.Ob[ Γ ]
has-is-thin : ∀ {x y} {f : Hom x y} x' y' → is-prop (ℙ.Hom[ f ] x' y')
has-univalence : ∀ x → is-category (Fibre ℙ x)
```
First, the space of predicates over $\Gamma$ must be a [[set]]. Second,
the entailment relation $\phi \vdash_\Gamma \psi$ must be a
[[proposition]], rather than an arbitrary set --- which we will use as
justification to omit the names of its inhabitants. Finally, each
[[fibre category]] $\bP(\Gamma)$ must be [[univalent|univalent
category]]. In light of the previous restriction, this means that each
fibre satisfies _antisymmetry_, or, specialising to logic, that
inter-derivable propositions are indistinguishable.
Next, each fibre $\bP(\Gamma)$ must be [[finitely complete]]. The binary
products interpret conjunction, and the terminal object interprets the
true proposition; since we are working with posets, these two shapes of
limit suffice to have full finite completeness.
```agda
fibrewise-meet : ∀ {x} x' y' → Product (Fibre ℙ x) x' y'
fibrewise-top : ∀ x → Terminal (Fibre ℙ x)
```
Everything we have so far is fine, but it only allows us to talk about
predicates over a _specific_ context, and we do not yet have an
interpretation of _substitution_ that would allow us to move between
fibres. This condition is fortunately very easy to state: it suffices to
ask that $\bP$ be a [[Cartesian fibration]].
```agda
cartesian : Cartesian-fibration ℙ
```
We're almost done with the structure. To handle existential
quantification, the remaining connective of regular logic, we use the
key insight of Lawvere: the existential elimination and introduction
rules
<div class=mathpar>
$$
\frac{\phi \vdash_{x} \psi}{\exists_x \phi \vdash \psi}
$$
$$
\frac{\exists_x \phi \vdash \psi}{\phi \vdash_{x} \psi}
$$
</div>
say precisely that existential quantification along $x$ is [[left
adjoint]] to weakening by $x$! Since weakening will be interpreted by
[[cartesian lifts]], we will interpret the existential quantification by
a left adjoint to that: in other words, $\bP$ must also be a
[[cocartesian fibration]] over $\bP$.
```agda
cocartesian : Cocartesian-fibration ℙ
```
Note that we have assumed the existence of left adjoints to arbitrary
substitutions, which correspond to forms of existential quantification
more general than quantification over the latest variable. For example,
if the base category $\cB$ has finite products, then existential
quantification of a predicate $\phi : \bP(A)$ over $\delta : A \to A
\times A$ corresponds to the predicate "$(i, j) \mapsto (i = j) \land
\phi(i)$".
<details>
<summary>That concludes the _data_ of a regular hyperdoctrine. We will
soon write down the axioms it must satisfy: but before that, we need a
digression to introduce better notation for working with the
deeply-nested data we have introduced.
</summary>
```agda
module cartesian = Cartesian-fibration cartesian
module cocartesian = Cocartesian-fibration cocartesian
module fibrewise-meet {x} (x' y' : ℙ.Ob[ x ]) = Product (fibrewise-meet x' y')
module fibrewise-top x = Terminal (fibrewise-top x)
_[_] : ∀ {x y} → ℙ.Ob[ x ] → Hom y x → ℙ.Ob[ y ]
_[_] x f = cartesian.has-lift.x' f x
exists : ∀ {x y} (f : Hom x y) → ℙ.Ob[ x ] → ℙ.Ob[ y ]
exists = cocartesian.has-lift.y'
_&_ : ∀ {x} (p q : ℙ.Ob[ x ]) → ℙ.Ob[ x ]
_&_ = fibrewise-meet.apex
aye : ∀ {x} → ℙ.Ob[ x ]
aye = fibrewise-top.top _
infix 30 _[_]
infix 25 _&_
```
</details>
The first two axioms concern the commutativity of substitution and the
conjunctive connectives:
```agda
field
subst-&
: ∀ {x y} (f : Hom y x) (x' y' : ℙ.Ob[ x ])
→ (x' & y') [ f ] ≡ x' [ f ] & y' [ f ]
subst-aye
: ∀ {x y} (f : Hom y x)
→ aye [ f ] ≡ aye
```
Next, we have a _structural rule_, called **Frobenius reciprocity**,
governing the interaction of existential quantification and conjunction.
If substitution were invisible, it would say that $(\exists \phi) \land
\psi$ is $\exists (\phi \land \psi)$; Unfortunately, proof assistants
force us to instead say that if we have $\phi : \bP(\Gamma)$, $\psi :
\bP(\Delta)$, and $\rho : \Gamma \to \Delta$, then $\exists_\rho(\phi)
\land \psi$ is $\exists_\rho(\phi \land \psi[\rho])$.
```agda
field
frobenius
: ∀ {x y} (f : Hom x y) {α : ℙ.Ob[ x ]} {β : ℙ.Ob[ y ]}
→ exists f α & β ≡ exists f (α & β [ f ])
```
Finally, we have a general rule for the commutativity of existential
quantification and substitution. While in general the order matters, the
**Beck-Chevalley condition** says that we can conclude
$$
\exists_h (a[k]) = (\exists_g a)[f]
$$
provided that the square
~~~{.quiver}
\[\begin{tikzcd}[ampersand replacement=\&]
d \&\& a \\
\\
b \&\& c
\arrow["k"', from=1-1, to=3-1]
\arrow["h", from=1-1, to=1-3]
\arrow["f", from=1-3, to=3-3]
\arrow["g"', from=3-1, to=3-3]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=3-3]
\end{tikzcd}\]
~~~
is a pullback.
```agda
beck-chevalley
: ∀ {a b c d} {f : Hom a c} {g : Hom b c} {h : Hom d a} {k : Hom d b}
→ is-pullback B h f k g
→ ∀ {α} → exists h (α [ k ]) ≡ (exists g α) [ f ]
```
That concludes the definition of regular hyperdoctrine. Said snappily, a
**regular hyperdoctrine** $\bP \liesover \cB$ is a [[bifibration]] into
[[(meet-)semilattices|meet-semilattice]] satisfying Frobenius reciprocity and
the Beck-Chevalley condition.
<!--
```agda
≤-Poset : ∀ {x : Ob} → Poset o' ℓ'
≤-Poset {x = x} .Poset.Ob = ℙ.Ob[ x ]
≤-Poset {x = x} .Poset._≤_ = ℙ.Hom[ id ]
≤-Poset {x = x} .Poset.≤-thin = has-is-thin _ _
≤-Poset {x = x} .Poset.≤-refl = ℙ.id'
≤-Poset {x = x} .Poset.≤-trans α β = Precategory._∘_ (Fibre ℙ _) β α
≤-Poset {x = x} .Poset.≤-antisym α β = has-univalence _ .to-path $
Cat.make-iso (Fibre ℙ _) α β (has-is-thin _ _ _ _) (has-is-thin _ _ _ _)
module _ {x} where
open Order.Reasoning (≤-Poset {x}) hiding (Ob-is-set ; Ob) public
open Disp ℙ public
subst-∘ : ∀ {x y z} (f : Hom y z) (g : Hom x y) {α} → (α [ f ]) [ g ] ≡ α [ f ∘ g ]
subst-∘ f g = ≤-antisym
(cartesian.has-lift.universalv _ _
(cartesian.has-lift.lifting _ _ ℙ.∘' cartesian.has-lift.lifting _ _))
(cartesian.has-lift.universalv _ _
(cartesian.has-lift.universal f _ g (cartesian.has-lift.lifting _ _)))
subst-id : ∀ {x} (α : ℙ.Ob[ x ]) → α [ id ] ≡ α
subst-id α = ≤-antisym
(cartesian.has-lift.lifting id α)
(cartesian.has-lift.universal id α _ (ℙ.id' ℙ.∘' ℙ.id'))
subst-≤ : ∀ {x y} (f : Hom x y) {α β : ℙ.Ob[ y ]} → α ≤ β → α [ f ] ≤ β [ f ]
subst-≤ f p = cartesian.has-lift.universalv f _ $
hom[ idl _ ] (p ℙ.∘' cartesian.has-lift.lifting f _)
exists-id : ∀ {x} (α : ℙ.Ob[ x ]) → exists id α ≡ α
exists-id α = ≤-antisym
(cocartesian.has-lift.universal id α _ (ℙ.id' ℙ.∘' ℙ.id'))
(cocartesian.has-lift.lifting id α)
&-univ : ∀ {x} {α β γ : ℙ.Ob[ x ]} → α ≤ β → α ≤ γ → α ≤ (β & γ)
&-univ p q = fibrewise-meet.⟨_,_⟩ _ _ p q
&-comm : ∀ {x} {α β : ℙ.Ob[ x ]} → α & β ≡ β & α
&-comm = ≤-antisym
(&-univ (fibrewise-meet.π₂ _ _) (fibrewise-meet.π₁ _ _))
(&-univ (fibrewise-meet.π₂ _ _) (fibrewise-meet.π₁ _ _))
≤-exists : ∀ {x y} (f : Hom x y) {α β} → α ≤ β [ f ] → exists f α ≤ β
≤-exists f p = cocartesian.has-lift.universalv f _ $
hom[ idr f ] (cartesian.has-lift.lifting f _ ℙ.∘' p)
subst-! : ∀ {x y} (f : Hom y x) {α} → ℙ.Hom[ id ] α (aye [ f ])
subst-! f {α} = subst (λ e → ℙ.Hom[ id ] α e) (sym (subst-aye f))
(Terminal.! (fibrewise-top _))
```
-->