Actually, there’s a more interesting way to go from partition-as-api to partition-as-coproduct-of-inclusions. You just pull the identity morphism 1I along the epic e:S↠I. The pullback of the identity functor is the partition-as-coproduct-of-inclusions.
Actually, there’s a more interesting way to go from partition-as-api to partition-as-coproduct-of-inclusions. You just pull the identity morphism 1I along the epic e:S↠I. The pullback of the identity functor is the partition-as-coproduct-of-inclusions.