Two-pointings #
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 Sym2
.
Categorically speaking, 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.
References #
- [nLab, Coalgebra of the real interval] (https://ncatlab.org/nlab/show/coalgebra+of+the+real+interval)
fst
andsnd
are distinct termsfst_ne_snd : toProd.fst ≠ toProd.snd
Two-pointing of a type. This is a Type-valued termed Nontrivial
.
Instances For
Equations
- instDecidableEqTwoPointing = decEqTwoPointing✝
Swaps the two pointed elements.
Equations
- TwoPointing.swap p = { toProd := (p.toProd.snd, p.toProd.fst), fst_ne_snd := (_ : p.toProd.snd ≠ p.toProd.fst) }
The two-pointing of constant functions.
Equations
- One or more equations did not get rendered due to their size.
The product of two two-pointings.
Equations
- One or more equations did not get rendered due to their size.
The sum of two pointings. Keeps the first point from the left and the second point from the right.
The false
, true
two-pointing of Bool
.
Equations
- TwoPointing.bool = { toProd := (false, true), fst_ne_snd := Bool.ff_ne_tt }
Equations
- TwoPointing.instInhabitedTwoPointingBool = { default := TwoPointing.bool }
The False
, True
two-pointing of Prop
.
Equations
- TwoPointing.prop = { toProd := (False, True), fst_ne_snd := false_ne_true }