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 hPropUnivalence for hProp and a proof of the fact that it is equivalent to a simplier and better known axiom propositionalUnivalenceAxiom. 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 preferred choice in this situation.

Contents

• The type hProp of types of h-level 1
• The type tildehProp of pairs (P, p : P) where P : hProp
• Intuitionistic logic on hProp
  • The hProp version of the "inhabited" construction.
  • ishinh and negation neg
  • ishinh and coprod
• Images and surjectivity for functions between types
  • The two-out-of-three properties of surjections
  • A function between types which is an inclusion and a surjection is a weak equivalence
  • 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
  • Negation and quantification
  • Negation and conjunction ("and") and disjunction ("or")
  • Property of being decidable and hdisj ("or")
  • The double negation version of hinhabited (does not require RR1)
• Univalence for hProp

Preamble

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 := make_hProp _ (isapropiscontr X). Definition isweq {X Y : UU} (f : X -> Y) : hProp := make_hProp _ (isapropisweq f). Definition isofhlevel (n : nat) (X : UU) : hProp := make_hProp _ (isapropisofhlevel n X). Definition isaprop (X : UU) : hProp := make_hProp (isaprop X) (isapropisaprop X). Definition isaset (X : UU) : hProp := make_hProp _ (isapropisaset X). Definition isisolated (X : UU) (x : X) : hProp := make_hProp _ (isapropisisolated X x). Definition isdecEq (X : UU) : hProp := make_hProp _ (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

ishinh and decidability

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 (∏ P)) <-> (exists (neg P)) and (neg (exists P)) <-> (∏ (neg P)). Of these four implications three are provable in the intuitionistic logic. The remaining implication (neg (∏ 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 ((¬ X) and (¬ Y)) <-> (¬ (X or Y)) and ((¬ X) or (¬ Y)) <-> (¬ (X and Y)). Of these four, three are provable unconditionally in the intuitionistic logic and the remaining one (¬ (X and Y)) -> ((¬ X) or (¬ Y)) is provable only if one of the propositions is decidable. These two cases are proved in PartC.v under the names fromneganddecx and fromneganddecy.

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

For being decidable hconj see isdecpropdirprod in uu0.v

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

Univalence for hProp