# mathlib3documentation

data.two_pointing

# Two-pointings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]
def two_pointing.decidable_eq (α : Type u_3) [a : decidable_eq α] :
theorem two_pointing.ext {α : Type u_3} (x y : two_pointing α) (h : x.to_prod = y.to_prod) :
x = y
@[ext]
structure two_pointing (α : Type u_3) :
Type u_3

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

Instances for two_pointing
theorem two_pointing.ext_iff {α : Type u_3} (x y : two_pointing α) :
@[simp]
theorem two_pointing.swap_to_prod {α : Type u_1} (p : two_pointing α) :
def two_pointing.swap {α : Type u_1} (p : two_pointing α) :

Swaps the two pointed elements.

Equations
theorem two_pointing.swap_fst {α : Type u_1} (p : two_pointing α) :
theorem two_pointing.swap_snd {α : Type u_1} (p : two_pointing α) :
@[simp]
theorem two_pointing.swap_swap {α : Type u_1} (p : two_pointing α) :
p.swap.swap = p
@[reducible]
theorem two_pointing.to_nontrivial {α : Type u_1} (p : two_pointing α) :
@[protected, instance]
def two_pointing.nonempty {α : Type u_1} [nontrivial α] :
@[simp]
def two_pointing.pi (α : Type u_1) {β : Type u_2} (q : two_pointing β) [nonempty α] :

The two-pointing of constant functions.

Equations
@[simp]
theorem two_pointing.pi_fst (α : Type u_1) {β : Type u_2} (q : two_pointing β) [nonempty α] :
@[simp]
theorem two_pointing.pi_snd (α : Type u_1) {β : Type u_2} (q : two_pointing β) [nonempty α] :
def two_pointing.prod {α : Type u_1} {β : Type u_2} (p : two_pointing α) (q : two_pointing β) :

The product of two two-pointings.

Equations
@[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 β) :

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

Equations
@[simp]
theorem two_pointing.sum_fst {α : Type u_1} {β : Type u_2} (p : two_pointing α) (q : two_pointing β) :
(p.sum q).to_prod.fst =
@[simp]
theorem two_pointing.sum_snd {α : Type u_1} {β : Type u_2} (p : two_pointing α) (q : two_pointing β) :
(p.sum q).to_prod.snd =
@[protected]

The ff, tt two-pointing of bool.

Equations
@[simp]
@[simp]
@[protected, instance]
Equations
@[protected]

The false, true two-pointing of Prop.

Equations
@[simp]
@[simp]