# 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.

• X : Type u

The underlying type of a bipointed type.

• toProd : self.X × self.X

The two points of a bipointed type, bundled together as a pair.

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

Turns a bipointing into a bipointed type.

Equations
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.

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

Morphisms in Bipointed.

• toFun : X.XY.X

The underlying function of a morphism of bipointed types.

• map_fst : self.toFun X.toProd.1 = Y.toProd.1
• map_snd : self.toFun X.toProd.2 = Y.toProd.2
Instances For
theorem Bipointed.Hom.map_fst {X : Bipointed} {Y : Bipointed} (self : X.Hom Y) :
self.toFun X.toProd.1 = Y.toProd.1
theorem Bipointed.Hom.map_snd {X : Bipointed} {Y : Bipointed} (self : X.Hom Y) :
self.toFun X.toProd.2 = Y.toProd.2
@[simp]
theorem Bipointed.Hom.id_toFun (X : Bipointed) (a : X.X) :
().toFun a = id a
def Bipointed.Hom.id (X : Bipointed) :
X.Hom X

The identity morphism of X : Bipointed.

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

Composition of morphisms of Bipointed.

Equations
• f.comp g = { toFun := g.toFun f.toFun, map_fst := , map_snd := }
Instances For
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Bipointed.swap_map_toFun :
∀ {X Y : Bipointed} (f : X Y) (a : X.X), (Bipointed.swap.map f).toFun a = f.toFun 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 = X.toProd.swap

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
theorem Bipointed.swapEquiv_functor_obj_toProd (X : Bipointed) :
(Bipointed.swapEquiv.functor.obj X).toProd = X.toProd.swap
@[simp]
theorem Bipointed.swapEquiv_inverse_map_toFun :
∀ {X Y : Bipointed} (f : X Y) (a : X.X), (Bipointed.swapEquiv.inverse.map f).toFun a = f.toFun a
@[simp]
theorem Bipointed.swapEquiv_functor_map_toFun :
∀ {X Y : Bipointed} (f : X Y) (a : X.X), (Bipointed.swapEquiv.functor.map f).toFun a = f.toFun a
@[simp]
theorem Bipointed.swapEquiv_unitIso_hom_app_toFun (X : Bipointed) :
∀ (a : ().X), (Bipointed.swapEquiv.unitIso.hom.app X).toFun a = (CategoryTheory.CategoryStruct.id (Bipointed.swap.obj (Bipointed.swap.obj X))).toFun ((CategoryTheory.CategoryStruct.comp { toFun := id, map_fst := , map_snd := } (CategoryTheory.CategoryStruct.comp (Bipointed.swap.map { toFun := id, map_fst := , map_snd := }) (Bipointed.swap.map (Bipointed.swap.map { toFun := id, map_fst := , map_snd := })))).toFun a)
@[simp]
theorem Bipointed.swapEquiv_counitIso_hom_app_toFun (X : Bipointed) (a : (().obj X).X) :
(Bipointed.swapEquiv.counitIso.hom.app X).toFun a = a
@[simp]
@[simp]
theorem Bipointed.swapEquiv_unitIso_inv_app_toFun (X : Bipointed) :
∀ (a : (().obj X).X), (Bipointed.swapEquiv.unitIso.inv.app X).toFun a = (CategoryTheory.CategoryStruct.comp (Bipointed.swap.map (Bipointed.swap.map { toFun := id, map_fst := , map_snd := })) (CategoryTheory.CategoryStruct.comp (Bipointed.swap.map { toFun := id, map_fst := , map_snd := }) { toFun := id, map_fst := , map_snd := })).toFun ((CategoryTheory.CategoryStruct.id (Bipointed.swap.obj (Bipointed.swap.obj X))).toFun a)
@[simp]
theorem Bipointed.swapEquiv_counitIso_inv_app_toFun (X : Bipointed) (a : ().X) :
(Bipointed.swapEquiv.counitIso.inv.app X).toFun a = a
@[simp]
theorem Bipointed.swapEquiv_inverse_obj_toProd (X : Bipointed) :
(Bipointed.swapEquiv.inverse.obj X).toProd = X.toProd.swap

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]

The functor from Pointed to Bipointed which bipoints the point.

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
theorem pointedToBipointedCompBipointedToPointedFst_hom_app_toFun (X : Pointed) (a : (.obj X).X) :
().toFun a = a

BipointedToPointed_fst is inverse to PointedToBipointed.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem pointedToBipointedCompBipointedToPointedSnd_hom_app_toFun (X : Pointed) (a : (.obj X).X) :
().toFun a = a
@[simp]

BipointedToPointed_snd is inverse to PointedToBipointed.

Equations
• One or more equations did not get rendered due to their size.
Instances For

The free/forgetful adjunction between PointedToBipointed_fst and BipointedToPointed_fst.

Equations
• One or more equations did not get rendered due to their size.
Instances For

The free/forgetful adjunction between PointedToBipointed_snd and BipointedToPointed_snd.

Equations
• One or more equations did not get rendered due to their size.
Instances For