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
andY
isX × 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.
A restatement of types.lift_π_apply
that uses pi.π
and pi.lift
.
A restatement of types.map_π_apply
that uses pi.π
and pi.map
.
The category of types has punit
as a terminal object.
Equations
- category_theory.limits.types.terminal_limit_cone = {cone := {X := punit, π := {app := category_theory.limits.types.terminal_limit_cone._aux_1, naturality' := category_theory.limits.types.terminal_limit_cone._proof_1}}, is_limit := id {lift := category_theory.limits.types.terminal_limit_cone._aux_2, fac' := category_theory.limits.types.terminal_limit_cone._proof_3, uniq' := category_theory.limits.types.terminal_limit_cone._proof_4}}
The category of types has pempty
as an initial object.
Equations
- category_theory.limits.types.initial_limit_cone = {cocone := {X := pempty, ι := {app := category_theory.limits.types.initial_limit_cone._aux_1, naturality' := category_theory.limits.types.initial_limit_cone._proof_1}}, is_colimit := id {desc := category_theory.limits.types.initial_limit_cone._aux_2, fac' := category_theory.limits.types.initial_limit_cone._proof_3, uniq' := category_theory.limits.types.initial_limit_cone._proof_4}}
The product type X × Y
forms a cone for the binary product of X
and Y
.
The product type X × Y
is a binary product for X
and Y
.
Equations
- category_theory.limits.types.binary_product_limit X Y = {lift := λ (s : category_theory.limits.binary_fan X Y) (x : s.X), (s.fst x, s.snd x), fac' := _, uniq' := _}
The category of types has X × Y
, the usual cartesian product,
as the binary product of X
and Y
.
The functor which sends X, Y
to the product type X × Y
.
Equations
- category_theory.limits.types.binary_product_functor = {obj := λ (X : Type u), {obj := λ (Y : Type u), X × Y, map := λ (Y₁ Y₂ : Type u) (f : Y₁ ⟶ Y₂), (category_theory.limits.types.binary_product_limit X Y₂).lift (category_theory.limits.binary_fan.mk prod.fst (prod.snd ≫ f)), map_id' := _, map_comp' := _}, map := λ (X₁ X₂ : Type u) (f : X₁ ⟶ X₂), {app := λ (Y : Type u), (category_theory.limits.types.binary_product_limit X₂ Y).lift (category_theory.limits.binary_fan.mk (prod.fst ≫ f) prod.snd), naturality' := _}, map_id' := category_theory.limits.types.binary_product_functor._proof_8, map_comp' := category_theory.limits.types.binary_product_functor._proof_9}
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
- category_theory.limits.types.binary_product_iso_prod = category_theory.nat_iso.of_components (λ (X : Type u), category_theory.nat_iso.of_components (λ (Y : Type u), ((category_theory.limits.limit.is_limit (category_theory.limits.pair X Y)).cone_point_unique_up_to_iso (category_theory.limits.types.binary_product_limit X Y)).symm) _) category_theory.limits.types.binary_product_iso_prod._proof_6
The sum type X ⊕ Y
forms a cocone for the binary coproduct of X
and Y
.
The sum type X ⊕ Y
is a binary coproduct for X
and Y
.
Equations
- category_theory.limits.types.binary_coproduct_colimit X Y = {desc := λ (s : category_theory.limits.binary_cofan X Y), sum.elim s.inl s.inr, fac' := _, uniq' := _}
The category of types has X ⊕ Y
,
as the binary coproduct of X
and Y
.
The category of types has Π j, f j
as the product of a type family f : J → Type
.
Equations
- category_theory.limits.types.product_limit_cone F = {cone := {X := Π (j : J), F j, π := {app := λ (j : category_theory.discrete J) (f : ((category_theory.functor.const (category_theory.discrete J)).obj (Π (j : J), F j)).obj j), f j, naturality' := _}}, is_limit := {lift := λ (s : category_theory.limits.cone (category_theory.discrete.functor F)) (x : s.X) (j : 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.coproduct_colimit_cocone F = {cocone := {X := Σ (j : J), F j, ι := {app := λ (j : category_theory.discrete J) (x : (category_theory.discrete.functor F).obj j), ⟨j, x⟩, naturality' := _}}, is_colimit := {desc := λ (s : category_theory.limits.cocone (category_theory.discrete.functor F)) (x : {X := Σ (j : J), F j, ι := {app := λ (j : category_theory.discrete J) (x : (category_theory.discrete.functor F).obj j), ⟨j, x⟩, naturality' := _}}.X), s.ι.app x.fst x.snd, fac' := _, uniq' := _}}
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
- category_theory.limits.types.type_equalizer_of_unique f w t = category_theory.limits.fork.is_limit.mk' (category_theory.limits.fork.of_ι f w) (λ (s : category_theory.limits.fork g h), ⟨λ (i : ((category_theory.functor.const category_theory.limits.walking_parallel_pair).obj s.X).obj category_theory.limits.walking_parallel_pair.zero), classical.some _, _⟩)
The converse of type_equalizer_of_unique
.
Show that the subtype {x : Y // g x = h x}
is an equalizer for the pair (g,h)
.
Equations
- category_theory.limits.types.equalizer_limit = {cone := category_theory.limits.fork.of_ι subtype.val category_theory.limits.types.equalizer_limit._proof_1, is_limit := category_theory.limits.fork.is_limit.mk' (category_theory.limits.fork.of_ι subtype.val category_theory.limits.types.equalizer_limit._proof_1) (λ (s : category_theory.limits.fork g h), ⟨λ (i : ((category_theory.functor.const category_theory.limits.walking_parallel_pair).obj s.X).obj category_theory.limits.walking_parallel_pair.zero), ⟨s.ι i, _⟩, _⟩)}