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)

structure TwoPointing (α : Type u_3) extends α × α : Type u_3

Two-pointing of a type. This is a Type-valued termed Nontrivial.

• fst : α
• snd : α
• fst_ne_snd : self.toProd.1 ≠ self.toProd.2

  fst and snd are distinct terms

theorem TwoPointing.ext {α : Type u_3} {x y : TwoPointing α} (fst : x.toProd.1 = y.toProd.1) (snd : x.toProd.2 = y.toProd.2) : x = y

theorem TwoPointing.ext_iff {α : Type u_3} {x y : TwoPointing α} : x = y ↔ x.toProd.1 = y.toProd.1 ∧ x.toProd.2 = y.toProd.2

instance instDecidableEqTwoPointing {α✝ : Type u_3} [DecidableEq α✝] : DecidableEq (TwoPointing α✝)

def instDecidableEqTwoPointing.decEq {α✝ : Type u_3} [DecidableEq α✝] (x✝ x✝¹ : TwoPointing α✝) : Decidable (x✝ = x✝¹)

theorem TwoPointing.snd_ne_fst {α : Type u_1} (p : TwoPointing α) : p.toProd.2 ≠ p.toProd.1

def TwoPointing.swap {α : Type u_1} (p : TwoPointing α) : TwoPointing α

Swaps the two pointed elements.

@[simp]

theorem TwoPointing.swap_toProd {α : Type u_1} (p : TwoPointing α) : p.swap.toProd = (p.toProd.2, p.toProd.1)

theorem TwoPointing.swap_fst {α : Type u_1} (p : TwoPointing α) : p.swap.toProd.1 = p.toProd.2

theorem TwoPointing.swap_snd {α : Type u_1} (p : TwoPointing α) : p.swap.toProd.2 = p.toProd.1

@[simp]

theorem TwoPointing.swap_swap {α : Type u_1} (p : TwoPointing α) : p.swap.swap = p

theorem TwoPointing.to_nontrivial {α : Type u_1} (p : TwoPointing α) : Nontrivial α

instance TwoPointing.instNonemptyOfNontrivial {α : Type u_1} [Nontrivial α] : Nonempty (TwoPointing α)

@[simp]

theorem TwoPointing.nonempty_two_pointing_iff {α : Type u_1} : Nonempty (TwoPointing α) ↔ Nontrivial α

def TwoPointing.pi (α : Type u_1) {β : Type u_2} (q : TwoPointing β) [Nonempty α] : TwoPointing (α → β)

The two-pointing of constant functions.

@[simp]

theorem TwoPointing.pi_fst (α : Type u_1) {β : Type u_2} (q : TwoPointing β) [Nonempty α] : (pi α q).toProd.1 = Function.const α q.toProd.1

@[simp]

theorem TwoPointing.pi_snd (α : Type u_1) {β : Type u_2} (q : TwoPointing β) [Nonempty α] : (pi α q).toProd.2 = Function.const α q.toProd.2

def TwoPointing.prod {α : Type u_1} {β : Type u_2} (p : TwoPointing α) (q : TwoPointing β) : TwoPointing (α × β)

The product of two two-pointings.

@[simp]

theorem TwoPointing.prod_fst {α : Type u_1} {β : Type u_2} (p : TwoPointing α) (q : TwoPointing β) : (p.prod q).toProd.1 = (p.toProd.1, q.toProd.1)

@[simp]

theorem TwoPointing.prod_snd {α : Type u_1} {β : Type u_2} (p : TwoPointing α) (q : TwoPointing β) : (p.prod q).toProd.2 = (p.toProd.2, q.toProd.2)

def TwoPointing.sum {α : Type u_1} {β : Type u_2} (p : TwoPointing α) (q : TwoPointing β) : TwoPointing (α ⊕ β)

The sum of two pointings. Keeps the first point from the left and the second point from the right.

@[simp]

theorem TwoPointing.sum_fst {α : Type u_1} {β : Type u_2} (p : TwoPointing α) (q : TwoPointing β) : (p.sum q).toProd.1 = Sum.inl p.toProd.1

@[simp]

theorem TwoPointing.sum_snd {α : Type u_1} {β : Type u_2} (p : TwoPointing α) (q : TwoPointing β) : (p.sum q).toProd.2 = Sum.inr q.toProd.2

def TwoPointing.bool : TwoPointing Bool

The false, true two-pointing of Bool.

@[simp]

theorem TwoPointing.bool_fst : TwoPointing.bool.toProd.1 = false

@[simp]

theorem TwoPointing.bool_snd : TwoPointing.bool.toProd.2 = true

instance TwoPointing.instInhabitedBool : Inhabited (TwoPointing Bool)

def TwoPointing.prop : TwoPointing Prop

The False, True two-pointing of Prop.

@[simp]

theorem TwoPointing.prop_fst : TwoPointing.prop.toProd.1 = False

@[simp]

theorem TwoPointing.prop_snd : TwoPointing.prop.toProd.2 = True