The category of two-pointed types #
This defines TwoP
, the category of two-pointed types.
References #
- [nLab, coalgebra of the real interval] (https://ncatlab.org/nlab/show/coalgebra+of+the+real+interval)
Equations
- TwoP.instCoeSortType = { coe := TwoP.X }
Turns a two-pointing into a two-pointed type.
Equations
- TwoP.of toTwoPointing = { X := X, toTwoPointing := toTwoPointing }
Instances For
@[simp]
Equations
- TwoP.instInhabited = { default := TwoP.of TwoPointing.bool }
Turns a two-pointed type into a bipointed type, by forgetting that the pointed elements are distinct.
Instances For
Swaps the pointed elements of a two-pointed type. TwoPointing.swap
as a functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
Adding a second point is left adjoint to forgetting the second point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Adding a first point is left adjoint to forgetting the first point.
Equations
- One or more equations did not get rendered due to their size.