Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
% (find-angg "LATEX/2008graphs.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008graphs.tex && latex    2008graphs.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008graphs.tex && pdflatex 2008graphs.tex"))
% (eev "cd ~/LATEX/ && Scp 2008graphs.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (find-dvipage "~/LATEX/2008graphs.dvi")
% (find-pspage  "~/LATEX/2008graphs.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips  -D 300 -P pk -o 2008graphs.ps 2008graphs.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvired -D 300 -P pk -o 2008graphs.ps 2008graphs.dvi")
% (find-pspage  "~/LATEX/2008graphs.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage  "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2008graphs.pdf" (ee-twupfile "LATEX/2008graphs.pdf") 'over)
% (ee-cp "~/LATEX/2008graphs.pdf" (ee-twusfile "LATEX/2008graphs.pdf") 'over)
% (find-angg "LATEX/2008sheaves.tex")
% http://angg.twu.net/LATEX/2008graphs.pdf

% (find-dn4tex-links "2008graphs")
% (defun d () (interactive) (find-dvipage "~/LATEX/2008graphs.dvi"))
% (find-dvipage "~/LATEX/2008graphs.dvi")

% «.nd-to-sc»				(to "nd-to-sc")
% «.heyting-algebras»			(to "heyting-algebras")
% «.calculating-VimpW»			(to "calculating-VimpW")
% «.curry-howard-1»			(to "curry-howard-1")
% «.dags-as-heyting-algebras»		(to "dags-as-heyting-algebras")
% «.preamble-dgs-and-topologies»	(to "preamble-dgs-and-topologies")
% «.preamble-dg-to-topology»		(to "preamble-dg-to-topology")
% «.preamble-truth-values»		(to "preamble-truth-values")
% «.topological-spaces»			(to "topological-spaces")
% «.preorders-and-posets»		(to "preorders-and-posets")
% «.minimal-dag»			(to "minimal-dag")
% «.presheaves»				(to "presheaves")
% «.subtopology-of-R»			(to "subtopology-of-R")
% «.coherent-families»			(to "coherent-families")
% «.saturation»				(to "saturation")
% «.a-presheaf-on-a-dag»		(to "a-presheaf-on-a-dag")
% «.presheaf-on-a-dag-germs»		(to "presheaf-on-a-dag-germs")
% «.denses-and-stables»			(to "denses-and-stables")
% «.subst-for-iff»			(to "subst-for-iff")
% «.LT-modalities»			(to "LT-modalities")
% «.LT-modalities-and»			(to "LT-modalities-and")
% «.LT-modalities-or»			(to "LT-modalities-or")
% «.LT-modalities-imp»			(to "LT-modalities-imp")
% «.tops-for-or-and-imp»		(to "tops-for-or-and-imp")
% «.more-about-not-not»			(to "more-about-not-not")
% «.modalities-alt-axioms»		(to "modalities-alt-axioms")
% «.LT-modalities-quants»		(to "LT-modalities-quants")
% «.embedding»				(to "embedding")
% «.sat-cov-fibration»			(to "sat-cov-fibration")
% «.geometric-morphisms»		(to "geometric-morphisms")



\documentclass[oneside]{book}
\usepackage[latin1]{inputenc}
\usepackage{edrx08}       % (find-dn4ex "edrx08.sty")
%L process "edrx08.sty"  -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex   % (find-dn4ex "edrxheadfoot.tex")
\begin{document}

\input 2008graphs.dnt

%*
% (eedn4-51-bounded)

Index of the slides:
\msk
% To update the list of slides uncomment this line:
\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")
\tocline {Natural Deduction and Sequent Calculus} {2}
\tocline {Heyting Algebras} {3}
\tocline {Some DAGs are Heyting Algebras} {4}
\tocline {Calculating $V⊃W$} {5}
\tocline {``Mundo funcional'' e ``Mundo l\'ogico'' (Curry-Howard)} {6}
\tocline {Preamble: DGs and topologies} {7}
\tocline {Preamble: each DG induces a topology} {8}
\tocline {Preamble: truth-values} {9}
\tocline {Topological spaces} {10}
\tocline {Preorders and partial orders} {11}
\tocline {The minimal DAG for a topology} {12}
\tocline {Presheaves} {13}
\tocline {A subtopology of $\R $} {14}
\tocline {Coherent families} {15}
\tocline {Saturation and bisaturation} {16}
\tocline {A (bad) presheaf on a DAG} {17}
\tocline {A presheaf on a DAG: its space of germs} {18}
\tocline {Dense and stable truth-values} {19}
\tocline {Substitution principles for `$\Leftrightarrow $'} {20}
\tocline {Lawvere-Tierney Modalities} {21}
\tocline {LT-modalities and `and'} {22}
\tocline {LT-modalities and `or'} {23}
\tocline {LT-modalities and implication} {24}
\tocline {The topologies for `or' and `implies'} {25}
\tocline {More about double negation} {26}
\tocline {Modalities: alternative axioms} {27}
\tocline {LT-modalities and the quantifiers} {28}
\tocline {The fibration of saturated covers} {29}
\tocline {Embedding} {30}
\tocline {Geometric morphisms} {31}


% ----------
% Definitions

\def\bbV{\mathbb{V}}
\def\Nondecr{{Nondecr}}
\def\emp{\emptyset}
\def\DG{{DG}}
\def\Vee{\dagVee}
\def\O{\Opens}
\def\OX{\O(X)}
\def\OR{{\Opens(\R)}}
\def\D{\mathbb{D}}
\def\V{\mathbb{V}}
\def\Cinfty{\mathcal{C}^\infty}
\def\bbV{{\mathbb{V}}}
\def\calU{{\mathcal{U}}}
\def\calV{{\mathcal{V}}}
\def\calW{{\mathcal{W}}}
\def\DG {{DG}}
\def\DAG{{DAG}}
\def\Top{{Top}}
\def\TopCAI{{TopCAI}}
\def\Iinfty{{\bigcap_\infty}}
\def\cai{{cai}}
\def\dquo#1{\text{``$#1$''}}
%:****^{**}*
%:***^**
%:*<=>*\Bij *
%:*&*\&*
%:*\&*\&*



\newpage
% --------------------
% «nd-to-sc»  (to ".nd-to-sc")
% (s "Natural Deduction and Sequent Calculus" "nd-to-sc")
\myslide {Natural Deduction and Sequent Calculus} {nd-to-sc}

%:           [P&Q]^1                    P&Q|-P&Q          
%:           -------                    ---------          
%:  [P&Q]^1     Q     Q⊃R    P&Q|-P&Q     P&Q|-Q     Q⊃R|-Q⊃R
%:  -------     ----------   ---------    ---------------- 
%:     P            R         P&Q|-P         Q⊃R,P&Q|-R
%:     --------------          -----------------------      
%:         P&R                      Q⊃R,P&Q|-P&R
%:      ------1                    ------------
%:      P&Q⊃P&R                    Q⊃R|-P&Q⊃P&R
%:                                                         
%:      ^nd-to-sc-1                ^nd-to-sc-2
%:
$$\ded{nd-to-sc-1}$$

$$\ded{nd-to-sc-2}$$


\newpage
% --------------------
% «heyting-algebras»  (to ".heyting-algebras")
% (s "Heyting Algebras" "heyting-algebras")
\myslide {Heyting Algebras} {heyting-algebras}

A {\sl Heyting Algebra} is a 7-uple

$(, , , ∧, ∨, ⊃, \vdash)$, where:

\msk

$\begin{array}{rcl}
    ,  && , \\
 ∧, ∨, ⊃ &:& × \to ,\\
  \vdash &\subseteq&  \\
 \end{array}
$

\msk

and the relation $\vdash$ respects the following ``derivation rules'':

%D diagram O(X)-structure
%D 2Dx    100     +25     +25  +15  +20      +25
%D 2D 100     --| p0 |-	       t0   a0 <==== a1
%D 2D	     /    -    \       -     -        -
%D 2D	    /     |	\      |     |  <-->  |
%D 2D	   v      v	 v     v     v	      v
%D 2D +25 p1 <--| p2 |--> p3   t1   a2 ====> a3
%D 2D
%D 2D +15 c0 |--> c1 <--| c2   i0              
%D 2D	   -      -       -    -               
%D 2D	    \     |	 /     |               
%D 2D	     \    v	/      v               
%D 2D +25     --> c3 <--       i1              
%D 2D
%D ((            p0 .tex=  P
%D    p1 .tex= Q p2 .tex= Q∧R p3 .tex= R
%D    @ 0 @ 1 |-> @ 0 @ 2 |-> @ 0 @ 3 |->
%D    @ 1 @ 2 <-| @ 2 @ 3 |->
%D ))
%D (( c0 .tex= P c1 .tex= P∨Q c2 .tex= Q
%D               c3 .tex=  R
%D    @ 0 @ 1 |-> @ 1 @ 2 <-|
%D    @ 0 @ 3 |-> @ 1 @ 3 |-> @ 2 @ 3 |->
%D ))
%D (( t0 .tex= P t1 .tex= 
%D    @ 0 @ 1 |->
%D ))
%D (( i0 .tex=  i1 .tex= P
%D    @ 0 @ 1 |->
%D ))
%D (( a0 .tex= P∧Q a1 .tex= P
%D    a2 .tex=  R  a3 .tex= Q⊃R
%D    @ 0 @ 1 <= @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =>
%D    @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram

\bsk

$\diag{O(X)-structure}$

\bsk

%:  P|-Q  Q|-R
%:  ----------  ----
%:     P|-R     P|-P
%:
%:     ^O(x)-c  ^O(x)-id
%:
%:  P|-Q  P|-R                           P∧Q|-R
%:  ----------  ------   ------   ----   ------(\vbij)
%:    P|-Q∧R    Q∧R|-Q   Q∧R|-R   P|-   P|-Q⊃R
%:  
%:    ^O(X)-1   ^O(X)-2  ^O(X)-3  ^O(X)-4 ^O(X)-5
%:  
%:  P|-R  Q|-R
%:  ----------  ------   ------   ----
%:    P∨Q|-R    P|-P∨Q   Q|-P∨Q   |-P
%:  
%:    ^O(X)-6   ^O(X)-7  ^O(X)-8  ^O(X)-9
%:
$\begin{array}{ccccc}
 \ded{O(x)-c} & \ded{O(x)-id} \\ \\
 \ded{O(X)-1} & \ded{O(X)-2} & \ded{O(X)-3} & \ded{O(X)-4} & \ded{O(X)-5} \\ \\
 \ded{O(X)-6} & \ded{O(X)-7} & \ded{O(X)-8} & \ded{O(X)-9} \\
 \end{array}
$

\bsk

Here are three Heyting Algebras:

%D diagram three-HAs
%D 2Dx     100   +40 +20 +20      +30 +20 +20   
%D 2D  100 1         111              X         
%D 2D            
%D 2D  +20       110 101 011      U       V    
%D 2D            
%D 2D  +20       100 010 001          W
%D 2D            
%D 2D  +20 0         000             \emp       
%D 2D
%D (( 0 1 ->
%D ))
%D (( 000 001 -> 000 010 -> 000 100 ->
%D    001 011 -> 001 101 ->
%D    010 011 -> 010 110 ->
%D    100 101 -> 100 110 ->
%D    011 111 -> 101 111 -> 110 111 ->
%D ))
%D (( X .tex= \dagVee111
%D    U .tex= \dagVee101
%D    V .tex= \dagVee011
%D    W .tex= \dagVee001
%D    \emp .tex= \dagVee000
%D    \emp W -> W U -> W V -> U X -> V X -> 
%D ))
%D enddiagram
%D
$$\diag{three-HAs}$$

Note: consider the partial order induced by the DAGs above -

i.e., the reflexive/transitive closure of the DAGs.





\newpage
% --------------------
% «dags-as-heyting-algebras»  (to ".dags-as-heyting-algebras")
% (s "Some DAGs are Heyting Algebras" "dags-as-heyting-algebras")
\myslide {Some DAGs are Heyting Algebras} {dags-as-heyting-algebras}

{\bf Theorem:} if

$(, , , ∧, ∨, ⊃, \vdash)$ and

$(, ', ', ∧', ∨', ⊃', \vdash)$ are Heyting Algebras, then

we have

$ \bij '$,

$ \bij $,

and for any $P, Q  $,

$P∧Q \bij P∧'Q$,

$P∨Q \bij P∨'Q$,

$P⊃Q \bij P⊃'Q$.

\msk

{\bf Proof} (half of it):

%:  -----     -----  
%:  |-'     |-'  
%:
%:  ^dagha-1  ^dagha-2
%:
%:  ------   ------   -------   -------   
%:  P&Q|-P   P&Q|-Q   P|-P∨'Q   Q|-P∨'Q   
%:  ---------------   -----------------   
%:     P&Q|-P&'Q         P∨Q|-P∨'Q
%:                                      
%:     ^dagha-3          ^dagha-3       
%:
%:                       --------
%:                       P⊃Q|-P⊃Q
%:  =================   ----------
%:  (P⊃Q)&'P|-(P⊃Q)&P   (P⊃Q)&P|-Q
%:  ------------------------------
%:          (P⊃Q)&'P|-Q
%:          ---------
%:          P⊃Q|-P⊃'Q
%:
%:          ^dagha-4
%:
$$\ded{dagha-1} \qquad \ded{dagha-2}$$

$$\ded{dagha-3} \qquad \ded{dagha-3}$$

$$\ded{dagha-4}$$

\msk

{\bf Theorem:} if

$(, , , ∧, ∨, ⊃, \vdash)$ and

$(, ', ', ∧', ∨', ⊃', \vdash)$ are Heyting Algebras and

$(, \vdash)$ is a DAG, then

$='$, $='$, $∧=∧'$, $∨=∨'$, $⊃=⊃'$.

\ssk

So, if a DAG $(, \vdash)$ is Heyting Algebra,

then it is a Heyting Algebra in a unique way:

$, , ∧, ∨, ⊃$ are well-defined.


% being a Heyting Algebra is a ``property'' of some DAGs,
% not ``extra structure''.

\bsk

{\bf Amazing fact:}

For any topological space $(X, \Opens(X))$,

the DAG $(\Opens(X), \subseteq)$ is a Heyting Algebra.



\newpage
% --------------------
% «calculating-VimpW»  (to ".calculating-VimpW")
% (s "Calculating $Vprotect⊃W$" "calculating-VimpW")
\myslide {Calculating $V\protect⊃W$} {calculating-VimpW}

What is $V⊃W$?

Idea: look at all $U$s such that $U\&V \vdash W$.

\bsk

%D diagram calculating-VimpW
%D 2Dx        100         +30
%D 2D  100 \arga∧V <--| \arga
%D 2D         |           |
%D 2D         |    <->    |
%D 2D         v           v
%D 2D  +30    W |------> V⊃W
%D 2D
%D (( \arga∧V \arga   W V⊃W
%D    @ 0 @ 1 <-| @ 0 @ 2 -> @ 1 @ 3 -> @ 2 @ 3 |->
%D    @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
{
\def\foo#1{\def\arga{#1}\diag{calculating-VimpW}}
$\foo{?}$

\bsk

$\foo{\emp} \quad
  \foo{W}    \quad
  \foo{U}
$
}

\bsk

In $\Opens(\bbV)$, this works for these open sets: $\dagKite01011$.

Define $V⊃W$ as the greatest of them.

More formally:

$V⊃W := \sup \sst{U}{U\&V \vdash W}$

$V⊃W := \bigcup\; \sst{U}{U\&V \vdash W}$

$V⊃W := \bigcup\; \sst{U}{U \cap V \subseteq W}$

$V⊃W := \bigcup\; \sst{A^\bol}{A^\bol \cap V \subseteq W}$

$V⊃W := \bigcup\; \sst{A^\bol}{A^\bol \subseteq W \cup (X \bsl V)}$

$V⊃W := (W \cup (X \bsl V))^\bol$


\newpage
% --------------------
% «curry-howard-1»  (to ".curry-howard-1")
% (s "``Mundo funcional'' e ``Mundo lógico'' (Curry-Howard)" "curry-howard-1")
\myslide {``Mundo funcional'' e ``Mundo lógico'' (Curry-Howard)} {curry-howard-1}

Compare a prova abaixo à esquerda, em Dedução Natural, de que $Q⊃R$
implica $P∧Q⊃P∧R$, com a construção do termo
$dA{×}B.\ang{d,f('d)}:(A{×}B \to A{×}C)$ em $$-cálculo simplesmente
tipado:

%:*&*\&*
%:*&**
%:*×*{×}*
%:*<*\langle *
%:*>*\rangle *
%:
%:     fB->C                 Q->R      
%:  =============(?)      ============(?)
%:  f^\#A×B->A×C         (P&Q)->(P&R)   
%:                                
%:  ^4-functional?        ^4-logical?   
%:  
%:           [P&Q]^1                    [dA×B]^1          
%:           -------                    ---------          
%:  [P&Q]^1     Q     Q⊃R   [dA×B]^1      'dB     fB->C 
%:  -------     ----------   ---------     ---------------- 
%:     P            R          dA           f('d)C      
%:     --------------          -----------------------      
%:         P&R                      <d,f('d)>A×C               
%:      ----------1          ------------------------------1
%:      (P&Q⊃P&R)              dA×B.<d,f('d)>:A×B->A×C
%:                                                         
%:      ^4-logical              ^4-functional                  
%:
$$\ded{4-logical} \qquad \ded{4-functional}$$

As duas têm exatamente a mesma estrutura. Isto é um exemplo do
Isomorfismo de Curry-Howard em funcionamento; ele diz que há uma
bijeção natural entre derivações em Dedução Natural e termos de
$$-cálculo simplesmente tipado. Repare que na árvore um $$-cálculo
os termos sempre crescem à medida que descemos; se usamos uma nova
notação --- ``downcased types'' --- podemos não só manter os termos
pequenos, como suprimir os tipos --- os tipos podem ser reconstruídos
``convertendo para maiúsculas'' os termos. Note que os ``conectivos''
também têm que ser convertidos: `,' convertido para maiúscula vira
`$×$', e `$\mto$' convertido para maiúscula vira `$\to$'.

%:           [a,b]^1             
%:           -------               a,b := d
%:   [a,b]^1    b     b|->c      b|->c := f
%:   -------    -----------  
%:       a           c               a :=  (a,b)     
%:       -------------               b := '(a,b)     
%:           a,c                     c := (b|->c)(b)  
%:         ---------               a,c := <a,c>       
%:         a,b|->a,c         a,b|->a,c := (a,b).(a,c)
%:
%:         ^4-DNC
%:
$$\cded{4-DNC} \qquad
  \begin{array}{rcl}
             a,b &:=& d \\
        b \mto c &:=& f \\
                        \\
               b &:=& '(a,b)       \\
               c &:=& (b \mto c)(b) \\
             a,c &:=& \ang{a,c}     \\
    a,b \mto a,c &:=& (a,b).(a,c)  \\
  \end{array}
$$

Agrora cada barra da árvore define um novo termo a partir de termos
anteriores; isto gera o dicionário à direita... e a semântica de cada
barra passa a ser: ``se eu sei o significado dos termos acima da
barra, eu sei o significado do termo abaixo da barra'', ou: ``se eu
sei `$a$' e sei `$c$' eu sei `$a,c$'\,'', ``se eu sei `$b$' e `$b \mto
c$' eu sei `$c$'\,'', etc.

Os ``termos'' em DNC funcionam de um modo bem diferente dos termos de
$$-cálculo. Em DNC nós permitimos nomes longos para variáveis (por
exemplo, `$a,b$'), a distinção sintática entre variáveis e termos
não-primitivos não existe, e, aliás, sem o dicionário não é nem
possível determinar só pelos nomes de dois termos qual é ``mais
primitivo'' que o outro: por exemplo, $b \mto c$ é mais primitivo que
$c$ mas $a,b \mto a,c$ é menos primitivo que $a,c$.




\newpage
% --------------------
% «preamble-dgs-and-topologies»  (to ".preamble-dgs-and-topologies")
% (s "Preamble: DGs and topologies" "preamble-dgs-and-topologies")
\myslide {Preamble: DGs and topologies} {preamble-dgs-and-topologies}

A {\sl directed graph} is a set of worlds, $W$,

and a relation $R \subseteq W×W$.

\msk

Important fact:

DGs induce topologies,

topologies induce DGs,

and in the finite case (which is what matters to us)

the correspondence $\DG \leftrightarrows \Top$ is especially
well-behaved.

\msk

This will be our archetypical DAG:
%
$$\bbV := (W, R) := (\sof{\aa,\bb,\cc}, \sof{\aa\to\cc, \bb\to\cc})$$
%
%D diagram Vee-dag
%D 2Dx     100 +15 +15
%D 2D  100 \aa     \bb
%D 2D
%D 2D  +20     \cc
%D 2D
%D (( \aa \cc -> \bb \cc -> ))
%D enddiagram
%D
$$\bbV \quad \equiv \diag{Vee-dag}$$

This will be the topological space induced by $\bbV$:
%
$$(\bbV, \Opens(\bbV)) :=
  (\sof{\aa,\bb,\cc},
   \sof{\emp,
        \sof{\cc},
        \sof{\aa,\cc},
        \sof{\bb,\cc},
        \sof{\aa,\bb,\cc}
   })
$$

We will use the correspondence mainly to represent

finite topological spaces by their associated DGs (or DAGs).


\newpage
% --------------------
% «preamble-dg-to-topology»  (to ".preamble-dg-to-topology")
% (s "Preamble: each DG induces a topology" "preamble-dg-to-topology")
\myslide {Preamble: each DG induces a topology} {preamble-dg-to-topology}

A function $f: W \to \sof{0,1}$ is ``{\sl non-decreasing} (on $R$)''

when all arrows in $R$ are ``non-decreasing''.

$$\bbV := (W, R) := (\sof{\aa,\bb,\cc}, \sof{\aa\to\cc, \bb\to\cc})$$

$$\bbV \quad \equiv \diag{Vee-dag}$$

$\Vee100$ decreases on the arrow $\aa\to\cc$: $f(\aa\to\cc) = 1 \to 0$.

$\Vee010$ decreases on $\bb\to\cc$.

$\Vee110$ decreases on both $\aa\to\cc$ and $\bb\to\cc$.

The non-decreasing functions $\bbV \to \sof{0,1}$ are
$\Vee000, \Vee001, \Vee011, \Vee101, \Vee111$.

A ``{\sl non-decreasing subset}'' $W' \subseteq W$ is one whose

characteristic function is non-decreasing (on $R$).

Definition:
%
$$\Nondecr(W,R) := \sst{W' \subseteq W}{\text{$W'$ is non-decreasing on $R$}}$$

For a DG $\bbD := (W,R)$ the induced topological space is:
%
$$(\bbD, \Opens(\bbD)) := (W, \Opens(\bbD)) := (W, \Nondecr(W, R))$$

For the dag $\V$ above, this is:
%
$$(\bbV, \Opens(\bbV)) :=
  (\sof{\aa,\bb,\cc},
   \sof{\emp,
        \sof{\cc},
        \sof{\aa,\cc},
        \sof{\bb,\cc},
        \sof{\aa,\bb,\cc}
   })
$$

Fact: topologies induced by DGs are closed by arbitrary intersections

of open sets --- not just by finite intersections.



\newpage
% --------------------
% «preamble-truth-values»  (to ".preamble-truth-values")
% (s "Preamble: truth-values" "preamble-truth-values")
\myslide {Preamble: truth-values} {preamble-truth-values}

Abuse of language:

We will often write subsets of $W$ (non-decreasing or not)

as if they were the corresponding functions $W \to \sof{0,1}$.

So, for example:

$\sof{\bb,\cc} \equiv \Vee011$,

$\Opens(\bbV) = \Nondecr(\bbV) \equiv \sof{\Vee000, \Vee001, \Vee011, \Vee101, \Vee111}$.

\bsk

Terminology:

A function $W \to \sof{0,1}$ is a ``{\sl modal truth-value}''.

A non-decreasing function $W \to \sof{0,1}$ is an ``{\sl
intuitionistic truth-value}''.

We will see later that the modal truth-values live in a category $\Set^W$

and that the intuitionistic truth-values live in a category $\Set^\bbD$.

\bsk
\bsk

{\bf Big fact:} we can interpret propositional logic on modal truth-values...

just operate on each world separately, e.g.: $\Vee011 \land \Vee101 = \Vee001$.

On modal truth-values the ``logic'' is boolean but not two-valued.

\msk

{\bf Bigger fact:} the intuitionistic truth-values on a DAG $\D$ form

a ``Heyting algebra'', $\O(\D)$ --- we can interpret propositional logic there,

but it will be {\sl intuitionistic} --- we can't prove $P⊃P$ there because

that is {\sl not always true}: take $P:=\Vee001$, then $P \equiv \Vee111$.

\msk

{\bf Mind-blowing fact:} the notion of ``taking the union of all open sets in

a given cover'' can be interpreted as a {\sl new logical operation}, obeying

some axioms: namely, $^* = $, $P^{**} = P^*$, $P^*∧Q^* = (P∧Q)^*$.

This ``taking the union...'' operation is a particular case of something much

more general: {\sl Lawvere-Tierney topologies}, that generalize both

{\bf sheaves} and {\bf forcing}.

\msk

We can understand \und{sheaves} through \und{logic}.

\bsk
\bsk



\fbox{
\begin{tabular}{l}
{\bf Tiny, but amazing, fact:} we can understand all these ideas \\
from the cases of the DAGs $\V \equiv \dagVee***$ and $\O(\V)^\op \equiv \dagKite*****$, \\
and then generalizing. This tiny \& amazing fact --- that in a sense \\
is trivial, and is little more than working out in full detail \\
a few chosen exercises from topos theory books --- \\
is the guiding thread for these notes. \\
\end{tabular}
}






\newpage
% --------------------
% «topological-spaces»  (to ".topological-spaces")
% (s "Topological spaces" "topological-spaces")
\myslide {Topological spaces} {topological-spaces}


A topological space is a pair $(X,\O(X))$

where $\O(X) \subset \Pts(X)$ is a topology on the set $X$:

(i) $X\O(X)$, $\emp\O(X)$,

(ii) $\O(X)$ is closed by arbitrary unions,

(iii) $\O(X)$ is closed by finite intersections.

\msk

Sometimes an $\OX$ is closed by {\bf arbitrary intersections}...

This happens for $(\V,\O(\V))$ and for $(\R,\Pts(\R))$, but not for $(\R,\O(\R))$.

When this happens we say that $\OX$ is an {\sl Alexandroff topology},

and that $(X,\OX)$ is an {\sl Alexandroff space}.

We will refer to these things by more mnemonic names:

$\OX$ is a ``topcai'', $(X,\OX)$ is a ``topcai space''.

\msk

There is an inclusion of categories - a functor:
%
$$\TopCAI \monicto \Top$$

and we can take a topology $\OX$ and look at the set of

arbitrary intersections of its open sets, $\Iinfty\OX$ -

it turns out that $\Iinfty\OX$ is closed by arbitrary unions,

and is a topology - actually a topcai.

\msk

This operation - ``closing by arbitrary intersections'' - is a functor:

$$\begin{array}{rccc}
  \cai: &   \Top  & \to  & \TopCAI \\
        & (X,\OX) & \mto & (X,\Iinfty\OX) \\
  \end{array}
$$

and there is an adjunction $(\monicto) \dashv \cai$.

\msk

($\TopCAI$ is a ``coreflective subcategory'' of $\Top$ -

the inclusion funtor $(\monicto)$ has a right adjoint).


\msk

Note that its counit on $(\R,\O(\R))$ is the

continuous map $\dquo{\id}: (\R,\Pts(\R)) \to (\R,\O(\R))$:



%D diagram counit-R
%D 2Dx     100      +50   +50      +50
%D 2D  100 a0 <---| a1    b0 <---| b1 
%D 2D       |       |      |       |  
%D 2D       |  <->  |      |  <->  |  
%D 2D       v       v      v       v  
%D 2D  +30 a2 |---> a3    b2 |---> b3 
%D 2D                                 
%D 2D  +20 a4 <===> a5    b4 <===> b5 
%D 2D
%D (( a0 .tex= (X,\OX)   a1 .tex= (X,\OX)
%D    a2 .tex= (Y,\O(Y)) a3 .tex= (Y,\Iinfty\O(Y))
%D    a4 .tex= \Top    a5 .tex= \TopCAI
%D    a0 a1 <-| a0 a2 -> a1 a3 -> a2 a3 |-> .plabel= b \cai
%D    a0 a3 harrownodes nil 20 nil <->
%D    a4 a5 <-< sl^ a4 a5 ->> sl_ .plabel= b \cai
%D ))
%D (( b0 .tex= (\R,\Pts(\R))   b1 .tex= (\R,\Pts(\R))
%D    b2 .tex= (\R,\O(\R))     b3 .tex= (\R,\Pts(\R))
%D    b4 .tex= \Top    b5 .tex= \TopCAI
%D    b0 b1 <-|
%D    b0 b2 -> .plabel= l \dquo{\id}
%D    b1 b3 -> .plabel= r \id
%D    b2 b3 |-> .plabel= b \cai
%D    b0 b3 harrownodes nil 20 nil <->
%D    b4 b5 <-< sl^ b4 b5 ->> sl_ .plabel= b \cai
%D ))
%D enddiagram
%D
$$\diag{counit-R}$$


\newpage
% --------------------
% «preorders-and-posets»  (to ".preorders-and-posets")
% (s "Preorders and partial orders" "preorders-and-posets")
\myslide {Preorders and partial orders} {preorders-and-posets}

A {\sl preorder} on $W$ is a relation $(\le) \subset W×W$ that is:

(i) reflexive: $a \le a$

(ii) transitive: if $a \le b$ and $b \le c$, then $a \le c$.

A {\sl partial order} is a preorder that is also:

(iii) anti-symmetric: if $a \le b$ and $b \le a$, then $a = b$.

\msk

A directed graph $(W,R)$ induces a preorder $(W,\le) := (W,R^*)$...

Mnemonic: the `$*$' is a Kleene star: if $a R a_1 R a_2 R a_3 R b$ then

$a R^4 b$, and thus $a R^* b$; ``$R^*$'' means ``at least zero `$R$'s''.

More formally: $R^* := R^0 \cup R^1 \cup R^2 \cup R^3 \cup \ldots$,

the reflexive/transitive closure of $R$.

($R^0$ is the diagonal --- $a R^0 b$ iff $a=b$).


\msk

Each cycle in a DG $(W,R)$ becomes a set of

``equivalent elements'' in the induced preorder

Let's consider just DAGs for a while.

DAGs induce partial orders --- aciclicity leads to antisymmetry.

\msk

A DG can be converted to a DAG by identifying the elements

in each cycle:



%D diagram collapsing-cycles
%D 2Dx     100 +10 +10 +10      +40
%D 2D  100 a <===> b         \{a,b\}
%D 2D       \                   |
%D 2D        v                  v
%D 2D  +20     c ----> d    \{c,d,e\}
%D 2D           ^     /         |
%D 2D            \   v          |
%D 2D  +20         e            |
%D 2D              |            |
%D 2D              v            v
%D 2D  +20         f          \{f\}
%D 2D
%D 2D                    q
%D 2D  +20        \DG -------> \DAG
%D (( a b -> sl^ a b <- sl_
%D    a c ->    c d -> d e -> e c ->    e f ->
%D ))
%D (( \{a,b\} \{c,d,e\} \{f\}
%D    @ 0 @ 1 -> @ 1 @ 2 ->
%D ))
%D (( \DG \DAG -> .plabel= a q
%D enddiagram
%D
$$\diag{collapsing-cycles}$$

\msk

It turns out that the inclusions $\DG^* \monicto \DG$ and $\DAG^* \monicto \DAG$ 

have left adjoints: in both cases, $* \dashv (\monicto)$,

and the units of the adjunctions take a DG or DAG $(W,R)$

to its reflexive and transitive closure.

\msk

Also, the inclusion $\DAG^* \monicto \DG^*$ have a left adjoint: `$q$'.


%D diagram DAG-DG-adjunctions
%D 2Dx     100   +15  +20  +15
%D 2D  100       \DG* <=> \DG
%D 2D           <=>       ->
%D 2D  +25 \DAG* <=> \DAG
%D 2D
%D (( \DG*  \DG   >-> sl_ \DG*  \DG  <- sl^ .plabel= a *
%D    \DAG* \DAG  >-> sl_ \DAG* \DAG <- sl^ .plabel= a *
%D    \DAG* \DG* >-> sl_ \DAG*  \DG* <- sl^ .plabel= l q
%D    \DAG  \DG   >->
%D ))
%D enddiagram
%D
$$\diag{DAG-DG-adjunctions}$$


\newpage
% --------------------
% «minimal-dag»  (to ".minimal-dag")
% (s "The minimal DAG for a topology" "minimal-dag")
\myslide {The minimal DAG for a topology} {minimal-dag}

Each DG $\D = (W,R)$ induces a topcai: $(W, \Nondecr(R))$ -

but several DGs induce the same topcai.

One canonical way to represent a topcai by a DG is to pick the

associated DG${}^*$ - it is the maximal DG generating that topcai.

\msk

For {\sl finite DAGs} - i.e., for finite $T_0$ topological spaces -

there is also a {\sl minimal} DAG generating that topology...

The process to obtain it is to drop all the arrows that are not

``essential''.

Here's an example:

(by the way: $\text{ess} \dashv {}^* \dashv (\monicot)$)
%
%D diagram dag-minimal
%D 2Dx     100 +15
%D 2D  100     a
%D 2D  +15 b
%D 2D  +15     c
%D 2D
%D (( a b -> b c ->
%D ))
%D enddiagram
%
%D diagram dag-medium
%D 2Dx     100 +15
%D 2D  100     a
%D 2D  +15 b
%D 2D  +15     c
%D 2D
%D (( a b -> b c ->
%D  # a loop (ur,dr)
%D    b loop (ul,dl)
%D    c loop (ur,dr)
%D ))
%D enddiagram
%
%D diagram dag-full
%D 2Dx     100 +15
%D 2D  100     a
%D 2D  +15 b
%D 2D  +15     c
%D 2D
%D (( a b -> b c -> a c ->
%D    a loop (ur,dr)
%D    b loop (ul,dl)
%D    c loop (ur,dr)
%D ))
%D enddiagram
%
%D diagram dags
%D 2Dx     100  +70
%D 2D  100 A    B
%D 2D
%D 2D  +60 C    D
%D 2D
%D 2D  +60 E    F
%D 2D
%D 2D  +40 \DAG \DAG*
%D 2D
%D (( A .tex= \usebox{\myboxa}
%D    B .tex= \usebox{\myboxc}
%D    C .tex= \usebox{\myboxb}
%D    D .tex= \usebox{\myboxc}
%D    E .tex= \usebox{\myboxc}
%D    F .tex= \usebox{\myboxc}
%D    A B <-| .plabel= a {ess}
%D    A C -> B D -> A D harrownodes nil 20 nil <->
%D    C D |-> .plabel= a *
%D    C E -> D F -> C F harrownodes nil 20 nil <->
%D    E F <-|
%D ))
%D (( \DAG \DAG*
%D    @ 0 @ 1  -> sl^^ .plabel= a {ess}
%D    @ 0 @ 1 <-       .plabel= m *
%D    @ 0 @ 1 >-> sl__
%D ))
%D enddiagram
%D
$$\savebox{\myboxa}{$\diag{dag-minimal}$}
  \savebox{\myboxb}{$\diag{dag-medium}$}
  \savebox{\myboxc}{$\diag{dag-full}$}
  \diag{dags}
$$

\msk

(The moral is that there is something canonical about

representing topologies ($T_0$, and on finite sets)

by DAGs with very few arrows)

\newpage
% --------------------
% «presheaves»  (to ".presheaves")
% (s "Presheaves" "presheaves")
\myslide {Presheaves} {presheaves}

A {\sl presheaf}  on $(X,\OX)$ is a

(contravariant) functor $\OX^\op \to \Set$.

A {\sl sheaf} is a presheaf obeying a

``glueing condition'', that we will see later.

Example: $\Cinfty: \Opens(\R)^\op \to \Set$. If $V \subset U$, then:
%
%D diagram presh-1
%D 2Dx         100              +35
%D 2D  100 \Cinfty(V) <--- \Cinfty(U)
%D 2D          ^        ^       ^
%D 2D          |        |       |
%D 2D          -        -       -
%D 2D  +25     V >------------> U
%D 2D
%D (( \Cinfty(V) \Cinfty(U) V  U
%D    @ 0 @ 1 <- .plabel= a _V^U
%D    @ 0 @ 2 <-| @ 1 @ 3 <-|  @ 0 @ 3 varrownodes nil 20 nil <-|
%D    @ 2 @ 3 >->
%D ))
%D enddiagram
%D
$$\diag{presh-1}$$

The map $_V^U := \Cinfty(V \monicto U)$ is called the

``restriction function''.

\msk

We will borrow some terminology from the case of functions

defined over open sets: for a presheaf $P: \OX^\op \to \Set$ and

$W \subseteq V \subseteq U$,
%
$$\begin{array}{rl}
  p_U \in P(U) & \text{a ``function/element with support $U$''} \\
  p_X \in P(X) & \text{a ``global function/element''} \\
  _V^U: P(U) \to P(V) & \text{``restriction function''} \\
  (_V^U := P(V \monicto U)) & \\
  \end{array}
$$

Functoriality means two conditions on restriction maps:

$P(U \monicto U) = \id_{P(U)}$

$P(W \monicto V)P(V \monicto U) = P(W \monicto U)$
%
%D diagram presh-2
%D 2Dx      100   +25    +25
%D 2D  100 P(W) <----- P(U)
%D 2D          <-    <-
%D 2D  +20       P(V)
%D 2D
%D 2D  +15  W >--------> U
%D 2D         >->   >->
%D 2D  +20        V
%D 2D
%D (( P(W) P(V) P(U)
%D      W    V    U
%D    @ 0 @ 1 <-  @ 1 @ 2 <-  @ 0 @ 2 <-
%D    @ 3 @ 4 >-> @ 4 @ 5 >-> @ 3 @ 5 >->
%D    @ 0 @ 3 <-| @ 1 @ 4 <-| @ 2 @ 5 <-|
%D ))
%D enddiagram
%D
$$\diag{presh-2}$$


\newpage
% --------------------
% «subtopology-of-R»  (to ".subtopology-of-R")
% (s "A subtopology of $\R$" "subtopology-of-R")
\myslide {A subtopology of $\protect\R$} {subtopology-of-R}

The topology on the DAG $\bbV$ can be seen as a subtopology of $\R$...

Consider the quotient $q$ below, or, equivalently, $q'$:

$$\begin{array}{l}
  q:  \R \to \{(-,0], \, (0,1), \, [1,)\} \\
  q': \R \to \{\aa, \cc, \bb\}
  \end{array}
$$

${q'}^{-1}(\Pts(\{\aa, \cc, \bb\})) \;\subset\; \Pts(\R)$ is a topology on $\R$ with 8 open sets.

${q'}^{-1}(\Pts(\{\aa, \cc, \bb\}))  \OR \;\subset\; \OR \;\subset\; \Pts(\R)$

is a topology on $\R$ with 5 open sets.

Compare:
%
%D diagram UVW-and-R-1
%D 2Dx     100 +12 +12   +20 +12 +12 +30 +12 +12 +27 +12 +12  
%D 2D  100                   X           X'    	              
%D 2D                      /   \       /   \   	              
%D 2D  +20 \aa     \bb   U       V   U'      V'	\aa'    \bb'  
%D 2D         \   /        \   /       \   /   	   \   /      
%D 2D  +20     \cc           W           W'    	    \cc'      
%D 2D                        |           |     	              
%D 2D  +20                 \emp        \emp{}  	              
%D 2D
%D ((        X .tex= \{\aa,\bb,\cc\}          
%D    U .tex= \{\aa,\cc\}    V .tex= \{\bb,\cc\}
%D                 W .tex= \{\cc\}
%D                 \emp           
%D    @ 0 @ 1 <- @ 0 @ 2 <-
%D    @ 1 @ 3 <- @ 2 @ 3 <-
%D    @ 3 @ 4 <-
%D ))
%D ((         X' .tex= (-,)
%D    U' .tex= (-,1)    V' .tex= (0,)
%D            W' .tex= (0,1)   
%D                \emp{}          
%D    @ 0 @ 1 <- @ 0 @ 2 <-
%D    @ 1 @ 3 <- @ 2 @ 3 <-
%D    @ 3 @ 4 <-
%D ))
%D (( \aa  \cc  -> \bb  \cc  ->
%D ))
%D (( \aa' .tex= (-,0] \bb' .tex= [1,) \cc' .tex= (0,1)
%D    \aa' \cc' -> \bb' \cc' ->
%D ))
%D enddiagram
%D
$$\diag{UVW-and-R-1}$$

We will refer to these open sets as $X$, $U$, $V$, $W$, $\emp$:

%D diagram XUVW-and-bits
%D 2Dx     100        +15     +15        +30 +15 +15  
%D 2D  100        \dagVee111                 X
%D 2D
%D 2D  +20 \dagVee101   \dagVee011       U       V 
%D 2D
%D 2D  +20        \dagVee001                 W
%D 2D
%D 2D  +20        \dagVee000                \emp
%D 2D
%D 2D  +20
%D 2D
%D ((        \dagVee111           
%D    \dagVee101   \dagVee011   
%D           \dagVee001           
%D           \dagVee000           
%D    @ 0 @ 1 <- @ 0 @ 2 <-
%D    @ 1 @ 3 <- @ 2 @ 3 <-
%D    @ 3 @ 4 <-
%D ))
%D ((      X U V W \emp
%D    @ 0 @ 1 <- @ 0 @ 2 <-
%D    @ 1 @ 3 <- @ 2 @ 3 <-
%D    @ 3 @ 4 <-
%D ))
%D enddiagram
%D
$$\diag{XUVW-and-bits}$$

Note that $U$ will sometimes mean a specific open set - $\dagVee101$ -,

sometimes an arbitrary open set; same for the other letters.


\newpage
% --------------------
% «coherent-families»  (to ".coherent-families")
% (s "Coherent families" "coherent-families")
\myslide {Coherent families} {coherent-families}

Now let $X := \R$, and let's consider two

functions defined on subsets of $X$:

$\begin{array}{rrcl}
  x_U: & U & \to  & \R \\
       & x & \mto & x  \\
  0_U: & U & \to  & \R \\
       & x & \mto & 0  \\
  \end{array}
$

(I.e., we're defining $x_X, x_U, x_V, x_W, x_\emp$,

$0_X, 0_U, 0_V, 0_W, 0_\emp$).

\msk

We can also consider families of functions,

whose supports are families of open sets -

$\{x_U, x_V\}$ and $\{x_U, 0_V\}$ are families with support $\{U,
V\}$.

Note: $\{x_U, x_V, 0_V\}$ is {\sl not} a family with support $\{U, V\}$

because $V$ has two ``images'': $x_V$ and $0_V$.

\bsk

A function defined on $U$ - say, $x_U$ -

induces a family $\{x_U\}$ defined on $\{U\}$, i.e., on $\dagKite01000$ -

and another family, $\{x_U, x_W, x_\emp,\}$,

defined on all open sets under $U$ -

i.e., on the saturation of $\{U\} = \dagKite01000$, which is
$\dagKite01011$.

\bsk

When we try to extend the family $\{x_U, 0_V\}$

to the saturation of $\dagKite01100$, i.e., to $\dagKite01111$,

we see that we get two different candidates for $W$ -

$x_W \neq 0_W$ - which is not good...

\msk

A family is said to be {\sl coherent} when its extension

to the saturation of its support is well-defined.

$\{x_U, x_V\}$ is coherent, $\{x_U, 0_V\}$ is not.

Here's a way to define formally coherence for families:

a family $a_\U$ is coherent iff $a_U, a_V  a_\U \; a_U|_{UV} =
a_V|_{UV}$.

Note that $\{x_U, 0_V, 0_W\}$ is not coherent.



\newpage
% --------------------
% «saturation»  (to ".saturation")
% (s "Saturation and bisaturation" "saturation")
\myslide {Saturation and bisaturation} {saturation}

Notation: the calligraphic letters $\calU, \calV, \calW$

will denote families of open sets, and the annotations

`${}^\bol$', `${}^\bul$', `${}^\dbul$' will indicate how saturated a
family is -

$\calU^\bol$: not necessarily saturated

$\calU^\bul$: saturated

$\calU^\dbul$: bisaturated

We will sometimes use $\bul$, $\dbul$ to denote {\sl operations}:

$\bul$ is ``saturate'', $\dbul$ is ``bisaturate''.



\newpage
% --------------------
% «a-presheaf-on-a-dag»  (to ".a-presheaf-on-a-dag")
% (s "A (bad) presheaf on a DAG" "a-presheaf-on-a-dag")
\myslide {A (bad) presheaf on a DAG} {a-presheaf-on-a-dag}

%D diagram UVW-and-R
%D 2Dx     100 +15 +15  +30 +15 +15  
%D 2D  100     X            X'     
%D 2D        /   \        /   \   
%D 2D  +20 U       V    U'      V'  
%D 2D        \   /        \   /   
%D 2D  +20     W            W'      
%D 2D          |            |      
%D 2D  +20   \emp         \emp{}
%D 2D
%D 2D  +20
%D 2D
%D ((    X           
%D    U     V   
%D       W
%D      \emp           
%D    @ 0 @ 1 <- @ 0 @ 2 <-
%D    @ 1 @ 3 <- @ 2 @ 3 <-
%D    @ 3 @ 4 <-
%D ))
%D ((      X' .tex= (-,)
%D    U' .tex= (-,1)    V' .tex= (0,)
%D         W' .tex= (0,1)   
%D              \emp{}          
%D    @ 0 @ 1 <- @ 0 @ 2 <-
%D    @ 1 @ 3 <- @ 2 @ 3 <-
%D    @ 3 @ 4 <-
%D ))
%D enddiagram
%D
$$\diag{UVW-and-R}$$

Here is a presheaf over $(X,\Opens(X))$ (``$P$'') that is

not a sheaf - it violates the two sheaf conditions.

$P$ is not collated - because

$\{p_U, p_{V'}\}$ is a coherent family (on $\{U,V\}$)

that cannot be collated to a global function.

$P$ is not separated - because

there are two different collations for $\{p_U, p_V\}$.

% (find-dn4file "dednat41.lua" "forths[\".PLABEL=\"] =")
% (find-dn4file "dednat41.lua" "storenode =")

%L thereplusxy = function (dx, dy, tag)
%L     ds[1] = storenode({x = ds[1].x + dx, y = ds[1].y + dy, tag = tag})
%L     return ds[1]
%L   end
%L forths["there+xy:"] = function ()
%L     thereplusxy(getword(), getword(), getword())
%L   end

\def\ph#1{\phantom{O}}
\def\ph#1{#1}
\def\ph#1{O}
\def\ph#1{{\color{red}#1}}
\def\ph#1{\phantom{#1}}

%D diagram bad-presheaf
%D 2Dx     100 +15 +15  +30 +15  +15  
%D 2D  100     X            X'     
%D 2D        /   \        /   \    
%D 2D  +20 U       V    U'      V'  
%D 2D        \   /        \   /    
%D 2D  +20     W            W'      
%D 2D          |            |      
%D 2D  +20   \emp         \emp{}
%D 2D
%D ((         X .tex= P(X)          
%D    U .tex= P(U)    V .tex= P(V)  
%D            W .tex= P(W)
%D         \emp .tex= P(\emp)          
%D    @ 0 @ 1 -> @ 0 @ 2 ->
%D    @ 1 @ 3 -> @ 2 @ 3 ->
%D    @ 3 @ 4 ->
%D ))
%D (( X' there+xy: -6 0 X'L .tex= \ph{p_X}
%D    X' there+xy:  6 0 X'R .tex= \ph{p'_X}
%D    V' there+xy: -6 0 V'L .tex= \ph{p_V}
%D    V' there+xy:  6 0 V'R .tex= \ph{p'_V}
%D ))
%D ((          X' .tex= \{p_X,p'_X\}
%D    U' .tex= \{p_U\}   V' .tex= \{p_V,p'_V\}
%D             W' .tex= \{p_W\}
%D         \emp{} .tex= \{p_\emp\}       
%D    # @ 0 @ 1 -> @ 0 @ 2 ->
%D    # @ 1 @ 3 -> @ 2 @ 3 ->
%D    # @ 3 @ 4 ->
%D                         X' place
%D    X'L U' -> X'R U' ->           X'L V'L -> X'R V'L ->
%D                                    V' place
%D                U' W' ->         V'L W' -> V'R W' ->
%D                       W' \emp{} ->
%D ))
%D enddiagram
%D
$$\diag{bad-presheaf}$$



\newpage
% --------------------
% «presheaf-on-a-dag-germs»  (to ".presheaf-on-a-dag-germs")
% (s "A presheaf on a DAG: its space of germs" "presheaf-on-a-dag-germs")
\myslide {A presheaf on a DAG: its space of germs} {presheaf-on-a-dag-germs}

Its space of germs is built like this:

for each point in $X$ - i.e., for $\aa, \bb, \gg$; let's look

at $\aa$ - look at all open sets containing $\aa$ (namely:

$U=\{\aa,\cc\}, X=\{\aa,\bb,\cc\}$) and take the colimit of $P$

on these open sets as they get smaller and smaller.

As there is a smallest open set containing $\aa$ - and $\bb$,

and $\cc$ - these colimits/germs are very easy to calculate:


%D diagram bad-presheaf-germs
%D 2Dx     100 +15 +15  +30 +15  +15  
%D 2D  100 \aa     \bb  \aa'     \bb'  
%D 2D         \   /        \    /  
%D 2D  +20     \cc          \cc'      
%D 2D
%D (( \aa \cc -> \bb \cc ->
%D ))
%D (( \bb' there+xy: -6 0 \bb'L .tex= \ph{p_\bb}
%D    \bb' there+xy:  6 0 \bb'R .tex= \ph{p'_\bb}
%D ))
%D (( \aa' .tex= \{p_\aa\}
%D    \bb' .tex= \{p_\bb,p'_\bb\}
%D    \cc' .tex= \{p_\cc\}
%D    \aa' \cc' ->
%D    \bb' place   \bb'L \cc' -> \bb'R \cc' ->
%D ))
%D enddiagram
%D
$$\begin{matrix}
  p_\aa  := p_U  \\
  p_\bb  := p_V  \\
  p'_\bb := p'_V \\
  p_\cc  := p_W  \\
  \end{matrix}
  \qquad
  \cdiag{bad-presheaf-germs}
$$

\msk

The projection map $E \to X$ is the obvious one.

We need to put a topology to $E$; it turns out (why?) that the

right topology is the one induced by the obvious graph.

Now this induces a sheaf of sections...

{\bf (I am skipping some steps -)}

%D diagram bad-presheaf-sheaf
%D 2Dx     100 +15 +15  +30 +15  +15  
%D 2D  100     X            X'     
%D 2D        /   \        /   \    
%D 2D  +20 U       V    U'      V'  
%D 2D        \   /        \   /    
%D 2D  +20     W            W'      
%D 2D          |            |      
%D 2D  +20   \emp         \emp{}
%D 2D
%D 2D  +20
%D 2D
%D ((         X .tex= S(X)          
%D    U .tex= S(U)    V .tex= S(V)  
%D            W .tex= S(W)
%D         \emp .tex= S(\emp)          
%D    @ 0 @ 1 -> @ 0 @ 2 ->
%D    @ 1 @ 3 -> @ 2 @ 3 ->
%D    @ 3 @ 4 ->
%D ))
%D (( X' there+xy: -5 0 X'L .tex= \ph{s_X}
%D    X' there+xy:  5 0 X'R .tex= \ph{s'_X}
%D    V' there+xy: -5 0 V'L .tex= \ph{s_V}
%D    V' there+xy:  5 0 V'R .tex= \ph{s'_V}
%D ))
%D ((          X' .tex= \{s_X,s'_X\}
%D    U' .tex= \{s_U\}   V' .tex= \{s_V,s'_V\}
%D             W' .tex= \{s_W\}
%D         \emp{} .tex= \{s_\emp\}       
%D    # @ 0 @ 1 -> @ 0 @ 2 ->
%D    # @ 1 @ 3 -> @ 2 @ 3 ->
%D    # @ 3 @ 4 ->
%D                         X' place
%D    X'L U' -> X'R U' ->           X'L V'L -> X'R V'R ->
%D                                    V' place
%D                U' W' ->         V'L W' -> V'R W' ->
%D                       W' \emp{} ->
%D ))
%D enddiagram
%D
$$\diag{bad-presheaf-sheaf}$$




\newpage
% --------------------
% «denses-and-stables»  (to ".denses-and-stables")
% (s "Dense and stable truth-values" "denses-and-stables")
\myslide {Dense and stable truth-values} {denses-and-stables}

At the left below we see the representation as a presheaf

of the ``$\dbul$-stable truth-values'', $\sst{Ï}{Ï^\dbul=Ï} \subset $;

It is a sheaf, and it can be recovered from its ``global elements''.

\msk

%D diagram denses-and-stables
%D 2Dx     100 +25 +25  +40 +25  +25  
%D 2D  100     X            X'     
%D 2D        /   \        /   \    
%D 2D  +30 U       V    U'      V'  
%D 2D        \   /        \   /    
%D 2D  +30     W            W'      
%D 2D          |            |      
%D 2D  +30   \emp         \emp{}
%D 2D
%D ((         X .tex= \sof{\k00001,\k00011,\k00111,\k01011,\k11111}
%D    U .tex= \sof{\k001,\k011,\k111}   V .tex= \sof{\k001,\k011,\k111}
%D            W .tex= \sof{\k01,\k11}
%D         \emp .tex= \sof{\k1})          
%D    @ 0 @ 1 -> @ 0 @ 2 ->
%D    @ 1 @ 3 -> @ 2 @ 3 ->
%D    @ 3 @ 4 ->
%D ))
%D ((         X' .tex= \sof{\k01111,\k11111}
%D    U' .tex= \sof{\k111}   V' .tex= \sof{\k111}
%D            W' .tex= \sof{\k11}
%D         \emp{} .tex= \sof{\k0,\k1}
%D    @ 0 @ 1 -> @ 0 @ 2 ->
%D    @ 1 @ 3 -> @ 2 @ 3 ->
%D    @ 3 @ 4 ->
%D ))
%D enddiagram
%D
$$\def\k{\dagKite}
  \diag{denses-and-stables}
$$

\msk

At the right above we see the representation as a presheaf

of the ``$\dbul$-dense truth-values'', $_\dbul := \sst{Ï}{Ï^\dbul=} \subset $.

It is not a sheaf, it can't be recovered from its ``global elements''

as $\sst{Ï}{Ï^\dbul=Ï}$ can; yet - and I have to admit that I found that

{\sl very} surprising - we can recover the modality from

the subobject $_\dbul \monicto $, by:

$Ï^\dbul := Ï  _\dbul$



% \end{document}


\newpage
% --------------------
% «subst-for-iff»  (to ".subst-for-iff")
% (s "Substitution principles for `$\Bij$'" "subst-for-iff")
\myslide {Substitution principles for `$\Bij$'} {subst-for-iff}

We will also use the following ``substitution principles'':

if $P$, $Q$, $Q'$, $R$, $R'$ are formulas, and $R'$ is obtained from $R$

by replacing some occurrences of $Q$ in it by $Q'$, then

%:  P|-Q<=>Q'           P|-Q<=>Q'  P|-R
%:  =========           ===============
%:  P|-R<=>R'    and        P|-R'
%:
%:  ^<=>-subst-1            ^<=>-subst-2
%:
$$\ded{<=>-subst-1} \qquad \ded{<=>-subst-2}$$

\msk

The ``theorems'' above - and the ones in the following slides -

can be proved using just the sequent calculus rules for intuitionistic

propositional logic augmented with the three axioms for `${}^*$'.

\msk

To make the proofs more manageable we will often make use of the

``\,`$\Bij$' trick'': starting from $P \vdash Q \Bij Q'$ and a proof of $P \vdash R$

we can produce a proof of $P \vdash R'$, where $R'$ is $R$

with some occurrences of `$Q$' replaced by `$Q'$'s.

\msk

Example:

(...)

To prove these first theorems ---

and the ones in the next slides ---

we will need some facts about the

biconditional, `$\Bij$', that is defined as:
%
$$P \Bij Q := (P⊃Q)∧(Q⊃P)$$




\newpage
% --------------------
% «LT-modalities»  (to ".LT-modalities")
% (s "Lawvere-Tierney Modalities" "LT-modalities")
\myslide {Lawvere-Tierney Modalities} {LT-modalities}

A {\sl (Lawvere-Tierney) modality} is an operation `${}^*$' on

intuitionistic truth-values obeing the following three axioms:
%:
%:                 P|-Q         
%:   ----         ------        -------
%:   |-*         P*|-Q*        P**|-P*
%:
%:   ^ax*-1       ^ax*-2        ^ax*-3
%:
$$\ded{ax*-1} \qquad \ded{ax*-2} \qquad \ded{ax*-3}$$

The supersaturation operation, $P^* := P^\dbul$, is an example of an

LT-modality --- but there are others:

\msk

$P^* := P^{} := P$

$P^* := P^{(\aa∨)} := \aa ∨ P$

$P^* := P^{(\bb⊃)} := \bb ⊃ P$

\msk

First theorems:

\ssk

$P \vdash P^*$

\ssk

$(P∧Q)^* \vdash P^*∧Q^*$

\ssk

$P∧Q^* \vdash (P∧Q)^*$

$P^*∧Q^* \vdash (P∧Q)^*$

\msk

From what we already have,

we can prove that $P \Bij Q$ implies

$P^* \Bij Q^*$ in a weak sense:
%:
%:  |-P<=>Q   |-P<=>Q
%:  -------   -------
%:   |-P⊃Q     |-Q⊃P
%:   -----     -----
%:   P|-Q      Q|-P
%:  ------    ------
%:  P*|-Q*    Q*|-P*
%:  -------   -------
%:  |-P*⊃Q*   |-Q*⊃P*
%:  -----------------
%:      |-P*<=>Q*
%:
%:      ^P<=>Q|-P*<=>Q*-weak
%:
$$\ded{P<=>Q|-P*<=>Q*-weak}$$

But there isn't much that we can do when $P \Bij Q$ is weaker than $$...

For example, if $P:=\dagVee011$ and $Q:=\dagVee101$, then $P \Bij Q=\dagVee001$.

\msk

We will treat this as an axiom:
%:
%:  --------------
%:  P<=>Q|-P*<=>Q*
%:
%:  ^antisymmetry-star
%:
$$\ded{antisymmetry-star}$$

(Actually this is true for any unary operation

on truth-values of a Heyting algebra).



\newpage
% --------------------
% «LT-modalities-and»  (to ".LT-modalities-and")
% (s "LT-modalities and `and'" "LT-modalities-and")
\myslide {LT-modalities and `and'} {LT-modalities-and}

Theorems:

\ssk

$P \vdash P^*$

\ssk

$(P∧Q)^* \vdash P^*∧Q^*$

\ssk

$P∧Q^* \vdash (P∧Q)^*$

$P^*∧Q^* \vdash (P∧Q)^*$

\msk

Proofs:

%:                --------
%:                P|-<=>P
%:  --------     ----------
%:  |-<=>*     P|-*<=>P*
%:  -----------------------
%:     P|-<=>P*
%:     ---------
%:       P|-P*
%:
%:       ^and*-1
%:
%:                              ------------ 
%:			        P|-Q<=>(P∧Q) 
%:    ------       ------      ==============
%:    P∧Q|-P       P∧Q|-Q      P|-Q*<=>(P∧Q)*
%:  ----------	 ----------    --------------
%:  (P∧Q)*|-P*	 (P∧Q)*|-Q*     P|-Q*⊃(P∧Q)* 
%:  -----------------------     ------------ 
%:       (P∧Q)*|-P*∧Q*	        P∧Q*|-(P∧Q)*
%:
%:       ^and*-2                ^and*-3
%:
%:                     ============
%:                     P*∧Q|-(P∧Q)*
%:  ==============   ----------------   ---------------
%:  P*∧Q*|-(P*∧Q)*   (P*∧Q)*|-(P∧Q)**   (P∧Q)**|-(P∧Q)*
%:  ---------------------------------------------------
%:                    P*∧Q*|-(P∧Q)*
%:   
%:                    ^and*-4
%:
$$\ded{and*-1}$$
$$\ded{and*-2} \qquad \ded{and*-3}$$
$$\ded{and*-4}$$

\msk

The cube of modalities for `$∧$' has only four different

truth-values (the case $P^* := P^{}$, $P = \dagVee011$, $Q = \dagVee101$

shows that they are all distinct):
%
%D diagram and-cube
%D 2Dx      100 +20    +25  +20	       +40 +20     +25  +20	 
%D 2D  100  P∧Q        P∧Q*	       P∧Q'        P∧Q*'	 
%D 2D  +20     (P∧Q)*     (P∧Q*)*         (P∧Q)*'     (P∧Q*)*'
%D 2D      			      			 
%D 2D  +20 P*∧Q       P*∧Q*	      P*∧Q'       P*∧Q*'	 
%D 2D  +20    (P*∧Q)*    (P*∧Q*)*        (P*∧Q)*'    (P*∧Q*)*'
%D 2D
%D ((  P∧Q    P*∧Q    P∧Q*    P*∧Q*
%D    (P∧Q)* (P*∧Q)* (P∧Q*)* (P*∧Q*)*
%D    @ 0 @ 1  -> @ 0 @ 2  -> @ 1 @ 3  -> @ 2 @ 3  ->
%D    @ 4 @ 5  =  @ 4 @ 6  =  @ 5 @ 7  =  @ 6 @ 7  = 
%D    @ 0 @ 4  -> @ 1 @ 5  -> @ 2 @ 6  -> @ 3 @ 7  = 
%D ))
%D ((  P∧Q'    P*∧Q'    P∧Q*'    P*∧Q*'
%D    (P∧Q)*' (P*∧Q)*' (P∧Q*)*' (P*∧Q*)*'
%D    @ 0 .tex= \dagVee001 @ 1 .tex= \dagVee101
%D    @ 2 .tex= \dagVee011 @ 3 .tex= \dagVee111
%D    @ 4 .tex= \dagVee111 @ 5 .tex= \dagVee111
%D    @ 6 .tex= \dagVee111 @ 7 .tex= \dagVee111
%D    @ 0 @ 1  -> @ 0 @ 2  -> @ 1 @ 3  -> @ 2 @ 3  ->
%D    @ 4 @ 5  =  @ 4 @ 6  =  @ 5 @ 7  =  @ 6 @ 7  = 
%D    @ 0 @ 4  -> @ 1 @ 5  -> @ 2 @ 6  -> @ 3 @ 7  = 
%D ))
%D enddiagram
%D
$$\diag{and-cube}$$



\newpage
% --------------------
% «LT-modalities-or»  (to ".LT-modalities-or")
% (s "LT-modalities and `or'" "LT-modalities-or")
\myslide {LT-modalities and `or'} {LT-modalities-or}

Theorems:

\msk

%:  
%:    ------       ------          -------------
%:    P|-P∨Q       Q|-P∨Q          P*∨Q*|-(P∨Q)*
%:  ----------   ----------      -----------------
%:  P*|-(P∨Q)*   Q*|-(P∨Q)*      (P*∨Q*)*|-(P∨Q)**
%:  -----------------------      -----------------
%:       P*∨Q*|-(P∨Q)*            (P*∨Q*)*|-(P∨Q)*
%:
%:       ^or*-1                   ^or*-2
%:
$$\ded{or*-1} \qquad \ded{or*-2}$$

\msk

The cube of modalities for `$∨$' has only five different

truth-values (the case $P^* := P^{}$,
$P = \dagHouse00001$, $Q = \dagHouse00010$

shows that they are all distinct):
%
%D diagram or-cube
%D 2Dx      100 +20    +25  +20	       +40 +20     +25  +20	 
%D 2D  100  P∨Q        P∨Q*	       P∨Q'        P∨Q*'	 
%D 2D  +20     (P∨Q)*     (P∨Q*)*         (P∨Q)*'     (P∨Q*)*'
%D 2D      			      			 
%D 2D  +20 P*∨Q       P*∨Q*	      P*∨Q'       P*∨Q*'	 
%D 2D  +20    (P*∨Q)*    (P*∨Q*)*        (P*∨Q)*'    (P*∨Q*)*'
%D 2D
%D ((  P∨Q    P*∨Q    P∨Q*    P*∨Q*
%D    (P∨Q)* (P*∨Q)* (P∨Q*)* (P*∨Q*)*
%D    @ 0 @ 1  -> @ 0 @ 2  -> @ 1 @ 3  -> @ 2 @ 3  ->
%D    @ 4 @ 5  =  @ 4 @ 6  =  @ 5 @ 7  =  @ 6 @ 7  = 
%D    @ 0 @ 4  -> @ 1 @ 5  -> @ 2 @ 6  -> @ 3 @ 7  ->
%D ))
%D ((  P∨Q'    P*∨Q'    P∨Q*'    P*∨Q*'
%D    (P∨Q)*' (P*∨Q)*' (P∨Q*)*' (P*∨Q*)*'
%D    @ 0 .tex= \dagHouse00011 @ 1 .tex= \dagHouse00111
%D    @ 2 .tex= \dagHouse01011 @ 3 .tex= \dagHouse01111
%D    @ 4 .tex= \dagHouse11111 @ 5 .tex= \dagHouse11111
%D    @ 6 .tex= \dagHouse11111 @ 7 .tex= \dagHouse11111
%D    @ 0 @ 1  -> @ 0 @ 2  -> @ 1 @ 3  -> @ 2 @ 3  ->
%D    @ 4 @ 5  =  @ 4 @ 6  =  @ 5 @ 7  =  @ 6 @ 7  = 
%D    @ 0 @ 4  -> @ 1 @ 5  -> @ 2 @ 6  -> @ 3 @ 7  ->
%D ))
%D enddiagram
%D
$$\diag{or-cube}$$

% Here's the tableau that shows that the implication
%   (P*⊃Q)*⊃(P⊃Q)*
% can't be strict when P*:=A∨P - i.e., it describes the
% intuitionistic countermodels for (A∨(P⊃Q))⊃(A∨((A∨P)⊃Q)).
%
%   (A∨(P⊃Q))⊃(A∨((A∨P)⊃Q))
%            0               a
%     1       00      0    b<-a
%    1∨  1                   b
%       01                 c<-b
%                   1  0   d<-b
%                  1∨1       d
%
% b<-a.(A1b ∨ (c<-b.  P0c∨Q1c)) ∧
%       (A0b ∧ (d<-b. (A1d∨P1d)∧Q0d))
%
% b<-a.       (c<-b.  P0c∨Q1c) ∧
%       (A0b ∧ (d<-b. (A1d∨P1d)∧Q0d))
%
% b<-a.       (c<-b.      P0c) ∧
%       (A0b ∧ (d<-b. (A1d∨P1d)∧Q0d))
%
% b<-a. P0b ∧
%        A0b ∧ (d<-b. A1d∧Q0d)



\newpage
% --------------------
% «LT-modalities-imp»  (to ".LT-modalities-imp")
% (s "LT-modalities and implication" "LT-modalities-imp")
\myslide {LT-modalities and implication} {LT-modalities-imp}

Theorems:

%:
%:  ----------
%:  (P⊃Q)∧P|-Q
%:  --------------
%:  ((P⊃Q)∧P)*|-Q*
%:  --------------    -----------   ------------- 
%:  (P⊃Q)*∧P*|-Q*     P⊃Q|-(P⊃Q)*   (P⊃Q)*|-P*⊃Q* 
%:  -------------     ---------------------------  
%:  (P⊃Q)*|-P*⊃Q*            P⊃Q|-P*⊃Q*           
%:                                                
%:  ^imp*-1                  ^imp*-2              
%:
%:                     ---------------   -------     
%:                     P*∧(P⊃Q*)*|-Q**   Q**|-Q* 
%:  -------------      ------------------------- 
%:  (P⊃Q)*|-P*⊃Q*           P*∧(P⊃Q*)*|-Q*       
%:  -------------           --------------       
%:  P*∧(P⊃Q)*|-Q*           (P⊃Q*)*|-P*⊃Q*       
%:                    
%:  ^imp*-3                 ^imp*-4
%:
$$\ded{imp*-1} \qquad \ded{imp*-2}$$
$$\ded{imp*-3} \qquad \ded{imp*-4}$$

\msk

The cube of modalities for `$⊃$' has only five different truth-values.

The case $P^* := \dagSqr0011 ∨ P$, $P = \dagSqr0010$, $Q = \dagSqr0000$
distinguishes them all:
%
%D diagram imp-cube-Aor
%D 2Dx      100 +20    +25  +20	       +40 +20     +25  +20	 
%D 2D  100  P⊃Q        P⊃Q*	       P⊃Q'        P⊃Q*'	 
%D 2D  +20     (P⊃Q)*     (P⊃Q*)*         (P⊃Q)*'     (P⊃Q*)*'
%D 2D      			      			 
%D 2D  +20 P*⊃Q       P*⊃Q*	      P*⊃Q'       P*⊃Q*'	 
%D 2D  +20    (P*⊃Q)*    (P*⊃Q*)*        (P*⊃Q)*'    (P*⊃Q*)*'
%D 2D
%D ((  P⊃Q    P*⊃Q    P⊃Q*    P*⊃Q*
%D    (P⊃Q)* (P*⊃Q)* (P⊃Q*)* (P*⊃Q*)*
%D    @ 0 @ 1 <-  @ 0 @ 2  -> @ 1 @ 3  -> @ 2 @ 3  =
%D    @ 4 @ 5 <-  @ 4 @ 6  -> @ 5 @ 7  -> @ 6 @ 7  =
%D    @ 0 @ 4  -> @ 1 @ 5  -> @ 2 @ 6  =  @ 3 @ 7  =
%D ))
%D ((  P⊃Q'    P*⊃Q'    P⊃Q*'    P*⊃Q*'
%D    (P⊃Q)*' (P*⊃Q)*' (P⊃Q*)*' (P*⊃Q*)*'
%D    @ 0 .tex= \dagSqr0101 @ 1 .tex= \dagSqr0000
%D    @ 2 .tex= \dagSqr1111 @ 3 .tex= \dagSqr1111
%D    @ 4 .tex= \dagSqr0111 @ 5 .tex= \dagSqr0011
%D    @ 6 .tex= \dagSqr1111 @ 7 .tex= \dagSqr1111
%D    @ 0 @ 1 <-  @ 0 @ 2  -> @ 1 @ 3  -> @ 2 @ 3  =
%D    @ 4 @ 5 <-  @ 4 @ 6  -> @ 5 @ 7  -> @ 6 @ 7  =
%D    @ 0 @ 4  -> @ 1 @ 5  -> @ 2 @ 6  =  @ 3 @ 7  =
%D ))
%D enddiagram
%D
$$\diag{imp-cube-Aor}$$

When the modality is $P^* := P$ we can't distinguish the four

truth-values in the front face of the cube (the `$(P^?⊃Q^?)^*$'s)...

The best that we can do is this. For $P^* := P$, $P = \dagHouse00001$, $Q = \dagHouse00010$,
%
%D diagram imp-cube-notnot
%D 2Dx      100 +20    +25  +20	       +40 +20     +25  +20	 
%D 2D  100  P⊃Q        P⊃Q*	       P⊃Q'        P⊃Q*'	 
%D 2D  +20     (P⊃Q)*     (P⊃Q*)*         (P⊃Q)*'     (P⊃Q*)*'
%D 2D      			      			 
%D 2D  +20 P*⊃Q       P*⊃Q*	      P*⊃Q'       P*⊃Q*'	 
%D 2D  +20    (P*⊃Q)*    (P*⊃Q*)*        (P*⊃Q)*'    (P*⊃Q*)*'
%D 2D
%D ((  P⊃Q    P*⊃Q    P⊃Q*    P*⊃Q*
%D    (P⊃Q)* (P*⊃Q)* (P⊃Q*)* (P*⊃Q*)*
%D    @ 0 @ 1 <-  @ 0 @ 2  -> @ 1 @ 3  -> @ 2 @ 3  =
%D    @ 4 @ 5  =  @ 4 @ 6  =  @ 5 @ 7  =  @ 6 @ 7  =
%D    @ 0 @ 4  -> @ 1 @ 5  -> @ 2 @ 6  =  @ 3 @ 7  =
%D ))
%D ((  P⊃Q'    P*⊃Q'    P⊃Q*'    P*⊃Q*'
%D    (P⊃Q)*' (P*⊃Q)*' (P⊃Q*)*' (P*⊃Q*)*'
%D    @ 0 .tex= \dagHouse01011 @ 1 .tex= \dagHouse00011
%D    @ 2 .tex= \dagHouse11111 @ 3 .tex= \dagHouse11111
%D    @ 4 .tex= \dagHouse11111 @ 5 .tex= \dagHouse11111
%D    @ 6 .tex= \dagHouse11111 @ 7 .tex= \dagHouse11111
%D    @ 0 @ 1 <-  @ 0 @ 2  -> @ 1 @ 3  -> @ 2 @ 3  =
%D    @ 4 @ 5  =  @ 4 @ 6  =  @ 5 @ 7  =  @ 6 @ 7  =
%D    @ 0 @ 4  -> @ 1 @ 5  -> @ 2 @ 6  =  @ 3 @ 7  =
%D ))
%D enddiagram
%D
$$\diag{imp-cube-notnot}$$



\newpage
% --------------------
% «tops-for-or-and-imp»  (to ".tops-for-or-and-imp")
% (s "The topologies for `or' and `implies'" "tops-for-or-and-imp")
\myslide {The topologies for `or' and `implies'} {tops-for-or-and-imp}

\def\dagRehprime#1#2#3#4#5#6#7{%
  \dagpicture(26,60)(-10,-36)[16]{
    \dagput( 0, 12){$#1$}    % top
    \dagput( 0,  0){$#2$}    % second line
    \dagput(-6,-12){$#3$}    % third line, left
    \dagput( 6,-12){$#4$}    % third line, right
    \dagput( 0,-24){$#5$}    % fourth line, left
    \dagput(12,-24){$#6$}    % fourth line, left
    \dagput( 6,-36){$#7$}    % bottom
  }}

$\dagReh0011 ∨ \dagReh???? = \dagReh??11$

$\dagReh0011 ⊃ \dagReh???? = (\dagReh0011 ⊃_c \dagReh????)^o
                        = (_c\dagReh0011 ∨_c \dagReh????)^o
                           = (\dagReh1100 ∨_c \dagReh????)^o
                           = (\dagReh11??)^o$

The image of an idempotent operator is its fixset.

% $\bhbox{\dagRehprime1234567}$

%D diagram ??
%D 2Dx     100 +20 +20 +20
%D 2D  100     A
%D 2D
%D 2D  +25     B
%D 2D
%D 2D  +20 C       D
%D 2D
%D 2D  +20     E       F
%D 2D
%D 2D  +20         G
%D 2D
%D (( A .tex= \dagReh1111
%D    B .tex= \dagReh0111
%D    C .tex= \dagReh0101  D .tex= \dagReh0011
%D    E .tex= \dagReh0001  F .tex= \dagReh0010
%D    G .tex= \dagReh0000
%D    A B - B C - B D - C E - D E - D F - E G - F G -
%D ))
%D enddiagram

%D diagram ??or
%D 2Dx     100 +20 +20 +20
%D 2D  100     A
%D 2D
%D 2D  +25     B
%D 2D
%D 2D  +20 C       D
%D 2D
%D 2D  +20     E       F
%D 2D
%D 2D  +20         G
%D 2D
%D (( A .tex= \dagRehprime\x\o\o\o\o\o\o
%D    B .tex= \dagRehprime\x\x\o\o\o\o\o
%D    C .tex= \dagRehprime\x\x\x\o\o\o\o  D .tex= \dagRehprime\x\x\o\x\o\o\o
%D    E .tex= \dagRehprime\x\x\x\x\x\o\o  F .tex= \dagRehprime\x\x\o\x\o\x\o
%D    G .tex= \dagRehprime\x\x\x\x\x\x\x
%D    A B - B C - B D - C E - D E - D F - E G - F G -
%D ))
%D enddiagram

%D diagram ??imp
%D 2Dx     100 +20 +20 +20
%D 2D  100     A
%D 2D
%D 2D  +25     B
%D 2D
%D 2D  +20 C       D
%D 2D
%D 2D  +20     E       F
%D 2D
%D 2D  +20         G
%D 2D
%D (( A .tex= \dagRehprime\x\x\x\x\x\x\x
%D    B .tex= \dagRehprime\x\o\x\x\x\x\x
%D    C .tex= \dagRehprime\x\o\o\x\o\x\o  D .tex= \dagRehprime\x\o\x\o\o\x\x
%D    E .tex= \dagRehprime\x\o\o\o\o\x\o  F .tex= \dagRehprime\x\o\x\o\o\o\o
%D    G .tex= \dagRehprime\x\o\o\o\o\o\o
%D    A B - B C - B D - C E - D E - D F - E G - F G -
%D ))
%D enddiagram
%D
$$\def\o{\bol}
  \def\x{\bul}
  \diag{??}
  \qquad
  \diag{??or}
  \qquad
  \diag{??imp}
$$



\newpage
% --------------------
% «more-about-not-not»  (to ".more-about-not-not")
% (s "More about double negation" "more-about-not-not")
\myslide {More about double negation} {more-about-not-not}

The value of $P$ depends only on the values of $P$

on the terminal worlds (the ``leaves'').

\msk

How to see this:

\ssk

$P$ is the opposite of $P$ at the leaf-worlds and is the

biggest possible (i.e., as 1-ish as possible) in the

other worlds;

$P$ coincides with $P$ at the leaf-worlds and is the

biggest possible in the other worlds.

%D diagram not-on-leaf-worlds
%D 2Dx     100     +40       +40
%D 2D  100 P
%D 2D         |-->
%D 2D  +25 P' |--> notP |--> notnotP
%D 2D         |-->
%D 2D  +25 P''
%D 2D
%D (( P       .tex= \dagSeven0001100
%D    P''     .tex= \dagSeven0101100
%D    P'      .tex= \dagSeven???1100
%D    notP    .tex= \dagSeven0010011
%D    notnotP .tex= \dagSeven0101100
%D    P   notP |-> .plabel= a 
%D    P'  notP |-> .plabel= a 
%D    P'' notP |-> .plabel= b 
%D    notP notnotP |-> .plabel= a 
%D ))
%D enddiagram
%D
$$\diag{not-on-leaf-worlds}$$

\msk

Let's write (temporarily) `${}^?$' for ``apply `${}^*$' or not''.

$P^?∧Q^?$ stands for: $P∧Q$, $P∧Q^*$, $P^*∧Q$, $P^*∧Q^*$ ---

four truth-values.

\msk

Fact: when ${}^* = $,

$(P^?∧Q^?)^*$ is well-defined,

$(P^?∨Q^?)^*$ is well-defined,

$(P^?⊃Q^?)^*$ is well-defined,

$(P)^*$ is well-defined ---

the outer `${}^*$' dominates everything and makes

all inner applications of `${}^*$'s irrelevant.

\msk

In the cubes from the previous slides,

``the outer `${}^*$' dominates'' means:

``the four truth-values in the front face ---

the `$(P^?\text{ op }Q^?)^*$'s --- are all equivalent''.

This is not true for the modality $P^* = P^{(\aa∨)} = \aa∨P$!




\newpage
% --------------------
% «modalities-alt-axioms»  (to ".modalities-alt-axioms")
% (s "Modalities: alternative axioms" "modalities-alt-axioms")
\myslide {Modalities: alternative axioms} {modalities-alt-axioms}

A {\sl Lawvere-Tierney topology} is usually defined as an arrow $j:  \to $

such that these three diagrams commute:

%:*`*\ign *
\def\ign#1{}

%D diagram LT-topology
%D 2Dx     100     +30   +20       +30      +30          +35
%D 2D          t               j                   /\
%D 2D  100 1 ----> `0   `2 ----> `3      × -------> 
%D 2D        \      |        \      |        |           |
%D 2D       t \     | j     j \     | j  j×j |           | j
%D 2D          \    v          \    v        v     /\    v
%D 2D  +30      -> `1          -> `4     {×} -----> {}
%D 2D
%D (( 1 `0 `1
%D    @ 0 @ 1 -> .plabel= a t
%D    @ 0 @ 2 -> .plabel= l t
%D    @ 1 @ 2 -> .plabel= r j
%D ))
%D (( `2 `3 `4
%D    @ 0 @ 1 -> .plabel= a j
%D    @ 0 @ 2 -> .plabel= l j
%D    @ 1 @ 2 -> .plabel= r j
%D ))
%D (( ×  {×} {}
%D    @ 0 @ 1 -> .plabel= a {∧}
%D    @ 0 @ 2 -> .plabel= l j×j
%D    @ 1 @ 3 -> .plabel= r j
%D    @ 2 @ 3 -> .plabel= a {∧}
%D ))
%D enddiagram
%D
$$\diag{LT-topology}$$

Which means:
$$ Ï[]=Ï[^*] \qquad Ï[P^*]=Ï[P^{**}] \qquad Ï[P^*∧Q^*]=Ï[(P∧Q)^*] $$
%:
%:  -----     -------   -------   -------------  -------------
%:  |-*     P*|-P**   P**|-P*   P*∧Q*|-(P∧Q)*  (P∧Q)*|-P*∧Q*
%:
%:  ^LT-ax-1  ^LT-ax-2  ^LT-ax-3  ^LT-ax-4       ^LT-ax-5
%:
$$\ded{LT-ax-1} \qquad \ded{LT-ax-2} \qquad \ded{LT-ax-3}$$

$$\ded{LT-ax-4} \qquad \ded{LT-ax-5}$$

\medskip

It is not clear that these axioms (``LT axioms'')

are equivalent to the three axioms (``LT-modality axioms'')

that we were using before...

We know that the modality axioms imply all the LT axioms,

but it is not obvious that the modality axioms $ \vdash ^*$

and \quad $\cded{ax*-2}$

can be proved from the LT axioms...

\medskip

Here are the proofs:
%:
%:                     P|-Q
%:                    ------
%:                    |-P⊃Q
%:   --------       ============
%:   P|-<=>P       |-P<=>(P∧Q)
%:  ----------    ---------------
%:  P|-*<=>P*    |-P*<=>(P*∧Q*)
%:  ----------    ---------------
%:  P|-<=>P*        |-P*⊃Q*
%:  ---------        --------
%:    P|-P*           P*|-Q*
%:
%:    ^LT-equiv-1     ^LT-equiv-2
%:
$$\ded{LT-equiv-1} \qquad \ded{LT-equiv-2}$$



\newpage
% --------------------
% «LT-modalities-quants»  (to ".LT-modalities-quants")
% (s "LT-modalities and the quantifiers" "LT-modalities-quants")
\myslide {LT-modalities and the quantifiers} {LT-modalities-quants}


Quantifiers:
%:
%:     -------          --------------
%:     P|-x.P          x.P*|-(x.P)*
%:   -----------      ------------------
%:   P*|-(x.P)*      (x.P*)*|-(x.P)**
%:  --------------    ------------------
%:  x.P*|-(x.P)*    (x.P*)*|-(x.P)*
%:
%:  ^ex*-1            ^ex*-2
%:
%:
%:     -------
%:     x.P|-P
%:   -----------      ----------------
%:   (x.P)*|-P*      (x.P*)*|-x.P**
%:  --------------    ----------------
%:  (x.P)*|-x.P*    (x.P*)*|-x.P*
%:
%:  ^fa*-1            ^fa*-2
%:
$$\ded{ex*-1} \qquad \ded{ex*-2}$$
$$\ded{fa*-1} \qquad \ded{fa*-2}$$

%D diagram ex-square
%D 2Dx      100       +40
%D 2D  100  x.P      x.P*
%D 2D
%D 2D  +40 (x.P)*   (x.P*)*
%D 2D
%D ((  x.P    x.P*   ->
%D    (x.P)* (x.P*)* =
%D     x.P   (x.P)*  ->
%D     x.P*  (x.P*)* ->
%D ))
%D enddiagram
%D
%D diagram fa-square
%D 2Dx      100       +40
%D 2D  100  x.P      x.P*
%D 2D
%D 2D  +40 (x.P)*   (x.P*)*
%D 2D
%D ((  x.P    x.P*   ->
%D    (x.P)* (x.P*)* ->
%D     x.P   (x.P)*  ->
%D     x.P*  (x.P*)* =
%D ))
%D enddiagram
%D
$$\diag{ex-square} \qquad \diag{fa-square}$$



\newpage
% --------------------
% «sat-cov-fibration»  (to ".sat-cov-fibration")
% (s "The fibration of saturated covers" "sat-cov-fibration")
\myslide {The fibration of saturated covers} {sat-cov-fibration}

\def\bbK{\mathbb{K}}
\def\bbV{\mathbb{V}}
\def\OKop{\Opens(\bbK^\op)}
\def\OOmop{\Opens(^\op)}
\def\calU{\mathcal{U}}
\def\calV{\mathcal{V}}

For a DAG $\bbD$, define $\bbD' := \Opens(\bbD)^\op \equiv (\Opens(\bbD), \supseteq)$.

For example, when $\bbV := \dagVee***$, we have:

%D diagram satcov-fibration
%D 2Dx      100     +40   +15   +40    +40
%D 2D  100 _X1           _V ->
%D 2D  +20 _X0 -------->       _W ---> emp1
%D 2D  +20     --> _U ------->         emp0
%D 2D
%D 2D  +20                V --->
%D 2D  +20  X ---------->       W --> \emp
%D 2D  +20    ----> U --------->
%D 2D
%D 2D  +20               \bb ->
%D 2D  +20                     \cc
%D 2D  +20         \aa ------>
%D 2D
%D (( _X1  .tex= \dagKite11111 y+= -5
%D    _X0  .tex= \dagKite01111
%D    _U   .tex= \dagKite01011
%D    _V   .tex= \dagKite00111
%D    _W   .tex= \dagKite00011
%D    emp1 .tex= \dagKite00001
%D    emp0 .tex= \dagKite00000 y+= 5
%D    _X1 _X0 -> _X0 _U -> _X0 _V -> _U _W -> _V _W -> _W emp1 -> emp1 emp0 ->
%D ))
%D (( X .tex= \foo{X}{\dagVee111}
%D    U .tex= \foo{U}{\dagVee101}
%D    V .tex= \foo{V}{\dagVee011}
%D    W .tex= \foo{W}{\dagVee001}
%D    \emp .tex= \foo{\emp}{\dagVee000}
%D    X U -> X V -> U W -> V W -> W \emp ->
%D ))
%D (( \aa \cc -> \bb \cc ->
%D ))
%D enddiagram
%D
% {\def\foo#1#2{#1{\equiv}#2}
$\def\foo#1#2{#1{\equiv}#2}
 % \foo{A}{B}
 \diag{satcov-fibration}
$
% }

\msk

% Fact: when $$ is a topology
% 
% the DAG $\OOmop$ is a fibration over $$,
% 
% with $\bigcup$ as the projection functor.
% 
% For example, when $ := \Opens(\bbV)$ we have:
% 
% 
% \msk


The projection $\bigcup: \OOmop \to $ respects $∧$ and $∨$, i.e.,

if $\bigcup \calU^\bul = U$ and $\bigcup \calV^\bul = V$ then

$\bigcup(\calU^\bul ∨ \calV^\bul) = U∨V$ (this is easy to see), and also

$\bigcup(\calU^\bul ∧ \calV^\bul) = U∧V$ (look at each $w  \bigcup(\calU^\bul ∧ \calV^\bul)$).

\msk

Each fiber $\bigcupU$ is a lattice with top element $\calU^\dbul$.

When $$ comes from a finite topology we can take

the intersection of all saturated covers of $U$,

and this gives a minimal saturated cover for $U$,

that we will call $\calU^\bulm$.

\msk

Fact: $\bulm \dashv \bigcup \dashv \dbul$.

%D diagram OKadj
%D 2Dx     100     +40   +30   +30
%D 2D  100 \OKop   AL -> B --> CR
%D 2D      ^v^     ^     v     ^
%D 2D  +30 \bbK    A --> BM -> C
%D 2D
%D (( \OKop .tex= \OOmop  \bbK .tex= 
%D    \OKop \bbK <. sl__ .plabel= l *-
%D    \OKop \bbK ->      .plabel= m \bigcup
%D    \OKop \bbK <- sl^^ .plabel= r **
%D    AL .tex= \dagKite01111  A  .tex= X
%D    B  .tex= \dagKite01111  BM .tex= X
%D    CR .tex= \dagKite11111  C  .tex= X
%D    AL B -> B CR ->   A BM -> BM C ->
%D    AL A <.| .plabel= l *-
%D    B BM |-> .plabel= m \bigcup
%D    CR C <-| .plabel= r **
%D ))
%D enddiagram
%D
$$\diag{OKadj}$$




\newpage
% --------------------
% «embedding»  (to ".embedding")
% (s "Embedding" "embedding")
\myslide {Embedding} {embedding}

A topology is a DAG in a natural way:

if $V, U  \O(X)$, then $V \to U$ iff $V \subseteq U$.

We will prefer $\O(X)^\op$ rather than $\O(X)$, for two

reasons: one is because then we will have a monotonic function
%
$$\begin{array}{rrcl}
  \dnto: & \D  & \to & \O(\D)^\op \\
         & \aa & \mto & \dnto\aa
  \end{array}
$$


%D diagram D-to-O(D)op
%D 2Dx     100 +15 +15  +40 +15 +15  +25 +15 +15
%D 2D  100                  X            X'   
%D 2D		              	          
%D 2D  +20 \aa     \bb  A       B    A'      B'
%D 2D		              	          
%D 2D  +20     \cc          C   	 C'   
%D 2D		              	          
%D 2D  +20                  O   	 O'     
%D 2D
%D 2D  +20
%D 2D
%D (( \aa \cc -> \bb \cc ->
%D ))
%D ((       X .tex= \{\aa,\bb,\cc\}	    
%D    A .tex= \{\aa,\cc\}  B .tex= \{\bb,\cc\}
%D              C .tex= \{\cc\}	    
%D              O .tex= \emp
%D    X A -> X B -> A C -> B C -> C O ->
%D ))
%D ((       X' .tex= \dagVee111	    
%D    A' .tex= \dagVee101  B' .tex= \dagVee011
%D              C' .tex= \dagVee001
%D              O' .tex= \dagVee000
%D    X' A' -> X' B' -> A' C' -> B' C' -> C' O' ->
%D ))
%D (( \bb relphantom  5 8  A  relphantom -10 8 ->
%D      B relphantom  8 8  A' relphantom  -3 8 =
%D ))
%D enddiagram
%D
$$\diag{D-to-O(D)op}$$


\newpage
% --------------------
% «geometric-morphisms»  (to ".geometric-morphisms")
% (s "Geometric morphisms" "geometric-morphisms")
\myslide {Geometric morphisms} {geometric-morphisms}

%:*****

The obvious continuous function $f: 3 \to \bbV$

induces a geometric morphism, $(f^* \dashv f_*): \Set^3 \to \Set^V$.

It is essential: $f^! \dashv f^* \dashv f_*$.

%D diagram gm-1
%D 2Dx     100 +15 +15
%D 2D  100 a       b
%D 2D  +20     c
%D 2D
%D (( a .tex= A_\aa b .tex= A_\bb c .tex= A_\cc
%D    a place b place c place
%D ))
%D enddiagram
%D diagram gm-2
%D 2Dx     100 +20 +20
%D 2D  100 a       b
%D 2D  +20     c
%D 2D
%D (( a .tex= A_\aa b .tex= A_\bb c .tex= A_\aa{+}A_\bb{+}A_\cc
%D    a c -> b c ->
%D ))
%D enddiagram
%D diagram gm-3
%D 2Dx     100 +15 +15
%D 2D  100 a       b
%D 2D  +20     c
%D 2D
%D (( a .tex= B_\aa b .tex= B_\bb c .tex= B_\cc
%D    a place b place c place
%D ))
%D enddiagram
%D diagram gm-4
%D 2Dx     100 +20 +20
%D 2D  100 a       b
%D 2D  +20     c
%D 2D
%D (( a .tex= B_\aa b .tex= B_\bb c .tex= B_\cc
%D    a c -> b c ->
%D ))
%D enddiagram
%D diagram gm-5
%D 2Dx     100 +15 +15
%D 2D  100 a       b
%D 2D  +20     c
%D 2D
%D (( a .tex= C_\aa b .tex= C_\bb c .tex= C_\cc
%D    a place b place c place
%D ))
%D enddiagram
%D diagram gm-6
%D 2Dx     100 +20 +20
%D 2D  100 a       b
%D 2D  +20     c
%D 2D
%D (( a .tex= C_\aa{×}C_\cc b .tex= C_\bb{×}C_\cc c .tex= C_\cc
%D    a c -> b c ->
%D ))
%D enddiagram
%D diagram gm-example
%D 2Dx     100    +75
%D 2D  100 A      B
%D 2D
%D 2D  +60 C      D
%D 2D
%D 2D  +60 E      F
%D 2D
%D 2D  +40 \Set^3 \Set^bbV
%D 2D
%D (( A .tex= \usebox{\myboxa}
%D    B .tex= \usebox{\myboxb}
%D    C .tex= \usebox{\myboxc}
%D    D .tex= \usebox{\myboxd}
%D    E .tex= \usebox{\myboxe}
%D    F .tex= \usebox{\myboxf}
%D    A B |-> .plabel= a f_!
%D    A C -> B D -> A D harrownodes nil 20 nil <->
%D    C D <-| .plabel= a f^*
%D    C E -> D F -> C F harrownodes nil 20 nil <->
%D    E F |-> .plabel= a f_*
%D ))
%D (( \Set^3 \Set^bbV
%D    @ 0 @ 1 -> sl^^ .plabel= a f_!
%D    @ 0 @ 1 <-      .plabel= m f^*
%D    @ 0 @ 1 -> sl__ .plabel= b f_*
%D ))
%D enddiagram
%D
$$\savebox{\myboxa}{$\diag{gm-1}$}
  \savebox{\myboxb}{$\diag{gm-2}$}
  \savebox{\myboxc}{$\diag{gm-3}$}
  \savebox{\myboxd}{$\diag{gm-4}$}
  \savebox{\myboxe}{$\diag{gm-5}$}
  \savebox{\myboxf}{$\diag{gm-6}$}
  \diag{gm-example}
$$

A simpler example:

%D diagram gm-example-2
%D 2Dx     100    +40
%D 2D  100 A      B
%D 2D
%D 2D  +25 C      D
%D 2D
%D 2D  +25 E      F
%D 2D
%D 2D  +25 \Set^2 \Set^2{}
%D 2D
%D (( A .tex= (A,A')
%D    B .tex= (A+A',0)
%D    C .tex= (B,B')
%D    D .tex= (B,B)
%D    E .tex= (C,C')
%D    F .tex= (C×C',1)
%D    A B |-> .plabel= a g_!
%D    A C -> B D -> A D harrownodes nil 20 nil <->
%D    C D <-| .plabel= a g^*
%D    C E -> D F -> C F harrownodes nil 20 nil <->
%D    E F |-> .plabel= a g_*
%D ))
%D (( \Set^2 \Set^2{}
%D    @ 0 @ 1 -> sl^^ .plabel= a g_!
%D    @ 0 @ 1 <-      .plabel= m g^*
%D    @ 0 @ 1 -> sl__ .plabel= b g_*
%D ))
%D enddiagram
%D
$$\diag{gm-example-2}$$

%:****^{**}*
%:***^**

%*

\end{document}

% Local Variables:
% coding:           raw-text-unix
% ee-anchor-format: "«%s»"
% End: