Generalities on hSet . Vladimir Voevodsky. Feb. - Sep. 2011

In this file we introduce the type hSet of h-sets i.e. of types of h-level 2 as well as a number of constructions such as type of (monic) subtypes, images, surjectivity etc. which, while they formally apply to functions between arbitrary types actually only depend on the behavior of the function on the sets of connected componenets of these types.

While it is possible to write a part of this file in a form which does not require RR1 it seems like a waste of effort since it would require to repeat a lot of things twice. Accordingly we assume RR1 from the start in dealing with sets. The drawback is that all the subsequent files will not compile at the moment without the Type in Type patch.

Preambule

Settings

This line has to be removed for the file to compile with Coq8.2

Imports

The type of sets i.e. of types of h-level 2 in UU

Booleans as a set

Types X which satisfy " weak " axiom of choice for all families P : X -> UU0

Weak axiom of choice for X is the condition that for any family P : X -> UU0 over X such that all members of the family are inhabited the space of sections of the family is inhabited . Equivalently one can formulate it as an assertion that for any surjection ( see below ) p : Y -> X the space of sections of this surjection i.e. functions s : X -> Y together with a homotopy from funcomp s p to idfun X is inhabited . It does not provide a choice of a section for such a family or a surjection . In topos-theoretic semantics this condition corresponds to " local projectivity " of X . It automatically holds for the point unit but need not hold for sub-objects of unit i.e. for types of h-level 1 ( propositions ) . In particular it does not have to hold for general types with decidable equality .

Intuition based on standard univalent models suggests that any type satisfying weak axiom of choice is a set . Indeed it seems to be possible to show that if both a type and the set of connected components of this type ( see below ) satisfy weak axiom of choice then the type is a set . In particular , if one imposes weak axiom of choice for sets as an axiom then it would follow that every type satisfying weak axiom of choice is a set . I do not know however if there are models which would validate a possibility of types other than sets to satisfy weak axiom of choice .

Uses RR1

The type of monic sybtypes of a type (subsets of the set of connected components)

Genneral definitions

Direct product of two subtypes

A a subtype of with a paths between any every two elements is an h-prop.

Relations on types ( or equivalently relations on the sets of connected components)

General definitions

Direct product of two relations

Partial orderings and associated types .

Eqivalence relations and associated types .

Direct product of two equivalence relations

Equivalence classes with respect to a given relation

Direct product of equivalence classes

Images and surjectivity for functions between types (both depend only on the behavior of the corresponding function between the sets of connected components)

Surjections to sets are epimorphisms

The two-out-of-three properties of surjections

A function between hsets which is an inclusion and a surjection is a weak equivalence

Set quotients of types.

In this file we study the set quotients of types by equivalence relations. While the general notion of a quotient of a type by a relation is complicated due to the existence of different kinds of quotients (e.g. homotopy quotients or categorical quotients in the homotopy category which are usually different from each other) there is one particular class of quotients which is both very important for applications and semantically straightforward. These quotients are the universal functions from a type to an hset which respect a given relation. Some of the proofs in this section depend on the proerties of the hinhabited construction and some also depend on the univalence axiom for hProp which allows us to prove that the type of monic subtypes of a type is a set.

Our main construction is analogous to the usual construction of quotient as a set of equivalence classes. Wev also consider another construction of setquot which is analogous ( on the next h-level ) to our construction of ishinh . Both have generalizations to the "higher" quotients (i.e. groupoid quotients etc.) which will be considered separately. In particular, the quotients the next h-level appear to be closely related to the localizations of categories and will be considered in the section about types of h-level 3.

Setquotient defined in terms of equivalence classes

Universal property of seqtquot R for functions to sets satisfying compatibility condition iscomprelfun

Note: the axioms rax, sax and trans are not used in the proof of setquotuniv. If we consider a relation which is not an equivalence relation then setquot will still be the set of subsets which are equivalence classes. Now however such subsets need not to cover all of the type. In fact their set can be empty. Nevertheless setquotuniv will apply.

Functoriality of setquot for functions mapping one relation to another

Universal property of setquot for predicates with 1 , 2 and 3 variables

Important note : theorems proved above can not be used ( al least at the moment ) to construct terms whose complete normalization ( evaluation ) is important . For example they should not be used * directly * to construct isdeceq property of setquot since isdeceq is in turn used to construct boolean equality booleq and evaluation of booleq x y is important for computational purposes . Terms produced using these universality theorems will not fully normalize even in simple cases due to the following steps in the proof of setquotunivprop . As a part of the proof term of this theorem there appears the composition of an application of uahp , transfer of the resulting term of the identity type by maponpaths along P followed by the reconstruction of a equivalence ( two directional implication ) between the corresponding propositions through eqweqmaphProp . The resulting implications are " opaque " and the proofs of disjunctions P \/ Q produced with the use of such implications can not be evaluated to one of the summands of the disjunction . An example is given by the following theorem isdeceqsetquot_non_constr which , as simple experiments show, can not be used to compute the value of isdeceqsetquot . Below we give another proof of isdeceq ( setquot R ) using the same assumptions which is " constructive " i.e. usable for the evaluation purposes .

The case when the function between quotients defined by setquotfunt is a surjection , inclusion or a weak equivalence

setquot with respect to the product of two relations

Universal property of setquot for functions of two variables

Functoriality of setquot for functions of two variables mapping one relation to another

Set quotients with respect to decidable equivalence relations have decidable equality

The set of connected components of type.

Set quotients. Construction 2.

****************** THIS SECTION IS UNFINISHED ******************

The following construction of the set quotient is based on the following idea. Let X be a set. Then we have the obvious "double evaluation map" from X to the product over all sets Y of the sets ((X -> Y) -> Y). This is always an inclusion and in particular X is isomorphic to the image of this map. Suppore now we have a relation (which need not be an equivalence relation) R on X. Then we know that (X/R -> Y) is a subset of (X -> Y) which consists of functions compatible with the relation even if we do not know what X/R is. Thus we may consider the image of X in the product over all Y of ((X/R -> Y) ->Y) and it must be isomorphic to X/R. This ideas are realized in the definitions given below. There are two advantages to this approach. One is that the relation need not be an equivalence relation. Another one is that it can be more easily generalized to the higher quotients of type.

We also show that two constructions of set-quotients of types - the one given in set_quotients and the one given here agree up to an isomorphism (weak equivalence).

Functions compatible with a relation

The quotient set of a type by a relation.

The previous results show that setquot2 as constructed is indeed the categorical quotient of X with respect to R. What we can not direcly show for this construction is that for (X : UU0) (R : hrel X) ( x x' : X) ( e: paths (setquot2pr _ R x) (setquot2pr _ R x')) (is : iseqrel X R) one has R x x' . For this we will need to define setquot2 in terms of equivalence classes and then show that the two constructions agree.