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
Equations
- Bipointed.instInhabited = { default := Bipointed.of ((), ()) }
The identity morphism of X : Bipointed
.
Equations
- Bipointed.Hom.id X = { toFun := id, map_fst := ⋯, map_snd := ⋯ }
Instances For
@[simp]
Equations
- Bipointed.hasForget = CategoryTheory.HasForget.mk { obj := Bipointed.X, map := @Bipointed.Hom.toFun, map_id := Bipointed.hasForget.proof_1, map_comp := @Bipointed.hasForget.proof_2 }
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
BipointedToPointed_fst
is inverse to PointedToBipointed
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.