# mathlibdocumentation

category_theory.limits.shapes.types

# Special shapes for limits in Type.

The general shape (co)limits defined in category_theory.limits.types are intended for use through the limits API, and the actual implementation should mostly be considered "sealed".

In this file, we provide definitions of the "standard" special shapes of limits in Type, giving the expected definitional implementation:

• the terminal object is punit
• the binary product of X and Y is X × Y
• the product of a family f : J → Type is Π j, f j.

Because these are not intended for use with the has_limit API, we instead construct terms of limit_data.

As an example, when setting up the monoidal category structure on Type we use the types_has_terminal and types_has_binary_products instances.

@[simp]
theorem category_theory.limits.types.pi_lift_π_apply {β : Type u} (f : β → Type u) {P : Type u} (s : Π (b : β), P f b) (b : β) (x : P) :
= s b x

A restatement of types.lift_π_apply that uses pi.π and pi.lift.

@[simp]
theorem category_theory.limits.types.pi_map_π_apply {β : Type u} {f g : β → Type u} (α : Π (j : β), f j g j) (b : β) (x : λ (j : β), f j) :
= α b x)

A restatement of types.map_π_apply that uses pi.π and pi.map.

The category of types has punit as a terminal object.

Equations

The category of types has pempty as an initial object.

Equations

The product type X × Y forms a cone for the binary product of X and Y.

Equations
@[simp]
theorem category_theory.limits.types.binary_product_cone_X (X Y : Type u) :
= (X × Y)

@[simp]
theorem category_theory.limits.types.binary_product_limit_lift (X Y : Type u) (x : s.X) :
= (s.fst x, s.snd x)

The product type X × Y is a binary product for X and Y.

Equations

The category of types has X × Y, the usual cartesian product, as the binary product of X and Y.

Equations
@[simp]

@[simp]

The functor which sends X, Y to the product type X × Y.

Equations
@[simp]
theorem category_theory.limits.types.binary_product_functor_map_app (X₁ X₂ : Type u) (f : X₁ X₂) (Y : Type u) :

@[simp]
theorem category_theory.limits.types.binary_product_functor_obj_map (X Y₁ Y₂ : Type u) (f : Y₁ Y₂) :

The product functor given by the instance has_binary_products (Type u) is isomorphic to the explicit binary product functor given by the product type.

Equations

The sum type X ⊕ Y forms a cocone for the binary coproduct of X and Y.

Equations
@[simp]
theorem category_theory.limits.types.binary_coproduct_cocone_ι_app (X Y : Type u) (ᾰ : j) :
= category_theory.limits.walking_pair.rec sum.inl sum.inr j

The sum type X ⊕ Y is a binary coproduct for X and Y.

Equations
@[simp]
theorem category_theory.limits.types.binary_coproduct_colimit_desc (X Y : Type u) (ᾰ : X Y) :
= s.inr

The category of types has X ⊕ Y, as the binary coproduct of X and Y.

Equations
def category_theory.limits.types.product_limit_cone {J : Type u} (F : J → Type u) :

The category of types has Π j, f j as the product of a type family f : J → Type.

Equations
def category_theory.limits.types.coproduct_colimit_cocone {J : Type u} (F : J → Type u) :

The category of types has Σ j, f j as the coproduct of a type family f : J → Type.

Equations
def category_theory.limits.types.type_equalizer_of_unique {X Y Z : Type u} (f : X Y) {g h : Y Z} (w : f g = f h) (t : ∀ (y : Y), g y = h y(∃! (x : X), f x = y)) :

Show the given fork in Type u is an equalizer given that any element in the "difference kernel" comes from X. The converse of unique_of_type_equalizer.

Equations
theorem category_theory.limits.types.unique_of_type_equalizer {X Y Z : Type u} (f : X Y) {g h : Y Z} (w : f g = f h) (y : Y) (hy : g y = h y) :
∃! (x : X), f x = y

The converse of type_equalizer_of_unique.

theorem category_theory.limits.types.type_equalizer_iff_unique {X Y Z : Type u} (f : X Y) {g h : Y Z} (w : f g = f h) :
∀ (y : Y), g y = h y(∃! (x : X), f x = y)

def category_theory.limits.types.equalizer_limit {Y Z : Type u} {g h : Y Z} :

Show that the subtype {x : Y // g x = h x} is an equalizer for the pair (g,h).

Equations