The category of bipointed types #
This defines Bipointed
, the category of bipointed types.
TODO #
Monoidal structure
The category of bipointed types.
Instances for Bipointed
Equations
Turns a bipointing into a bipointed type.
Equations
- Bipointed.of to_prod = {X := X, to_prod := to_prod}
Equations
- Bipointed.inhabited = {default := Bipointed.of ((), ())}
Equations
Equations
- Bipointed.large_category = {to_category_struct := {to_quiver := {hom := Bipointed.hom}, id := Bipointed.hom.id, comp := Bipointed.hom.comp}, id_comp' := Bipointed.large_category._proof_1, comp_id' := Bipointed.large_category._proof_2, assoc' := Bipointed.large_category._proof_3}
Equations
- Bipointed.concrete_category = category_theory.concrete_category.mk {obj := Bipointed.X, map := Bipointed.hom.to_fun, map_id' := Bipointed.concrete_category._proof_1, map_comp' := Bipointed.concrete_category._proof_2}
Swaps the pointed elements of a bipointed type. prod.swap
as a functor.
The equivalence between Bipointed
and itself induced by prod.swap
both ways.
Equations
- Bipointed.swap_equiv = category_theory.equivalence.mk Bipointed.swap Bipointed.swap (category_theory.nat_iso.of_components (λ (X : Bipointed), {hom := {to_fun := id ↥((𝟭 Bipointed).obj X), map_fst := _, map_snd := _}, inv := {to_fun := id ↥((Bipointed.swap ⋙ Bipointed.swap).obj X), map_fst := _, map_snd := _}, hom_inv_id' := _, inv_hom_id' := _}) Bipointed.swap_equiv._proof_7) (category_theory.nat_iso.of_components (λ (X : Bipointed), {hom := {to_fun := id ↥((Bipointed.swap ⋙ Bipointed.swap).obj X), map_fst := _, map_snd := _}, inv := {to_fun := id ↥((𝟭 Bipointed).obj X), map_fst := _, map_snd := _}, hom_inv_id' := _, inv_hom_id' := _}) Bipointed.swap_equiv._proof_14)
The functor from Pointed
to Bipointed
which adds a second point.
Equations
- Pointed_to_Bipointed_fst = {obj := λ (X : Pointed), {X := option ↥X, to_prod := (↑(X.point), option.none ↥X)}, map := λ (X Y : Pointed) (f : X ⟶ Y), {to_fun := option.map f.to_fun, map_fst := _, map_snd := _}, map_id' := Pointed_to_Bipointed_fst._proof_3, map_comp' := Pointed_to_Bipointed_fst._proof_4}
The functor from Pointed
to Bipointed
which adds a first point.
Equations
- Pointed_to_Bipointed_snd = {obj := λ (X : Pointed), {X := option ↥X, to_prod := (option.none ↥X, ↑(X.point))}, map := λ (X Y : Pointed) (f : X ⟶ Y), {to_fun := option.map f.to_fun, map_fst := _, map_snd := _}, map_id' := Pointed_to_Bipointed_snd._proof_3, map_comp' := Pointed_to_Bipointed_snd._proof_4}
Bipointed_to_Pointed_fst
is inverse to Pointed_to_Bipointed
.
Equations
- Pointed_to_Bipointed_comp_Bipointed_to_Pointed_fst = category_theory.nat_iso.of_components (λ (X : Pointed), {hom := {to_fun := id ↥((Pointed_to_Bipointed ⋙ Bipointed_to_Pointed_fst).obj X), map_point := _}, inv := {to_fun := id ↥((𝟭 Pointed).obj X), map_point := _}, hom_inv_id' := _, inv_hom_id' := _}) Pointed_to_Bipointed_comp_Bipointed_to_Pointed_fst._proof_5
Bipointed_to_Pointed_snd
is inverse to Pointed_to_Bipointed
.
Equations
- Pointed_to_Bipointed_comp_Bipointed_to_Pointed_snd = category_theory.nat_iso.of_components (λ (X : Pointed), {hom := {to_fun := id ↥((Pointed_to_Bipointed ⋙ Bipointed_to_Pointed_snd).obj X), map_point := _}, inv := {to_fun := id ↥((𝟭 Pointed).obj X), map_point := _}, hom_inv_id' := _, inv_hom_id' := _}) Pointed_to_Bipointed_comp_Bipointed_to_Pointed_snd._proof_5
The free/forgetful adjunction between Pointed_to_Bipointed_fst
and Bipointed_to_Pointed_fst
.
Equations
- Pointed_to_Bipointed_fst_Bipointed_to_Pointed_fst_adjunction = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : Pointed) (Y : Bipointed), {to_fun := λ (f : Pointed_to_Bipointed_fst.obj X ⟶ Y), {to_fun := f.to_fun ∘ option.some, map_point := _}, inv_fun := λ (f : X ⟶ Bipointed_to_Pointed_fst.obj Y), {to_fun := λ (o : ↥(Pointed_to_Bipointed_fst.obj X)), option.elim Y.to_prod.snd f.to_fun o, map_fst := _, map_snd := _}, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := Pointed_to_Bipointed_fst_Bipointed_to_Pointed_fst_adjunction._proof_6, hom_equiv_naturality_right' := Pointed_to_Bipointed_fst_Bipointed_to_Pointed_fst_adjunction._proof_7}
The free/forgetful adjunction between Pointed_to_Bipointed_snd
and Bipointed_to_Pointed_snd
.
Equations
- Pointed_to_Bipointed_snd_Bipointed_to_Pointed_snd_adjunction = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : Pointed) (Y : Bipointed), {to_fun := λ (f : Pointed_to_Bipointed_snd.obj X ⟶ Y), {to_fun := f.to_fun ∘ option.some, map_point := _}, inv_fun := λ (f : X ⟶ Bipointed_to_Pointed_snd.obj Y), {to_fun := λ (o : ↥(Pointed_to_Bipointed_snd.obj X)), option.elim Y.to_prod.fst f.to_fun o, map_fst := _, map_snd := _}, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := Pointed_to_Bipointed_snd_Bipointed_to_Pointed_snd_adjunction._proof_6, hom_equiv_naturality_right' := Pointed_to_Bipointed_snd_Bipointed_to_Pointed_snd_adjunction._proof_7}