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?)

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.

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`

.

this holds because under an inconsistent context everything does.

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!

Joshua Grosso has marked this topic as resolved.

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: Feb 05 2023 at 07:03 UTC