Quick
index
main
eev
maths
blogme
dednat4
littlelangs

emacs
lua
(la)tex
fvwm
tcl
forth
icon
debian
debian-rj
w32/AIX
politics
personal
heroes
irc
contact

Hyperdoctrines

Quick 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