The Setoid of Setoid functions

The setoid functions form again a setoid.

Nullary and n-ary operations

Composition of Setoid functions

Let S1, S2 and S3 be setoids, f a setoid function from S1 to S2, and g from S2 to S3 in the following definition of composition.

Composition as operation

Projections

Combining operations

Let S1, S2 and S3 be setoids.

In the following definition, we assume f is a setoid function from S1 to S2, and op is an unary operation on S2. Then opOnFun is the composition op after f.

The Free Setoid

Let A:CSetoid.

Partial Functions

In this section we define a concept of partial function for an arbitrary setoid. Essentially, a partial function is what would be expected---a predicate on the setoid in question and a total function from the set of points satisfying that predicate to the setoid. There is one important limitations to this approach: first, the record we obtain has type Type, meaning that we can't use, for instance, elimination of existential quantifiers.

Furthermore, for reasons we will explain ahead, partial functions will not be defined via the CSetoid_fun record, but the whole structure will be incorporated in a new record.

Finally, notice that to be completely general the domains of the functions have to be characterized by a CProp-valued predicate; otherwise, the use you can make of a function will be a priori restricted at the moment it is defined.

Before we state our definitions we need to do some work on domains.

Subsets of Setoids

Subsets of a setoid will be identified with predicates from the carrier set of the setoid into CProp. At this stage, we do not make any assumptions about these predicates.

We will begin by defining elementary operations on predicates, along with their basic properties. In particular, we will work with well defined predicates, so we will prove that these operations preserve welldefinedness.

Let S:CSetoid and P,Q:S->CProp.

Although at this stage we never use it, for completeness's sake we also treat disjunction (corresponding to union of subsets).

The next definition is a bit tricky, and is useful for choosing among the elements that satisfy a predicate P those that also satisfy R in the case where R is only defined for elements satisfying P---consider R to be a condition on the image of an object via a function with domain P. We chose to call this operation extension.

Operations

We are now ready to define the concept of partial function between arbitrary setoids.

The next lemma states that every partial function is well defined.

Similar for automorphisms.

The next lemma states that every partial function is well defined.

A few characteristics of this definition should be explained:

• The domain of the partial function is characterized by a predicate that is required to be well defined but not strongly extensional. The motivation for this choice comes from two facts: first, one very important subset of real numbers is the compact interval [a,b]---characterized by the predicate fun x : IR => a [<=] x /\ x [<=] b, which is not strongly extensional; on the other hand, if we can apply a function to an element s of a setoid S it seems reasonable (and at some point we do have to do it) to apply that same function to any element s' which is equal to s from the point of view of the setoid equality.
• The last two conditions state that pfpfun is really a subsetoid function. The reason why we do not write it that way is the following: when applying a partial function f to an element s of S we also need a proof object H; with this definition the object we get is f(s,H), where the proof is kept separate from the object. Using subsetoid notation, we would get f(⟨s,H⟩); from this we need to apply two projections to get either the original object or the proof, and we need to apply an extra constructor to get f(⟨s,H⟩) from s and H. This amounts to spending more resources when actually working with these objects.
• This record has type Type, which is very unfortunate, because it means in particular that we cannot use the well behaved set existential quantification over partial functions; however, later on we will manage to avoid this problem in a way that also justifies that we don't really need to use that kind of quantification. Another approach to this definition that completely avoid this complication would be to make PartFunct a dependent type, receiving the predicate as an argument. This does work in that it allows us to give PartFunct type Set and do some useful stuff with it; however, we are not able to define something as simple as an operator that gets a function and returns its domain (because of the restrictions in the type elimination rules). This sounds very unnatural, and soon gets us into strange problems that yield very unlikely definitions, which is why we chose to altogether do away with this approach.

All partial functions will henceforth be denoted by capital letters.

We now present some methods for defining partial functions.

To begin with, we want to be able to ``see'' each total function as a partial function.

In any setoid we can also define constant functions (one for each element of the setoid) and an identity function:

Let c:S.

(These happen to be always total functions, but that is more or less obvious, as we have no information on the setoid; however, we will be able to define partial functions just applying other operators to these ones.)

If we have two setoid functions F and G we can always compose them. The domain of our new function will be the set of points s in the domain of F for which F(s) is in the domain of G. Notice that the use of extension here is essential. The inversion in the order of the variables is done to maintain uniformity with the usual mathematical notation.

Let G,F:(PartFunct S) and denote by Q and P, respectively, the predicates characterizing their domains.

Let F:(BinPartFunct S1 S2) and G:(PartFunct S2 S3), and denote by Q and P, respectively, the predicates characterizing their domains.

Bijections