Stream: Miscellaneous

Topic: ✔ Initial objects in Coq?


view this post on Zulip 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?)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Sep 18 2021 at 01:05):

this holds because under an inconsistent context everything does.

view this post on Zulip 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!

view this post on Zulip Notification Bot (Sep 18 2021 at 01:24):

Joshua Grosso has marked this topic as resolved.

view this post on Zulip 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: Aug 19 2022 at 19:03 UTC