mathlib3 documentation

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 #

structure Twop  :
Type (u+1)

The category of two-pointed types.

Instances for Twop
@[protected, instance]
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]

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

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

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

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

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

Equations
@[simp]
@[simp]

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

Equations

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