This file defines
TwoPointing α, the type of two pointings of
α. A two-pointing is the data of
two distinct terms.
This is morally a Type-valued
Nontrivial. Another type which is quite close in essence is
prod is a cospan in the category of types. This forms the category of
bipointed types. Two-pointed types form a full subcategory of those.
- [nLab, Coalgebra of the real interval] (https://ncatlab.org/nlab/show/coalgebra+of+the+real+interval)