# The category of bipointed types #

This defines `Bipointed`

, the category of bipointed types.

## TODO #

Monoidal structure

## Equations

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

Turns a bipointing into a bipointed type.

## Equations

- Bipointed.of to_prod = { X := X, toProd := to_prod }

## Instances For

@[simp]

## Equations

- Bipointed.instInhabited = { default := Bipointed.of ((), ()) }

theorem
Bipointed.Hom.map_fst
{X : Bipointed}
{Y : Bipointed}
(self : X.Hom Y)
:

self.toFun X.toProd.1 = Y.toProd.1

theorem
Bipointed.Hom.map_snd
{X : Bipointed}
{Y : Bipointed}
(self : X.Hom Y)
:

self.toFun X.toProd.2 = Y.toProd.2

@[simp]

The identity morphism of `X : Bipointed`

.

## Equations

- Bipointed.Hom.id X = { toFun := id, map_fst := ⋯, map_snd := ⋯ }

## Instances For

## Equations

- Bipointed.Hom.instInhabited X = { default := Bipointed.Hom.id X }

## Equations

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

@[simp]

theorem
Bipointed.swap_map_toFun :

∀ {X Y : Bipointed} (f : X ⟶ Y) (a : X.X), (Bipointed.swap.map f).toFun a = f.toFun a

@[simp]

Swaps the pointed elements of a bipointed type. `Prod.swap`

as a functor.

## Equations

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

## Instances For

@[simp]

theorem
Bipointed.swapEquiv_inverse_obj_X
(X : Bipointed)
:

(Bipointed.swapEquiv.inverse.obj X).X = X.X

@[simp]

theorem
Bipointed.swapEquiv_functor_obj_toProd
(X : Bipointed)
:

(Bipointed.swapEquiv.functor.obj X).toProd = X.toProd.swap

@[simp]

theorem
Bipointed.swapEquiv_inverse_map_toFun :

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

@[simp]

theorem
Bipointed.swapEquiv_functor_map_toFun :

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

@[simp]

theorem
Bipointed.swapEquiv_unitIso_hom_app_toFun
(X : Bipointed)
:

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

@[simp]

theorem
Bipointed.swapEquiv_counitIso_hom_app_toFun
(X : Bipointed)
(a : ((Bipointed.swap.comp Bipointed.swap).obj X).X)
:

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

@[simp]

theorem
Bipointed.swapEquiv_functor_obj_X
(X : Bipointed)
:

(Bipointed.swapEquiv.functor.obj X).X = X.X

@[simp]

theorem
Bipointed.swapEquiv_unitIso_inv_app_toFun
(X : Bipointed)
:

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

@[simp]

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

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

@[simp]

theorem
Bipointed.swapEquiv_inverse_obj_toProd
(X : Bipointed)
:

(Bipointed.swapEquiv.inverse.obj X).toProd = X.toProd.swap

@[simp]

@[simp]

@[simp]

@[simp]

@[simp]

@[simp]

@[simp]

theorem
pointedToBipointedCompBipointedToPointedFst_inv_app_toFun
(X : Pointed)
(a : ((CategoryTheory.Functor.id Pointed).obj X).X)
:

(pointedToBipointedCompBipointedToPointedFst.inv.app X).toFun a = a

@[simp]

theorem
pointedToBipointedCompBipointedToPointedFst_hom_app_toFun
(X : Pointed)
(a : ((pointedToBipointed.comp bipointedToPointedFst).obj X).X)
:

(pointedToBipointedCompBipointedToPointedFst.hom.app X).toFun a = a

`BipointedToPointed_fst`

is inverse to `PointedToBipointed`

.

## Equations

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

## Instances For

@[simp]

theorem
pointedToBipointedCompBipointedToPointedSnd_hom_app_toFun
(X : Pointed)
(a : ((pointedToBipointed.comp bipointedToPointedSnd).obj X).X)
:

(pointedToBipointedCompBipointedToPointedSnd.hom.app X).toFun a = a

@[simp]

theorem
pointedToBipointedCompBipointedToPointedSnd_inv_app_toFun
(X : Pointed)
(a : ((CategoryTheory.Functor.id Pointed).obj X).X)
:

(pointedToBipointedCompBipointedToPointedSnd.inv.app X).toFun a = a

`BipointedToPointed_snd`

is inverse to `PointedToBipointed`

.

## Equations

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

## Instances For

The free/forgetful adjunction between `PointedToBipointed_fst`

and `BipointedToPointed_fst`

.

## Equations

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

## Instances For

The free/forgetful adjunction between `PointedToBipointed_snd`

and `BipointedToPointed_snd`

.

## Equations

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