# mathlibdocumentation

category_theory.category.Bipointed

# The category of bipointed types #

This defines Bipointed, the category of bipointed types.

## TODO #

Monoidal structure

structure Bipointed  :
Type (u+1)
• X : Type ?
• to_prod : self.X × self.X

The category of bipointed types.

Instances for Bipointed
@[protected, instance]
def Bipointed.has_coe_to_sort  :
(Type u_1)
Equations
def Bipointed.of {X : Type u_1} (to_prod : X × X) :

Turns a bipointing into a bipointed type.

Equations
@[simp]
theorem Bipointed.coe_of {X : Type u_1} (to_prod : X × X) :
(Bipointed.of to_prod) = X
def prod.Bipointed {X : Type u_1} (to_prod : X × X) :

Alias of Bipointed.of.

@[protected, instance]
Equations
theorem Bipointed.hom.ext {X Y : Bipointed} (x y : X.hom Y) (h : x.to_fun = y.to_fun) :
x = y
theorem Bipointed.hom.ext_iff {X Y : Bipointed} (x y : X.hom Y) :
x = y x.to_fun = y.to_fun
@[ext]
structure Bipointed.hom (X Y : Bipointed) :
Type u

Morphisms in Bipointed.

Instances for Bipointed.hom
def Bipointed.hom.id (X : Bipointed) :
X.hom X

The identity morphism of X : Bipointed.

Equations
@[simp]
theorem Bipointed.hom.id_to_fun (X : Bipointed) (a : X) :
a = id a
@[protected, instance]
Equations
def Bipointed.hom.comp {X Y Z : Bipointed} (f : X.hom Y) (g : Y.hom Z) :
X.hom Z

Composition of morphisms of Bipointed.

Equations
@[simp]
theorem Bipointed.hom.comp_to_fun {X Y Z : Bipointed} (f : X.hom Y) (g : Y.hom Z) (ᾰ : X) :
(f.comp g).to_fun = (g.to_fun f.to_fun)
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem Bipointed.swap_obj_X (X : Bipointed) :

Swaps the pointed elements of a bipointed type. prod.swap as a functor.

Equations
@[simp]
theorem Bipointed.swap_map_to_fun (X Y : Bipointed) (f : X Y) (ᾰ : X) :
.to_fun = f.to_fun

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

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

The forgetful functor from Bipointed to Pointed which forgets about the second point.

Equations

The forgetful functor from Bipointed to Pointed which forgets about the first point.

Equations

The functor from Pointed to Bipointed which bipoints the point.

Equations

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

Equations

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

Equations

Bipointed_to_Pointed_fst is inverse to Pointed_to_Bipointed.

Equations
@[simp]

Bipointed_to_Pointed_snd is inverse to Pointed_to_Bipointed.

Equations
@[simp]

The free/forgetful adjunction between Pointed_to_Bipointed_fst and Bipointed_to_Pointed_fst.

Equations

The free/forgetful adjunction between Pointed_to_Bipointed_snd and Bipointed_to_Pointed_snd.

Equations