Two-pointings #
This file defines two_pointing α
, 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)
@[protected, instance]
@[ext]
Two-pointing of a type. This is a Type-valued termed nontrivial
.
Instances for two_pointing
- two_pointing.has_sizeof_inst
- two_pointing.nonempty
- two_pointing.inhabited
@[simp]
Swaps the two pointed elements.
@[reducible]
@[protected, instance]
@[simp]
theorem
two_pointing.nonempty_two_pointing_iff
{α : Type u_1} :
nonempty (two_pointing α) ↔ nontrivial α
def
two_pointing.pi
(α : Type u_1)
{β : Type u_2}
(q : two_pointing β)
[nonempty α] :
two_pointing (α → β)
The two-pointing of constant functions.
Equations
- two_pointing.pi α q = {to_prod := (λ (_x : α), q.to_prod.fst, λ (_x : α), q.to_prod.snd), fst_ne_snd := _}
@[simp]
theorem
two_pointing.pi_fst
(α : Type u_1)
{β : Type u_2}
(q : two_pointing β)
[nonempty α] :
(two_pointing.pi α q).to_prod.fst = function.const α q.to_prod.fst
@[simp]
theorem
two_pointing.pi_snd
(α : Type u_1)
{β : Type u_2}
(q : two_pointing β)
[nonempty α] :
(two_pointing.pi α q).to_prod.snd = function.const α q.to_prod.snd
def
two_pointing.prod
{α : Type u_1}
{β : Type u_2}
(p : two_pointing α)
(q : two_pointing β) :
two_pointing (α × β)
The product of two two-pointings.
@[simp]
theorem
two_pointing.prod_fst
{α : Type u_1}
{β : Type u_2}
(p : two_pointing α)
(q : two_pointing β) :
@[simp]
theorem
two_pointing.prod_snd
{α : Type u_1}
{β : Type u_2}
(p : two_pointing α)
(q : two_pointing β) :
@[protected]
def
two_pointing.sum
{α : Type u_1}
{β : Type u_2}
(p : two_pointing α)
(q : two_pointing β) :
two_pointing (α ⊕ β)
The sum of two pointings. Keeps the first point from the left and the second point from the right.
@[simp]
theorem
two_pointing.sum_fst
{α : Type u_1}
{β : Type u_2}
(p : two_pointing α)
(q : two_pointing β) :
@[simp]
theorem
two_pointing.sum_snd
{α : Type u_1}
{β : Type u_2}
(p : two_pointing α)
(q : two_pointing β) :
@[protected]
The ff
, tt
two-pointing of bool
.
Equations
- two_pointing.bool = {to_prod := (bool.ff, bool.tt), fst_ne_snd := bool.ff_ne_tt}
@[protected, instance]
Equations
@[protected]
The false
, true
two-pointing of Prop
.
Equations
- two_pointing.Prop = {to_prod := (false, true), fst_ne_snd := false_ne_true}