Describe coproducts in Sets

Stream: new members

[Noah Anderson]

How can I say that "disjoint union" is coproduct in the category of Sets?
(or the coproduct in the category of Sets is disjoint union

[Noah Anderson]

Do we have "category of sets" in mathlib? and is it possible to prove such thinig via simply verifying its universal property etc.?

[Noah Anderson]

Should it be something like this?

/-
Describe coproducts in Sets.
-/

open CategoryTheory Limits

universe u

structure Sets : Type (u + 1) where
  (carrier : Type u)
  [str : Set carrier]

structure Sets.Hom (A B : Sets.{u}) where
  private mk ::
  hom' : A.str → B.str

instance : Category Sets.{u} where
  Hom X Y := Sets.Hom X Y
  id X := ⟨id⟩
  comp f g := ⟨g.hom'.comp f.hom'⟩

variable (X Y : Sets.{u})

abbrev Z : Sets.{u} := {
  carrier := X.carrier ⊕ Y.carrier
  str := Set.univ
}

example (X Y : Sets) : HasBinaryCoproduct X Y := by
  sorry

[Aaron Liu]

In mathlib we have the category of types

[Aaron Liu]

This looks like it should be an equivalent category

[Aaron Liu]

But your coproduct is wrong

[Johan Commelin]

@Noah Anderson You can just work with Type u directly. Your current Sets has objects of the form $\text{str} \subseteq \text{carrier}$, but then you ignore the carrier when defining homs.

[Kevin Buzzard]

Lean uses type theory not set theory, and the type plays the role of a set here.

[Noah Anderson]

I see... so it would be CategoryTheory.Limits.Types.binaryCoproductIso I imagine, thanks!