# The category of pointed types #

This defines Pointed, the category of pointed types.

## TODO #

• Monoidal structure
• Upgrade typeToPointed to an equivalence
structure Pointed :
Type (u + 1)

The category of pointed types.

• X : Type u

the underlying type

• point : self.X

the distinguished element

Instances For
def Pointed.of {X : Type u_3} (point : X) :

Turns a point into a pointed type.

Equations
Instances For
@[simp]
theorem Pointed.coe_of {X : Type u_3} (point : X) :
(Pointed.of point).X = X
def Prod.Pointed {X : Type u_3} (point : X) :

Alias of Pointed.of.

Turns a point into a pointed type.

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

Morphisms in Pointed.

• toFun : X.XY.X

the underlying map

• map_point : self.toFun X.point = Y.point

compatibility with the distinguished points

Instances For
theorem Pointed.Hom.map_point {X : Pointed} {Y : Pointed} (self : X.Hom Y) :
self.toFun X.point = Y.point

compatibility with the distinguished points

@[simp]
theorem Pointed.Hom.id_toFun (X : Pointed) (a : X.X) :
().toFun a = id a
def Pointed.Hom.id (X : Pointed) :
X.Hom X

The identity morphism of X : Pointed.

Equations
• = { toFun := id, map_point := }
Instances For
instance Pointed.Hom.instInhabited (X : Pointed) :
Inhabited (X.Hom X)
Equations
• = { default := }
@[simp]
theorem Pointed.Hom.comp_toFun {X : Pointed} {Y : Pointed} {Z : Pointed} (f : X.Hom Y) (g : Y.Hom Z) :
∀ (a : X.X), (f.comp g).toFun a = (g.toFun f.toFun) a
def Pointed.Hom.comp {X : Pointed} {Y : Pointed} {Z : Pointed} (f : X.Hom Y) (g : Y.Hom Z) :
X.Hom Z

Composition of morphisms of Pointed.

Equations
• f.comp g = { toFun := g.toFun f.toFun, map_point := }
Instances For
@[simp]
theorem Pointed.Hom.id_toFun' (X : Pointed) :
.toFun = id
@[simp]
theorem Pointed.Hom.comp_toFun' {X : Pointed} {Y : Pointed} {Z : Pointed} (f : X Y) (g : Y Z) :
.toFun = g.toFun f.toFun
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Pointed.Iso.mk_inv_toFun {α : Pointed} {β : Pointed} (e : α.X β.X) (he : e α.point = β.point) (a : β.X) :
().inv.toFun a = e.symm a
@[simp]
theorem Pointed.Iso.mk_hom_toFun {α : Pointed} {β : Pointed} (e : α.X β.X) (he : e α.point = β.point) (a : α.X) :
().hom.toFun a = e a
def Pointed.Iso.mk {α : Pointed} {β : Pointed} (e : α.X β.X) (he : e α.point = β.point) :
α β

Constructs an isomorphism between pointed types from an equivalence that preserves the point between them.

Equations
• = { hom := { toFun := e, map_point := he }, inv := { toFun := e.symm, map_point := }, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem typeToPointed_map_toFun :
∀ {X Y : Type u} (f : X Y) (a : ), (typeToPointed.map f).toFun a =
@[simp]
theorem typeToPointed_obj_X (X : Type u) :
(typeToPointed.obj X).X =
@[simp]
theorem typeToPointed_obj_point (X : Type u) :
(typeToPointed.obj X).point = none

Option as a functor from types to pointed types. This is the free functor.

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

typeToPointed is the free functor.

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