Generalities on hProp. Vladimir Voevodsky . May - Sep. 2011 .

In this file we introduce the hProp - an analog of Prop defined based on the univalent semantics. We further introduce the hProp version of the "inhabited" construction - i.e. for any T in UU0 we construct an object ishinh T and a function hinhpr : T -> ishinh T which plays the role of inhabits from the Coq standard library. The semantic meaning of hinhpr is that it is universal among functions from T to objects of hProp. Proving that ishinh T is in hProp requires a resizing rule which can be written in the putative notation for such rules as follows : Resizing Rule RR1 ( U1 U2 : Univ ) ( X : U1 ) ( is : isaprop X ) |- X : U2 . Further in the file we introduce the univalence axiom for hProp and a proof of the fact that it is equivalent to a simplier and better known axiom uahp . We prove that this axiom implies that hProp satisfies isaset i.e. it is a type of h-level 2 . This requires another resizing rule : Resizing Rule RR2 ( U1 U2 : Univ ) |- @hProp U1 : U2 . Since resizing rules are not currently implemented in Coq the file does not compile without a patch provided by Hugo Herbelin which turns off the universe consistency verification. We do however keep track of universes in our development "by hand" to ensure that when the resizing rules will become available the current proofs will verify correctly. To point out which results require resizing rules in a substantial way we mark the first few of such reults by or comment . One can achieve similar results with a combination of usual axioms which imitate the resizing rules. However unlike the usual axioms the resizing rules do not affect the computation/normalization abilities of Coq which makes them the prefrred choice in this situation.

Preamble

Settings

Imports

Universe structure

To upstream files

The type hProp of types of h-level 1

The type tildehProp of pairs ( P , p : P ) where P : hProp

The following re-definitions should make proofs easier in the future when the unification algorithms in Coq are improved . At the moment they create more complications than they eliminate ( e.g. try to prove isapropishinh with isaprop in hProp ) so for the time being they are commented out . Definition iscontr ( X : UU ) : hProp := hProppair _ ( isapropiscontr X ) . Definition isweq { X Y : UU } ( f : X -> Y ) : hProp := hProppair _ ( isapropisweq f ) . Definition isofhlevel ( n : nat ) ( X : UU ) : hProp := hProppair _ ( isapropisofhlevel n X ) . Definition isaprop ( X : UU ) : hProp := hProppair ( isaprop X ) ( isapropisaprop X ) . Definition isaset ( X : UU ) : hProp := hProppair _ ( isapropisaset X ) . Definition isisolated ( X : UU ) ( x : X ) : hProp := hProppair _ ( isapropisisolated X x ) . Definition isdecEq ( X : UU ) : hProp := hProppair _ ( isapropisdeceq X ) .

Intuitionistic logic on hProp

The hProp version of the "inhabited" construction.

Note that the previous definitions do not require RR1 in an essential way ( except for the placing of ishinh in hProp UU - without RR1 it would be placed in hProp UU1 ) . The first place where RR1 is essentially required is in application of hinhuniv to a function X -> ishinh Y

ishinh and negation neg

ishinh and coprod

Images and surjectivity for functions between types

(both depend only on the behavior of the corresponding function between the sets of connected components)

The two-out-of-three properties of surjections

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

On the other hand, a weak equivalence is surjective

Intuitionistic logic on hProp .

Associativity and commutativity of hdisj and hconj up to logical equivalence

Proof of the only non-trivial axiom of intuitionistic logic for our constructions. For the full list of axioms see e.g. http://plato.stanford.edu/entries/logic-intuitionistic/

Negation and quantification.

There are four standard implications in classical logic which can be summarized as ( neg ( forall P ) ) <-> ( exists ( neg P ) ) and ( neg ( exists P ) ) <-> ( forall ( neg P ) ) . Of these four implications three are provable in the intuitionistic logic. The remaining implication ( neg ( forall P ) ) -> ( exists ( neg P ) ) is not provable in general . For a proof in the case of bounded quantification of decidable predicates on natural numbers see hnat.v . For some other cases when these implications hold see ??? .

Negation and conjunction ( "and" ) and disjunction ( "or" ) .

There are four implications in classical logic ( ( neg X ) and ( neg Y ) ) <-> ( neg ( X or Y ) ) and ( ( neg X ) or ( neg Y ) ) <-> ( neg ( X and Y ) ) . Of these four, three are provable unconditionally in the intuitionistic logic and the remaining one ( neg ( X and Y ) ) -> ( ( neg X ) or ( neg Y ) ) is provable only if one of the propositions is deidable. These two cases are proved in uu0.v under the names fromneganddecx and fromneganddecy .

Property of being decidable and hdisj ( "or" ) .

For being deidable hconj see isdecpropdirprod in uu0.v

The double negation version of hinhabited ( does not require RR1 ) .

Univalence axiom for hProp

We introduce here the weakest form of the univalence axiom - the univalence axiom for hProp which is equivalent to the second part of the extensionality axiom in Church simple type theory. This axiom is easily shown to be equivalent to its version with P = P' as a target and to weqtopathshProp (see below) as well as to the version of weqtopathshProp with P = P' as a target. The proof of theorem univfromtwoaxiomshProp is modeled on the proof of univfromtwoaxioms from univ01.v