# Documentation

Mathlib.CategoryTheory.Category.Bipointed

# The category of bipointed types #

This defines Bipointed, the category of bipointed types.

## TODO #

Monoidal structure

structure Bipointed :
Type (u + 1)

The category of bipointed types.

Instances For
def Bipointed.of {X : Type u_3} (to_prod : X × X) :

Turns a bipointing into a bipointed type.

Instances For
@[simp]
theorem Bipointed.coe_of {X : Type u_3} (to_prod : X × X) :
(Bipointed.of to_prod).X = X
def Prod.Bipointed {X : Type u_3} (to_prod : X × X) :

Alias of Bipointed.of.

Turns a bipointing into a bipointed type.

Instances For
theorem Bipointed.Hom.ext {X : Bipointed} {Y : Bipointed} (x : ) (y : ) (toFun : x.toFun = y.toFun) :
x = y
theorem Bipointed.Hom.ext_iff {X : Bipointed} {Y : Bipointed} (x : ) (y : ) :
x = y x.toFun = y.toFun
structure Bipointed.Hom (X : Bipointed) (Y : Bipointed) :

Morphisms in Bipointed.

Instances For
@[simp]
theorem Bipointed.Hom.id_toFun (X : Bipointed) (a : X.X) :

The identity morphism of X : Bipointed.

Instances For
@[simp]
theorem Bipointed.Hom.comp_toFun {X : Bipointed} {Y : Bipointed} {Z : Bipointed} (f : ) (g : ) :
∀ (a : X.X), = (g.toFun f.toFun) a
def Bipointed.Hom.comp {X : Bipointed} {Y : Bipointed} {Z : Bipointed} (f : ) (g : ) :

Composition of morphisms of Bipointed.

Instances For
@[simp]
theorem Bipointed.swap_map_toFun :
∀ {X Y : Bipointed} (f : X Y) (a : X.X), Bipointed.Hom.toFun (Bipointed.swap.map f) a =
@[simp]
theorem Bipointed.swap_obj_X (X : Bipointed) :
(Bipointed.swap.obj X).X = X.X
@[simp]
theorem Bipointed.swap_obj_toProd (X : Bipointed) :
(Bipointed.swap.obj X).toProd = Prod.swap X.toProd

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

Instances For
@[simp]
theorem Bipointed.swapEquiv_functor_obj_toProd (X : Bipointed) :
(Bipointed.swapEquiv.functor.obj X).toProd = Prod.swap X.toProd
@[simp]
theorem Bipointed.swapEquiv_unitIso_inv_app_toFun (X : Bipointed) :
∀ (a : ().X), Bipointed.Hom.toFun (Bipointed.swapEquiv.unitIso.inv.app X) a = Bipointed.Hom.toFun (CategoryTheory.CategoryStruct.comp (Bipointed.swap.map (Bipointed.swap.map { toFun := id, map_fst := (_ : id ().toProd.fst = id ().toProd.fst), map_snd := (_ : id ().toProd.snd = id ().toProd.snd) })) (CategoryTheory.CategoryStruct.comp (Bipointed.swap.map { toFun := id, map_fst := (_ : id (().obj (Bipointed.swap.obj X)).toProd.fst = id (().obj (Bipointed.swap.obj X)).toProd.fst), map_snd := (_ : id (().obj (Bipointed.swap.obj X)).toProd.snd = id (().obj (Bipointed.swap.obj X)).toProd.snd) }) { toFun := id, map_fst := (_ : id ().toProd.fst = id ().toProd.fst), map_snd := (_ : id ().toProd.snd = id ().toProd.snd) })) ()
@[simp]
theorem Bipointed.swapEquiv_functor_map_toFun :
∀ {X Y : Bipointed} (f : X Y) (a : X.X), Bipointed.Hom.toFun (Bipointed.swapEquiv.functor.map f) a =
@[simp]
theorem Bipointed.swapEquiv_inverse_obj_toProd (X : Bipointed) :
(Bipointed.swapEquiv.inverse.obj X).toProd = Prod.swap X.toProd
@[simp]
@[simp]
theorem Bipointed.swapEquiv_unitIso_hom_app_toFun (X : Bipointed) :
∀ (a : ().X), Bipointed.Hom.toFun (Bipointed.swapEquiv.unitIso.hom.app X) a = Bipointed.Hom.toFun (CategoryTheory.CategoryStruct.id (Bipointed.swap.obj (Bipointed.swap.obj X))) (Bipointed.Hom.toFun (CategoryTheory.CategoryStruct.comp { toFun := id, map_fst := (_ : id ().toProd.fst = id ().toProd.fst), map_snd := (_ : id ().toProd.snd = id ().toProd.snd) } (CategoryTheory.CategoryStruct.comp (Bipointed.swap.map { toFun := id, map_fst := (_ : id (().obj (Bipointed.swap.obj X)).toProd.fst = id (().obj (Bipointed.swap.obj X)).toProd.fst), map_snd := (_ : id (().obj (Bipointed.swap.obj X)).toProd.snd = id (().obj (Bipointed.swap.obj X)).toProd.snd) }) (Bipointed.swap.map (Bipointed.swap.map { toFun := id, map_fst := (_ : id ().toProd.fst = id ().toProd.fst), map_snd := (_ : id ().toProd.snd = id ().toProd.snd) })))) a)
@[simp]
theorem Bipointed.swapEquiv_inverse_map_toFun :
∀ {X Y : Bipointed} (f : X Y) (a : X.X), Bipointed.Hom.toFun (Bipointed.swapEquiv.inverse.map f) a =
@[simp]

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

Instances For
@[simp]

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

Instances For

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

Instances For

The functor from Pointed to Bipointed which bipoints the point.

Instances For

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

Instances For

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

Instances For

BipointedToPointed_fst is inverse to PointedToBipointed.

Instances For

BipointedToPointed_snd is inverse to PointedToBipointed.

Instances For

The free/forgetful adjunction between PointedToBipointed_fst and BipointedToPointed_fst.

Instances For

The free/forgetful adjunction between PointedToBipointed_snd and BipointedToPointed_snd.

Instances For