mathlib documentation

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

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) :

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

Equations
@[simp]
@[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