Joshua Grosso (Sep 18 2021 at 00:06): 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: Oct 13 2024 at 01:02 UTC