The category of pointed types #
This defines Pointed
, the category of pointed types.
TODO #
- Monoidal structure
- Upgrade
typeToPointed
to an equivalence
Turns a point into a pointed type.
Instances For
Alias of Pointed.of
.
Turns a point into a pointed type.
Instances For
theorem
Pointed.Hom.ext_iff
{X : Pointed}
{Y : Pointed}
(x : Pointed.Hom X Y)
(y : Pointed.Hom X Y)
:
theorem
Pointed.Hom.ext
{X : Pointed}
{Y : Pointed}
(x : Pointed.Hom X Y)
(y : Pointed.Hom X Y)
(toFun : x.toFun = y.toFun)
:
x = y
- toFun : X.X → Y.X
the underlying map
- map_point : Pointed.Hom.toFun s X.point = Y.point
compatibility with the distinguished points
Morphisms in Pointed
.
Instances For
@[simp]
@[simp]
theorem
Pointed.Hom.comp_toFun
{X : Pointed}
{Y : Pointed}
{Z : Pointed}
(f : Pointed.Hom X Y)
(g : Pointed.Hom Y Z)
:
∀ (a : X.X), Pointed.Hom.toFun (Pointed.Hom.comp f g) a = (g.toFun ∘ f.toFun) a
def
Pointed.Hom.comp
{X : Pointed}
{Y : Pointed}
{Z : Pointed}
(f : Pointed.Hom X Y)
(g : Pointed.Hom Y Z)
:
Pointed.Hom X Z
Composition of morphisms of Pointed
.
Instances For
@[simp]
theorem
Pointed.Iso.mk_inv_toFun
{α : Pointed}
{β : Pointed}
(e : α.X ≃ β.X)
(he : ↑e α.point = β.point)
(a : β.X)
:
Pointed.Hom.toFun (Pointed.Iso.mk e he).inv a = ↑e.symm a
@[simp]
theorem
Pointed.Iso.mk_hom_toFun
{α : Pointed}
{β : Pointed}
(e : α.X ≃ β.X)
(he : ↑e α.point = β.point)
(a : α.X)
:
Pointed.Hom.toFun (Pointed.Iso.mk e he).hom a = ↑e a
@[simp]
theorem
typeToPointed_map_toFun :
∀ {X Y : Type u} (f : X ⟶ Y) (a : Option X), Pointed.Hom.toFun (typeToPointed.map f) a = Option.map f a
Option
as a functor from types to pointed types. This is the free functor.
Instances For
typeToPointed
is the free functor.