HyperdoctrinesQuick index:
1. LPCE: rules ============== These are slightly different than the ones at [Hyp] because my ":"s list all their hypotheses at the top, not just the one being discharged. Sometimes I also list the variables - these derivations are happening in a fibration. P Q P&Q P&Q (&) ----- --- --- P&Q P Q [P]^1 R [Q]^1 R : : (\/) P Q P\/Q S S ---- ---- -------------------- P\/Q P\/Q S P [Q]^1 : (⊃) R Q Q⊃R --- ------ Q⊃R R a;P a : : (∀) a,b;Q b(a) a;∀b.P(b) ------ --------------- a;∀b.Q a;P(b(a)) P : (∃) P(b(a)) ∃b.P Q ------- -------- ∃b.P(b) Q P ⊥ . (⊤/⊥) - - ⊤ Q 2. LPCE rules for equality ========================== a : (=I) b(a) ⊤ . --------- b(a)=b(a) (=E) b=b' c=c' P(b,c) ------------------ (?) P(b',c') 3. LPCE rules for equality ========================== --| P |-- / - \ (&I,&E) / | \ v v v Q <---| Q&R |---> R P |---> P\/Q <---| Q / - \ (\/I,\/E) \ | / ("R" is omitted here...) \ v / --> S <-- P&Q <==== P (Q⊃R)&Q <== Q⊃R - - - - (⊃I) | |--> | (⊃E) | <--| | id v v | | R ====> Q⊃R R =====> Q⊃R Q(a) <====== Q(a) Q(a) <======= Q(a) <======== Q(a) - - - - - (∀I) | |--> | (∀E) | <--| | <--| | v v v v v R(a,b) ==> ∀b.R(a,b) R(a,b(a)) <=== R(a,b) ====> ∀b.R(a,b) b:=b(a) a,b |-------> a a |-------> a,b |---------> a P(a,b(a)) <===== P(a,b) ====> ∃b.P(a,b) P(a,b) ==> ∃b.P(a,b) - - - - - (∃I) | <--| | <--| | id (∃E) | |--> | v v v v v ∃b.P(a,b) <=== ∃b.P(a,b) <=== ∃b.P(a,b) Q(a) <==== Q(a) b:=b(a) a |-------> a,b |---------> a a,b |------> a 4. Fibrations (1) ================= The formal definition of fibration seems very artificial at first, so let's start with some hindsight - [Note: ``\ovl{f}'' is ``\overline{f}''] f:A->B a morphism in the base category P:={b||P(b)}, an object over B Q:={b||Q(b)} an object over B Set^>->(A) := proj^-1(A) the fiber over A Set^>->(B) := proj^-1(B) the fiber over B f^*: Set^>->(B) -> Set^>->(A) change-of-base functor P |-> f^*(P) {b||P(b)} |-> {a||P(f(a))} \ovl{f}: f^* -> id a natural transformation \ovl{f}P: f^*P -> P a cartesian morphism (a cart. lifting of f at P) \ovl{f}P □ . -------> |----> {a||P(f(a))} <------| {b||P(b)} P(f(a)) <===== P(b) - f^* - - - | | | | f^*(g)| <-| |g | <--| | | | | | | \ovl{f}P | | □ | v -------> v v |----> v {a||Q(f(a))} <------| {b||Q(b)} Q(f(a)) <===== Q(b) f^* f A ----------------> B a |--------> b In DNC we will mark cartesian morphisms with a `□'. 5. Cartesian morphisms (categorically) ====================================== Here is the formal definition of cartesian morphism. Any morphism b||Q |-> c||R induces a natural transformation: / P \ / P |-----\ \ | |-> | | v | . | Q | nat | Q |-> R | a||P^op --> ( | | |-> | | ) | | | a |-----\ | | | | |-> v | \ / \ b |-> c / When that natural transformation is a natural isomorphism we say that the b||Q |-> c||R is cartesian. The inverse of the `nat' map above gives the factorization of the a||P |-> c||R through b||Q |-> c||R, over a|->b. 6. The adjunctions for Σ and Π in half-DNC ========================================== c ======> b,c (|->) - - | <--| | (<-|) (|->) v v d <======= d (<-|) - - | |--> | (<-|) (|->) v v e ======> b|->e (|->) a,b |-----> a c ======> b,c - - a,b;c|-c'(b,c) | |--> | a;p|-<πp,c'(πp,π'p)> v v c' =====> b,c' - - a,b;c'|-d(b,c') | |--> | a;p|-d(πp,π'p) a,b;c'|-d(<b,c'>) | <--| | a;p|-d(p) v v d <======= d - - a,b;d|-d'(d) | <--| | a;d|-d'(d) v v d' <====== d' - - a,b;d'|-f(d')(b) | <--| | a;d'|-f(d) a,b;d'|-e(b,d') | |--> | a;d'|-λb,e(b,d') v v e ======> b|->e - - a,b;e|-e'(b,e) | |--> | a;f|-λb.e'(b,fb) v v e' =====> b|->e' a,b |-----> a 7. BCC in half-DNC ================== d ======================> c,d -/\ - | \\ |---> | v \\ v c,d <\\=================== c,d /\ \\ /\ \\ d =====================> c,d \\ | \\ - \\ | <---| \\ | id \\v \\v c,d <==================== c,d a,c |--------------------> a - __| - \ \ v v b,c |---------------------> b d =======================> p -/\ - | \\ |---> | v \\ v <c,d> <=\\================= <πp,π'p> /\ \\ /\ \\ d ======================> p \\ | \\ - \\ | <---| \\ | id \\v \\v <c,d> <==================== p a,c |--------------------> a - __| - \ \ v v b,c |---------------------> b 8. Hyperdoctrines ================= Hyperdoctrines are categories where we can interpret (a certain system of intuitionistic, typed) first-order logic. Our favorite (archetypal) hyperdoctrine is Set^>->. More generally: for any topos its fibration of subobjects is a hyperdoctrine; Set is a topos, and Sub(Set) = Set^>->. L 9. Hyperdoctrines: structure ============================ In the base category: --| a |-- a a,b <==== a / - \ - - - / | \ | | <--> | v v v v v v b <--| b,c |--> c * c ===> b|->c In each fiber: --| P |-- P P&Q <==== P / - \ - - - / | \ | | <--> | v v v v v v Q <--| Q&R |--> R ⊤ R ====> Q⊃R Between fibers: P(a,b) ===> ∃b.P(a,b) - - □ | <--> | |---> v v P(b(a)) <==== P(b) Q(a) <======= Q(a) - - | <--> | v v R(a,b) ===> ∀b.R(a,b) b:=b(a) a |--------> b a,b |-------> a Equality: P(a,b) ===> b=b'&P(a,b) - - | <--> | v v Q(a,b,b) <=== Q(a,b,b') b':=b a,b |------> a,b,b' Plus some technical conditions: Change of base preserves ⊤, &, ⊃. Beck-Chevalley (BCC) for ∃ and ∀. Frobenius. L 10. Change of base preserves ``and'' ==================================== P <============= P f^*P <-----------------| P ^ ^ ^ ^ ^ ^ | \ <-| | π_0 | \ f^*π_0 <-| | π_0 - - - | \ | P&Q <-| P&Q <=== P&Q f^*P×f^*Q <-- f^*(P×Q) <---| P×Q - - - | / | | / <-| | π_1 | / f^*π_1 <-| | π_1 v v v v v v Q <============= Q f^*Q <-----------------| Q a |---------> b A ---------f--------> B For any P, Q objects over B, f:A->B, <f^*π_0, f^*π_1>: f^*(P×Q) -> f^*P×f^*Q should be an iso. Change of base preserves ``⊤'' ============================ ⊤ <=== ⊤ f^*1 <---| 1 - | | ! | v v ⊤ 1 f a |---> b A ------> B For any f:A->B, !: f^*1 -> 1 should be an iso; that is, f^*1 should be a terminal object. 11. Change of base preserves implication ======================================== id: (P->Q) -> (P->Q) -------------------- ev: (P->Q)×P -> Q ---------------------------- f^*ev: f^*((P->Q)×P) -> f^*Q ---------------------------------------------------- <f^*π_0,f^*π_1>^-1;f^*ev: (f^*(P->Q) × f^*P) -> f^*Q ------------------------------------------------------- (<f^*π_0,f^*π_1>^-1;f^*ev)^v: f^*(P->Q) -> (f^*P->f^*Q) For any P, Q objects over B, f:A->B, this arrow should be an iso. L 12. Translating the ∃E_nd rule ============================== a,b;P(a,b),Q(a)|-R(a) ---------------------⊃I_cat [P(a,b)]^1 Q(a) a,b;P(a,b)|-Q(a)⊃R(a) : ----------------------∃E_cat ∃b.P(a,b) R(a) a;∃b.P(a,b)|-Q(a)⊃R(a) -------------------∃E_nd ----------------------⊃E_cat R(a) a;∃b.P(a,b),Q(a)|-R(a) P(a,b),Q(a) <=== P(a,b) =====> ∃b.P(a,b) ===> ∃b.P(a,b),Q(a) - - - - | |--> | |--> | |--> | v v v v R(a) ======> Q(a)⊃R(a) <=== Q(a)⊃R(a) <======= R(a) a,b ========== a,b |---------> a =============== a L 13. Translating the ∃I_nd rule ============================== {a,b||P(a,b)} P(a,b) -------------∃_0 ---------∃I_nd(w) {a||∃b.P(a,b)} ∃b.P(a,b) ----------------------id a;∃b.P(a,b)|-∃b.P(a,b) ----------------------∃I_cat P(a,b(a)) a|-b(a) a,b;P(a,b)|-∃b.P(a,b) ---------∃I_nd ----------------------------change.of.base ∃b.P(a,b) a;P(a,b(a))|-∃b.P(a,b) P(a,b(a)) <====== P(a,b) =====> ∃b.P(a,b) - - - | <--| | <--| |id v v v ∃b.P(a,b) <==== ∃b.P(a,b) <==== ∃b.P(a,b) b:=b(a) a |------------> a,b |---------> a 14. Equality in hyperdoctrines ============================== First, let's look at "proofs" of reflexivity, symmetry and transitivity in Set^>->. It's not clear that these proofs lift to arbitrary hyperdoctrines... ⊤ ========> b=b' - - refl | <--| | id v v b=b <======= b=b' b':=b a,b |-----> a,b,b' ⊤ =============> b=b' b=b' =======> b'=b''&b=b' - - - - refl | |--> | sym id | |--> | trans v v v v b=b <============ b'=b b=b' <=========== b=b'' /\ /\ // // ⊤ ==============> b'=b ⊤ ==============> b=b'' b':=b b'':=b' a,b |----------> a,b,b' a,b,b' |-------> a,b,b',b'' - - / / b':=b v b'':=b v a,b' |-----------> a,b',b a,b |-----------> a,b,b'' 15. BCC for equality ==================== P(a,c) ===============> c=c'&P(a,c) -/\ - | \\ |--> | v \\ v c=c&P(a,c) <============ c=c'&P(a,c) /\ \\ /\ \\ P(b,c) ===============> c=c'&P(b,c) \\ - \\ - \\ | <--| \\| \\v \v c=c&P(b,c) <============= c=c'&P(b,c) a,c |--------------------> a,c,c' - - \ \ v > b,c |--------------------> b,c,c' 16. Discarded diagrams ====================== ----| P |---- / - \ / | \ v v v Q <---| (Q⊃R)&Q |---> Q⊃R - <==== - (⊃E) | | ev | <---| | id | | v v R =======> Q⊃R c ===========> p - - | |--> | v v c =======> p c'(b,c) ==> <πp,c'(πp,π'p)> c =========> p - - - - | <--| | | |--> | v v v v d(<b,c>) <== d(p) d <=========== d d(b,c) <==== d(πp,π'p) - - | <--| | v v d <======= d d'(d) <======= d'(d) d <========= d - - - - | <--| | | |--> | v v v v f(d)(b) ===> f(d) e ===========> f e(b,d) ===> λb.e(b,d) - - | |--> | v v e'(b,e) ===> λb.e'(b,fb) a,b |-----> a a,b |---------> a a,b |--------> a |