Posts here have been ressurrected from several years ago

I have written a lot of [code](https://github.com/artagnon) in the past.

## Functors

For a fixed field $K$, consider the functors

$$ \begin{xy} \xymatrix{ \textbf{Set}\ar@<.5ex>[r]^V & \textbf{Vct}_K\ar@<.5ex>[l]^U } \end{xy} $$

```
Theorem hPropEquality (P : hProp) (a b : P) : a = b.
Proof.
by apply path_ishprop.
Qed.
```

- Every element of $A$ is either unit or nilpotent.
- $A/\mathfrak{N}$ is a field.

- The Merge dominates the Split, in which case, the Merge dominates everything lying on the outEdges of the Split leading to the Merge
- The Split dominates the Merge, in which case, the Split dominates everything on its outEdges leading to the Merge.