# The category of two-pointed types #

This defines `TwoP`

, the category of two-pointed types.

## References #

- [nLab,
*coalgebra of the real interval*] (https://ncatlab.org/nlab/show/coalgebra+of+the+real+interval)

The category of two-pointed types.

- X : Type u
The underlying type of a two-pointed type.

- toTwoPointing : TwoPointing self.X
The two points of a bipointed type, bundled together as a pair of distinct elements.

## Instances For

## Equations

- TwoP.instCoeSortType = { coe := TwoP.X }

@[simp]

## Equations

- TwoP.instInhabited = { default := TwoP.of TwoPointing.bool }

Turns a two-pointed type into a bipointed type, by forgetting that the pointed elements are distinct.

## Equations

- X.toBipointed = X.toTwoPointing.Bipointed

## Instances For

@[simp]

Swaps the pointed elements of a two-pointed type. `TwoPointing.swap`

as a functor.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

@[simp]

theorem
TwoP.swapEquiv_inverse_map_toFun :

∀ {X Y : TwoP} (f : X ⟶ Y) (a : X.toBipointed.X), (TwoP.swapEquiv.inverse.map f).toFun a = f.toFun a

@[simp]

theorem
TwoP.swapEquiv_functor_obj_toTwoPointing_toProd
(X : TwoP)
:

(TwoP.swapEquiv.functor.obj X).toTwoPointing.toProd = (X.toTwoPointing.toProd.2, X.toTwoPointing.toProd.1)

@[simp]

theorem
TwoP.swapEquiv_inverse_obj_toTwoPointing_toProd
(X : TwoP)
:

(TwoP.swapEquiv.inverse.obj X).toTwoPointing.toProd = (X.toTwoPointing.toProd.2, X.toTwoPointing.toProd.1)

@[simp]

@[simp]

theorem
TwoP.swapEquiv_counitIso_hom_app_toFun
(X : TwoP)
(a : ((TwoP.swap.comp TwoP.swap).obj X).toBipointed.X)
:

(TwoP.swapEquiv.counitIso.hom.app X).toFun a = a

@[simp]

theorem
TwoP.swapEquiv_unitIso_inv_app_toFun
(X : TwoP)
:

∀ (a : ((TwoP.swap.comp TwoP.swap).obj X).toBipointed.X),
(TwoP.swapEquiv.unitIso.inv.app X).toFun a = (CategoryTheory.CategoryStruct.comp (TwoP.swap.map (TwoP.swap.map { toFun := id, map_fst := ⋯, map_snd := ⋯ }))
(CategoryTheory.CategoryStruct.comp (TwoP.swap.map { toFun := id, map_fst := ⋯, map_snd := ⋯ })
{ toFun := id, map_fst := ⋯, map_snd := ⋯ })).toFun
((CategoryTheory.CategoryStruct.id (TwoP.swap.obj (TwoP.swap.obj X))).toFun a)

@[simp]

theorem
TwoP.swapEquiv_unitIso_hom_app_toFun
(X : TwoP)
:

∀ (a : ((CategoryTheory.Functor.id TwoP).obj X).toBipointed.X),
(TwoP.swapEquiv.unitIso.hom.app X).toFun a = (CategoryTheory.CategoryStruct.id (TwoP.swap.obj (TwoP.swap.obj X))).toFun
((CategoryTheory.CategoryStruct.comp { toFun := id, map_fst := ⋯, map_snd := ⋯ }
(CategoryTheory.CategoryStruct.comp (TwoP.swap.map { toFun := id, map_fst := ⋯, map_snd := ⋯ })
(TwoP.swap.map (TwoP.swap.map { toFun := id, map_fst := ⋯, map_snd := ⋯ })))).toFun
a)

@[simp]

theorem
TwoP.swapEquiv_counitIso_inv_app_toFun
(X : TwoP)
(a : ((CategoryTheory.Functor.id TwoP).obj X).toBipointed.X)
:

(TwoP.swapEquiv.counitIso.inv.app X).toFun a = a

@[simp]

@[simp]

theorem
TwoP.swapEquiv_functor_map_toFun :

∀ {X Y : TwoP} (f : X ⟶ Y) (a : X.toBipointed.X), (TwoP.swapEquiv.functor.map f).toFun a = f.toFun a

@[simp]

@[simp]

theorem
pointedToTwoPFst_obj_toTwoPointing_toProd
(X : Pointed)
:

(pointedToTwoPFst.obj X).toTwoPointing.toProd = (some X.point, none)

@[simp]

theorem
pointedToTwoPFst_map_toFun :

∀ {X Y : Pointed} (f : X ⟶ Y) (a : Option X.X), (pointedToTwoPFst.map f).toFun a = Option.map f.toFun a

@[simp]

theorem
pointedToTwoPSnd_obj_toTwoPointing_toProd
(X : Pointed)
:

(pointedToTwoPSnd.obj X).toTwoPointing.toProd = (none, some X.point)

@[simp]

theorem
pointedToTwoPSnd_map_toFun :

∀ {X Y : Pointed} (f : X ⟶ Y) (a : Option X.X), (pointedToTwoPSnd.map f).toFun a = Option.map f.toFun a

@[simp]

@[simp]

@[simp]

@[simp]

Adding a second point is left adjoint to forgetting the second point.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Adding a first point is left adjoint to forgetting the first point.

## Equations

- One or more equations did not get rendered due to their size.