$\Rightarrow: L \rightarrow L; (c \land a) \leq b \iff c \leq (a \Rightarrow b)$

In any topological space $(U, \tau)$ ( $U$ for universe set)
the open sets of that space form a Heyting algebra.
Here, set-union and set-intersection become the lattice join and lattice meet.
We define a "weak complement" denoted by $\lnot$ which is defined as:
$\lnot A \equiv \texttt{interior}(A^C)$

We need the $\texttt{interior}$ to make sure that we're left with an open
set. Also, this $\lnot$ is not really a complement, since we won't have that
$\lnot \lnot A = A$. but, more on that later!
We write open intervals with round parenthesis:
```
A
--(===)--
```

$\lnot A$ of the above set $A$ becomes the open interval that is in the
interior of $A$ complement.
```
--(===)-- A
==]---[== A complement
==)---(== Not A
```

Now, we can try to ask, when is $\lnot \lnot A = U$ (where $U$ is the universe
set or the full space). If we consider a set containing a single point,
then we will have:
```
==)(== A
------------ Not A
============ Not (Not A)
```

in words:
$\begin{aligned}
&A = U \setminus \{ 1 \} \\
&\lnot A = \texttt{interior}(A^c) = \texttt{interior}(\{ 1 \}) = \emptyset \\
&\lnot \lnot A = \texttt{interior}((\lnot A)^c) = \texttt{interior}(\emptyset^c) = \texttt{interior}(U) = U \\
\end{aligned}$

So in some sense, the law of excluded middle is "almost true": It holds that $A \simeq \lnot \lnot A$,
where $A$ excludes a set of points of measure zero.
This is really interesting, since it gives some sort of oddball probabilistic
flavour to things where if we blind ourselves to measure-0 sets, then $\lnot \lnot A = A$.
Now, we look at implication. The implication $A \Rightarrow B$ is the largest
set open $C$ such that $C \land A = B$. In pictures:
```
---(========)----- A
---------(=====)-- B
---------(==)----- A && B
===)-----(======== A -> B
```

The reason this is true is that from the definition:
$\begin{aligned}
&\Rightarrow: L \rightarrow L; c \leq (a \Rightarrow b) \iff (c \land a) \leq b \\
&\text{replacing $\leq$ with $=$ for insight:} \\
&\Rightarrow: L \rightarrow L; c = (a \Rightarrow b) \iff (c \land a) = b \\
\end{aligned}$

Alternatively, we can use the fact that in regular boolean algebra:
$a \Rightarrow b = \lnot a \lor b$

to derive $A -> B$:
```
---(========)----- A
===)--------(===== NOT A
---------(=====)-- B
[Extend B to everything that doesn't include
more of A than already included]
===)-----(======== NOT A or B = A -> B
```

`a -> b`

as `a`

contained in `b`

: `a -> b`

is true/top/the full real line if and only if
`a`

is contained in `b`

. We can show this using $\lnot a \lor b$ definition:
- $a \leq b$ (given)
- Since $a \leq b$, $\lnot a \geq \lnot b$, since $\lnot$ reverses inclusion order.
- $x \geq y$ implies that $x \lor p \geq y \lor p$ for all p, since $p$ is on both sides.
- Specializing to $x = \lnot a$, $y = \lnot b$, $p = b$ gives us $\lnot a \lor b \geq \lnot b \lor b$
- $\lnot b \lor b$ is universe $U$
- $\lnot a \lor b \geq U$, which means it's equal to $U$ (nothing can be greater than $U$).

```
----------(===)---- A
------(==========) B
----------(===)---- A && B
[Extend B to everything that doesn't include
more of A than already included.
But all of A is
already included!]
================== A -> B
```

`curry`

, `uncurry`

using `a -> b`

as containment: `curry`

, `uncurry`

are the adjunction/isomorphism:
```
((c,a) -> b) ~ (c -> (a -> b))
```

Read this as:
```
( c , a) -> b
(c `intersection` a) `contained in` b
```

if and only if
```
c -> (a -> b)
c `contained in` (a `implication` b)
```

That is, we have "read" `curry/uncurry`

as:
$c \land a \leq b \iff c \leq a \Rightarrow b$

which was the definition of $\Rightarrow$ we wanted!