[INCLUDE TH/speedbar.blogme] [SETFAVICON dednat4/dednat4-icon.png] [lua: LR = R ] [# (defun c () (interactive) (find-blogme3-sh0-if "2007hyperdoctrines")) ;; http://angg.twu.net/2007hyperdoctrines.html ;; file:///home/edrx/TH/L/2007hyperdoctrines.html #] [lua: -- (find-glyphashtml-links "bt") -- (eev-math-glyphs-edrx) eev_math_glyphs_edrx() sgmlify_table["\174"] = "⊥" sgmlify_table["\174"] = "⊥" ] [htmlize [J Hyperdoctrines] [WITHINDEX [# # «.lpce-rules» (to "lpce-rules") # «.lpce-rules-equality» (to "lpce-rules-equality") # «.lpce-rules-categorically» (to "lpce-rules-categorically") # «.fibrations-1» (to "fibrations-1") # «.cartesian-morphisms» (to "cartesian-morphisms") # «.Sum-and-Prod-in-half-DNC» (to "Sum-and-Prod-in-half-DNC") # «.BCC-in-half-DNC» (to "BCC-in-half-DNC") # «.hyperdoctrines» (to "hyperdoctrines") # «.hyperdoctrines-structure» (to "hyperdoctrines-structure") # «.change-of-base-preserves-and» (to "change-of-base-preserves-and") # «.change-of-base-preserves-imp» (to "change-of-base-preserves-imp") # «.translating-ExE-ND» (to "translating-ExE-ND") # «.translating-ExI-ND» (to "translating-ExI-ND") # «.equality-in-hds» (to "equality-in-hds") # «.BCC-for-equality» (to "BCC-for-equality") # «.discarded-diagrams» (to "discarded-diagrams") #] [RULE ----------------------------------------] [tsec «lpce-rules» (to ".lpce-rules") [++N]. 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 ] [tsec «lpce-rules-equality» (to ".lpce-rules-equality") [++N]. LPCE rules for equality ============================== a : (=I) b(a) § . --------- b(a)=b(a) (=E) b=b' c=c' P(b,c) ------------------ (?) P(b',c') ] [tsec «lpce-rules-categorically» (to ".lpce-rules-categorically") [++N]. 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 ] [tsec «fibrations-1» (to ".fibrations-1") [++N]. 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 `ñ'. ] [tsec «cartesian-morphisms» (to ".cartesian-morphisms") [++N]. 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. ] [RULE ------------------------------------------------------------] [tsec «Sum-and-Prod-in-half-DNC» (to ".Sum-and-Prod-in-half-DNC") [++N]. 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() | <--| | 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 ] [tsec «BCC-in-half-DNC» (to ".BCC-in-half-DNC") [++N]. 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 <=\\================= <p,'p> /\ \\ /\ \\ d ======================> p \\ | \\ - \\ | <---| \\ | id \\v \\v <==================== p a,c |--------------------> a - __| - \ \ v v b,c |---------------------> b ] [RULE ------------------------------------------------------------] [# (find-orgfile "Categories.org" "Hyperdoctrines: structure in DNC") #] [tsec «hyperdoctrines» (to ".hyperdoctrines") [++N]. 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^>->. ] [tsec «hyperdoctrines-structure» (to ".hyperdoctrines-structure") [++N]. 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. ] [tsec «change-of-base-preserves-and» (to ".change-of-base-preserves-and") [++N]. 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^*(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. ] [tsec «change-of-base-preserves-imp» (to ".change-of-base-preserves-imp") [++N]. Change of base preserves implication =========================================== id: (P->Q) -> (P->Q) -------------------- ev: (P->Q)×P -> Q ---------------------------- f^*ev: f^*((P->Q)×P) -> f^*Q ---------------------------------------------------- ^-1;f^*ev: (f^*(P->Q) × f^*P) -> f^*Q ------------------------------------------------------- (^-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. ] [tsec «translating-ExE-ND» (to ".translating-ExE-ND") [++N]. 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 ] [tsec «translating-ExI-ND» (to ".translating-ExI-ND") [++N]. 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 ] [tsec «equality-in-hds» (to ".equality-in-hds") [++N]. 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'' ] [tsec «BCC-for-equality» (to ".BCC-for-equality") [++N]. 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' ] [tsec «discarded-diagrams» (to ".discarded-diagrams") [++N]. 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() <== 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 ] ] ] [# # Local Variables: # coding: raw-text-unix # modes: (fundamental-mode blogme-mode) # End: #]