## Stream: Miscellaneous

### Topic: ✔ Initial objects in Coq?

#### Joshua Grosso (Sep 18 2021 at 00:06):

I'm trying to teach myself category theory (from Basic Category Theory for Computer Scientists), and I'm confused by an example for an initial object. Specifically: "In Set, the empty set {} is the only initial object; for every set S, the empty function is the unique function from {} to S" (page 16).
Is this equivalent to a function in Coq of type (say, with S = `nat`) `False -> nat`? If so, isn't there more than one such function (e.g. `fun _ => 1` and `fun _ => 2`)? (I recognize that I'm pretending that Coq functions are functions on sets—is that perhaps where the issue comes from?)

#### Pierre-Marie Pédrot (Sep 18 2021 at 01:04):

Up to funext, you can prove that those two functions are equal. Obviously funext does not hold in vanilla CIC, but it's taken for granted in CT.

#### Pierre-Marie Pédrot (Sep 18 2021 at 01:05):

If you want to expand it setoid style, you can still prove that `forall f g : False -> nat, forall e : False, f e = g e`.

#### Pierre-Marie Pédrot (Sep 18 2021 at 01:05):

this holds because under an inconsistent context everything does.

#### Joshua Grosso (Sep 18 2021 at 01:24):

Oops, I totally should've realized that—I even tried functional extensionality, but I just forgot to destruct the introduced parameter :-P Thank you for the help!

#### Notification Bot (Sep 18 2021 at 01:24):

Joshua Grosso has marked this topic as resolved.

#### Paolo Giarrusso (Sep 18 2021 at 04:19):

FWIW beyond the above, in ZFC the function from `{}` is unique _because_ functions are their graphs — just sets of ordered pairs of inputs and outputs. So funext follows as a theorem: function equality is extensional _because functions don't have intensions_. (But I doubt this distinction matters much in CT).

Last updated: May 31 2023 at 02:31 UTC