See the image. I got that from: wikipedia article. In that, I don't understand the first function
nil : () -> L. What is
I want to make a visual type theory so that we aren't stuck comprehending pure text for eternity.
Also, is the abstract type
List a product of some sort? The diagram doesn't indicate this since it's based on a product diagram of $E \times L$.
Assume that product has already been defined by a similar diagram and that there is a system that can interpret these smallish diagrams, so that ideally $E\times L$ and $p_L$ as well as the graphical arrows and blocks show up in a different color indicating that you cannot edit them.
Additionally in the wikipedia article, they say:
for any element e and any list l. It is implicit that cons (e, l) ≠ l cons (e, l) ≠ e cons (e1, l1) = cons (e2, l2) if e1 = e2 and l1 = l2 Note that first (nil ()) and rest (nil ()) are not defined.
But isn't the last one already true!?? How should I indicate the first two in diagram form?