For sets and , consider a partial function from to to be a pair where and is a normal function . This captures the notion that the partial function is only ‘defined’ on . Let be the category of sets with maps being partial functions. Let be the category of sets with distinguished elements, with maps being functions that preserve distinguished elements.
Theorem: is equivalent to .
Proof: First, we write down a functor that ‘completes’ a partial function into a regular (total function) by adding a special element to the sets. In particular, for a set let . We add an element to the set and quite literally distinguish it because it is special. For a map , let
Note that this map takes to so it does preserve distinguished elements.
Define as follows: For a pointed set let . For a point-preserving map let , where is simply the restriction of to the set . This is well-defined precisely because certainly does not contain , and certainly does not send anything in to !
We wish to define . So for a set , we need the component , but since , we just have . We make the obvious choice then and let , which is the identity arrow on in . Let’s verify that this is actually a natural transformation. Let be a map in . We need , but this follows immediately because and and are identity arrows. So we have naturality. Furthermore every is clearly an isomorphism so is a natural isomorphism.
We will now define . We need a point-preserving map. Note that is the set with replaced by , and distinguished instead of . So, be the map sending and for all other elements . Let be a map in . To check naturality we need
Let’s examine – it can be described explicity as:
Let . We will consider where is sent by the left-hand side and the right-hand side by considering cases. First suppose , and . Then the right-hand side sends to , and the left-hand side sends . Suppose and . Then the right-hand side sends to , and so does the left. Finally, suppose . Then the right-hand side sends . The left-hand side sends . So the left and right-hand side are identical in all cases, so they must represent the same map. Then, we have naturality. Furthermore, and are certainly equal cardinality, so they are in bijection and all components of are isomorphisms. Thus is a natural isomorphism.
So, we have shown an equivalence between and .