claytext demo


Posts here have been ressurrected from several years ago

I have written a lot of [code]( in the past.


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.
  by apply path_ishprop.
  1. Every element of $A$ is either unit or nilpotent.
  2. $A/\mathfrak{N}$ is a field.
  1. The Merge dominates the Split, in which case, the Merge dominates everything lying on the outEdges of the Split leading to the Merge
  2. The Split dominates the Merge, in which case, the Split dominates everything on its outEdges leading to the Merge.

† Hat tip to [Sanjoy]( for pointing out the fifth case.

‡ You might want to merge loops that share a header in a post-pass.