# mathlib3documentation

category_theory.category.Twop

# The category of two-pointed types #

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

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)
structure Twop  :
Type (u+1)

The category of two-pointed types.

Instances for Twop
@[protected, instance]
def Twop.has_coe_to_sort  :
(Type u_1)
Equations
def Twop.of {X : Type u_1} (to_two_pointing : two_pointing X) :

Turns a two-pointing into a two-pointed type.

Equations
@[simp]
theorem Twop.coe_of {X : Type u_1} (to_two_pointing : two_pointing X) :
(Twop.of to_two_pointing) = X
def two_pointing.Twop {X : Type u_1} (to_two_pointing : two_pointing X) :

Alias of Twop.of.

@[protected, instance]
Equations

Turns a two-pointed type into a bipointed type, by forgetting that the pointed elements are distinct.

Equations
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def Twop.swap  :

Swaps the pointed elements of a two-pointed type. two_pointing.swap as a functor.

Equations
@[simp]
@[simp]
theorem Twop.swap_obj_X (X : Twop) :
@[simp]
theorem Twop.swap_map_to_fun (X Y : Twop) (f : X Y) (ᾰ : (X.to_Bipointed)) :
(Twop.swap.map f).to_fun = f.to_fun
@[simp]
theorem Twop.swap_equiv_inverse_map_to_fun (X Y : Twop) (f : X Y) (ᾰ : (X.to_Bipointed)) :
= f.to_fun
def Twop.swap_equiv  :

The equivalence between Twop and itself induced by prod.swap both ways.

Equations
@[simp]
@[simp]
@[simp]
theorem Twop.swap_equiv_functor_map_to_fun (X Y : Twop) (f : X Y) (ᾰ : (X.to_Bipointed)) :
= f.to_fun
@[simp]
@[simp]
@[simp]

The functor from Pointed to Twop which adds a second point.

Equations
@[simp]
@[simp]
theorem Pointed_to_Twop_fst_map_to_fun (X Y : Pointed) (f : X Y) (o : option X) :
o = o
@[simp]
theorem Pointed_to_Twop_snd_map_to_fun (X Y : Pointed) (f : X Y) (o : option X) :
o = o
@[simp]

The functor from Pointed to Twop which adds a first point.

Equations
@[simp]
@[simp]

Adding a second point is left adjoint to forgetting the second point.

Equations

Adding a first point is left adjoint to forgetting the first point.

Equations