The doubling is the square

The doubling of a category is its product with itself: an object is a pair and a morphism is a pair. Essential smallness follows.

def RS.doubledProdFunctor {A : Type u} [CategoryTheory.Category.{v, u} A] : CategoryTheory.Functor (Doubled A) (A × A)

The doubling, as the product category.

Equations

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

def RS.prodDoubledFunctor {A : Type u} [CategoryTheory.Category.{v, u} A] : CategoryTheory.Functor (A × A) (Doubled A)

The product category, as the doubling.

Equations

• RS.prodDoubledFunctor = { obj := fun (X : A × A) => { even := X.1, odd := X.2 }, map := fun {X Y : A × A} (f : X ⟶ Y) => { even := f.1, odd := f.2 }, map_id := ⋯, map_comp := ⋯ }

def RS.doubledProdEquiv {A : Type u} [CategoryTheory.Category.{v, u} A] : Doubled A ≌ A × A

The doubling is the square of the category.

Equations

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