The category of pointed types #
This defines Pointed
, the category of pointed types.
TODO #
- Monoidal structure
- Upgrade
Type_to_Pointed
to an equivalence
- X : Type ?
- point : self.X
The category of pointed types.
Instances for Pointed
- Pointed.has_sizeof_inst
- Pointed.has_coe_to_sort
- Pointed.inhabited
- Pointed.large_category
- Pointed.concrete_category
@[protected, instance]
Equations
Turns a point into a pointed type.
Equations
- Pointed.of point = {X := X, point := point}
@[protected, instance]
Equations
- Pointed.inhabited = {default := Pointed.of ((), ())}
@[simp]
@[protected, instance]
Equations
- Pointed.hom.inhabited X = {default := Pointed.hom.id X}
@[protected, instance]
Equations
- Pointed.large_category = {to_category_struct := {to_quiver := {hom := Pointed.hom}, id := Pointed.hom.id, comp := Pointed.hom.comp}, id_comp' := Pointed.large_category._proof_1, comp_id' := Pointed.large_category._proof_2, assoc' := Pointed.large_category._proof_3}
@[protected, instance]
Equations
- Pointed.concrete_category = category_theory.concrete_category.mk {obj := Pointed.X, map := Pointed.hom.to_fun, map_id' := Pointed.concrete_category._proof_1, map_comp' := Pointed.concrete_category._proof_2}
Constructs a isomorphism between pointed types from an equivalence that preserves the point between them.
@[simp]
option
as a functor from types to pointed types. This is the free functor.
@[simp]
theorem
Type_to_Pointed_map_to_fun
(X Y : Type u)
(f : X ⟶ Y)
(o : option X) :
(Type_to_Pointed.map f).to_fun o = option.map f o
Type_to_Pointed
is the free functor.
Equations
- Type_to_Pointed_forget_adjunction = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : Type u_1) (Y : Pointed), {to_fun := λ (f : Type_to_Pointed.obj X ⟶ Y), f.to_fun ∘ option.some, inv_fun := λ (f : X ⟶ (category_theory.forget Pointed).obj Y), {to_fun := λ (o : ↥(Type_to_Pointed.obj X)), option.elim Y.point f o, map_point := _}, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := Type_to_Pointed_forget_adjunction._proof_4, hom_equiv_naturality_right' := Type_to_Pointed_forget_adjunction._proof_5}