## Stream: Is there code for X?

### Topic: category of sets

#### Utensil Song (Aug 15 2020 at 12:36):

It seems that there're no category of sets in mathlib?

I've made a #mwe (with a random proof as POC) but don't know if it's idiomatic or correct:

import init.function
import category_theory.category
import category_theory.full_subcategory
import algebra.category.Group

universes u v

open category_theory

variables (X : Type u)

instance Set.category : category (set X) :=
{ hom  := λ A B, A → B,
id   := λ S s, s,
comp :=  λ _ _ _ f g, g ∘ f }

lemma Set.injective_of_mono {A B : set X} (f : A ⟶ B) [mono f] : function.injective f :=
begin
assume a₁ a₂ h,
let α₁ : A → A := λ _, a₁,
let α₂ : A → A := λ _, a₂,
let hom_α₁ := as_hom α₁,
let hom_α₂ := as_hom α₂,
have t0 : hom_α₁ ≫ f = hom_α₂ ≫ f :=
begin
ext x',
cases x',
cases a₁,
cases a₂,
dsimp at *,
solve_by_elim,
end,
have t1 : hom_α₁ = hom_α₂ := (cancel_mono f).mp t0,
have t2 : α₁ = α₂ := by assumption,
have t3 : α₁ a₁ = α₂ a₁ := by rw t2,
have t4 : α₁ a₁ = a₁ := rfl,
have t5 : α₂ a₁ = a₂ := rfl,
assumption,
end


#### Utensil Song (Aug 15 2020 at 12:38):

I noticed docs#category_theory.bundled and docs#category_theory.induced_category and this topic but don't know how to apply them to a non-class set.

#### Markus Himmel (Aug 15 2020 at 12:39):

What mathematicians would call the category of sets is called the category of types in mathlib: docs#category_theory.types

#### Scott Morrison (Aug 15 2020 at 12:39):

I guess no one has noticed a use for it so far. (Of course we use the category of types a lot.)

#### Markus Himmel (Aug 15 2020 at 12:40):

Are you looking for the category of sets as in your wikipedia link or for the category of sets of a type X as in your code sample?

#### Utensil Song (Aug 15 2020 at 12:44):

Markus Himmel said:

Are you looking for the category of sets as in your wikipedia link or for the category of sets of a type X as in your code sample?

The code example is born out of the difficulty of expressing the "the category of sets " properly, I think.

#### Scott Morrison (Aug 15 2020 at 12:44):

But @Utensil Song, I think the point is that as we're using different foundations, the category of sets is not particularly interesting or useful, and everywhere that conventional mathematics uses their "category of sets" (in set theory), we want to use the "category of types" (in type theory).

#### Scott Morrison (Aug 15 2020 at 12:45):

The category of sets (in type theory) (i.e. the thing you just defined) is not the same thing as the category of sets (in set theory).

#### Adam Topaz (Aug 15 2020 at 12:47):

Perhaps worth mentioning: the category of subsets of X, as defined in the code above, can be constructed as a full subcategory of the category of types. Full subcategories exists already in mathlib, if you really need this.

#### Utensil Song (Aug 15 2020 at 12:57):

Scott Morrison said:

But Utensil Song, I think the point is that as we're using different foundations, the category of sets is not particularly interesting or useful, and everywhere that conventional mathematics uses their "category of sets" (in set theory), we want to use the "category of types" (in type theory).

Thanks for the clarification, now I realized it. I was having trouble treating types as sets and sets as subsets lately due to some discussions on Zulip.

Thanks for the pointers to docs#category_theory.types and docs#category_theory.​full_subcategory , they seem to be what I'm looking for (fail to recognize them previously).

#### Kenny Lau (Aug 15 2020 at 12:58):

we do have a category structure on set X owing to its complete lattice structure

#### Utensil Song (Aug 15 2020 at 13:02):

has_limits_of_complete_lattice ?

#### Kenny Lau (Aug 15 2020 at 13:02):

that’s saying it has all limits right

#### Kenny Lau (Aug 15 2020 at 13:03):

you can try #check (by apply_instance : category (set X)) if you want to find the name

#### Kenny Lau (Aug 15 2020 at 13:03):

ofc with variable (X : Type*) on the previous line

#### Utensil Song (Aug 15 2020 at 13:09):

preorder.small_category (set X)

#### Adam Topaz (Aug 15 2020 at 13:19):

Note that the preorder category structure on set X is different from what was defined above. The limits in this are essentially just Inf and colimits essentially just Sup.

Last updated: May 16 2021 at 05:21 UTC