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
XandYisX × Y - the product of a family
f : J → TypeisΠ j, f j.
It is not intended that these definitions will be global instances: they should be turned on as needed.
As an example, when setting up the monoidal category structure on Type
we use the types_has_terminal and types_has_binary_products instances.
def
category_theory.limits.types.types_has_terminal
:
category_theory.limits.has_terminal (Type u)
The category of types has punit as a terminal object.
Equations
- category_theory.limits.types.types_has_terminal = {has_limit := λ (F : category_theory.discrete pempty ⥤ Type u), {cone := {X := punit, π := {app := category_theory.limits.types.types_has_terminal._aux_1 F, naturality' := _}}, is_limit := id (λ (F : category_theory.discrete pempty ⥤ Type u), {lift := category_theory.limits.types.types_has_terminal._aux_2 F, fac' := _, uniq' := _}) F}}
The category of types has pempty as an initial object.
Equations
- category_theory.limits.types.types_has_initial = {has_colimit := λ (F : category_theory.discrete pempty ⥤ Type u), {cocone := {X := pempty, ι := {app := category_theory.limits.types.types_has_initial._aux_1 F, naturality' := _}}, is_colimit := id (λ (F : category_theory.discrete pempty ⥤ Type u), {desc := category_theory.limits.types.types_has_initial._aux_2 F, fac' := _, uniq' := _}) F}}
The category of types has X × Y, the usual cartesian product,
as the binary product of X and Y.
Equations
- category_theory.limits.types.types_has_binary_products = {has_limit := λ (F : category_theory.discrete category_theory.limits.walking_pair ⥤ Type u), {cone := {X := F.obj category_theory.limits.walking_pair.left × F.obj category_theory.limits.walking_pair.right, π := {app := λ (X : category_theory.discrete category_theory.limits.walking_pair), category_theory.limits.walking_pair.cases_on X prod.fst prod.snd, naturality' := _}}, is_limit := {lift := λ (s : category_theory.limits.cone F) (x : s.X), (s.π.app category_theory.limits.walking_pair.left x, s.π.app category_theory.limits.walking_pair.right x), fac' := _, uniq' := _}}}
The category of types has X ⊕ Y,
as the binary coproduct of X and Y.
Equations
- category_theory.limits.types.types_has_binary_coproducts = {has_colimit := λ (F : category_theory.discrete category_theory.limits.walking_pair ⥤ Type u), {cocone := {X := F.obj category_theory.limits.walking_pair.left ⊕ F.obj category_theory.limits.walking_pair.right, ι := {app := λ (X : category_theory.discrete category_theory.limits.walking_pair), category_theory.limits.walking_pair.cases_on X sum.inl sum.inr, naturality' := _}}, is_colimit := {desc := λ (s : category_theory.limits.cocone F) (x : {X := F.obj category_theory.limits.walking_pair.left ⊕ F.obj category_theory.limits.walking_pair.right, ι := {app := λ (X : category_theory.discrete category_theory.limits.walking_pair), category_theory.limits.walking_pair.cases_on X sum.inl sum.inr, naturality' := _}}.X), sum.elim (s.ι.app category_theory.limits.walking_pair.left) (s.ι.app category_theory.limits.walking_pair.right) x, fac' := _, uniq' := _}}}
def
category_theory.limits.types.types_has_products
:
category_theory.limits.has_products (Type u)
The category of types has Π j, f j as the product of a type family f : J → Type.
Equations
- category_theory.limits.types.types_has_products = λ (J : Type u), {has_limit := λ (F : category_theory.discrete J ⥤ Type u), {cone := {X := Π (j : category_theory.discrete J), F.obj j, π := {app := λ (j : category_theory.discrete J) (f : ((category_theory.functor.const (category_theory.discrete J)).obj (Π (j : category_theory.discrete J), F.obj j)).obj j), f j, naturality' := _}}, is_limit := {lift := λ (s : category_theory.limits.cone F) (x : s.X) (j : category_theory.discrete J), s.π.app j x, fac' := _, uniq' := _}}}
The category of types has Σ j, f j as the coproduct of a type family f : J → Type.
Equations
- category_theory.limits.types.types_has_coproducts = λ (J : Type u), {has_colimit := λ (F : category_theory.discrete J ⥤ Type u), {cocone := {X := Σ (j : category_theory.discrete J), F.obj j, ι := {app := λ (j : category_theory.discrete J) (x : F.obj j), ⟨j, x⟩, naturality' := _}}, is_colimit := {desc := λ (s : category_theory.limits.cocone F) (x : {X := Σ (j : category_theory.discrete J), F.obj j, ι := {app := λ (j : category_theory.discrete J) (x : F.obj j), ⟨j, x⟩, naturality' := _}}.X), s.ι.app x.fst x.snd, fac' := _, uniq' := _}}}
theorem
category_theory.limits.types.terminal_from
{P : Type u}
(f : P ⟶ ⊤_Type u)
(p : P) :
f p = punit.star
@[simp]
@[simp]
@[simp]
theorem
category_theory.limits.types.prod_lift
{X Y Z : Type u}
{f : X ⟶ Y}
{g : X ⟶ Z} :
category_theory.limits.prod.lift f g = λ (x : X), (f x, g x)
@[simp]
theorem
category_theory.limits.types.prod_map
{W X Y Z : Type u}
{f : W ⟶ X}
{g : Y ⟶ Z} :
category_theory.limits.prod.map f g = λ (p : W × Y), (f p.fst, g p.snd)
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
category_theory.limits.types.pi_π
{J : Type u}
{f : J → Type u}
(j : J)
(g : ∏ f) :
category_theory.limits.pi.π f j g = g j
@[simp]
theorem
category_theory.limits.types.pi_lift
{J : Type u}
{f : J → Type u}
{W : Type u}
{g : Π (j : J), W ⟶ f j} :
category_theory.limits.pi.lift g = λ (w : W) (j : J), g j w
@[simp]
theorem
category_theory.limits.types.pi_map
{J : Type u}
{f g : J → Type u}
{h : Π (j : J), f j ⟶ g j} :
category_theory.limits.pi.map h = λ (k : Π (j : J), f j) (j : category_theory.discrete J), h j (k j)
@[simp]
@[simp]
theorem
category_theory.limits.types.sigma_ι
{J : Type u}
{f : J → Type u}
(j : J)
(x : f j) :
category_theory.limits.sigma.ι f j x = ⟨j, x⟩
@[simp]
theorem
category_theory.limits.types.sigma_desc
{J : Type u}
{f : J → Type u}
{W : Type u}
{g : Π (j : J), f j ⟶ W}
{p : Σ (j : J), f j} :
category_theory.limits.sigma.desc g p = g p.fst p.snd
@[simp]
theorem
category_theory.limits.types.sigma_map
{J : Type u}
{f g : J → Type u}
{h : Π (j : J), f j ⟶ g j} :