Library UniMath.Foundations.Propositions

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
  • 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

Require Export UniMath.Foundations.PartD.

Universe structure



To upstream files

The type hProp of types of h-level 1


Definition hProp := total2 (λ X : UU, isaprop X).
Definition make_hProp (X : UU) (is : isaprop X) : hProp
  := tpair (λ X : UU, isaprop X) X is.
Definition hProptoType := @pr1 _ _ : hProp -> UU.
Coercion hProptoType : hProp >-> UU.

Definition propproperty (P : hProp) := pr2 P : isaprop (pr1 P).

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


Definition tildehProp := total2 (λ P : hProp, P).
Definition make_tildehProp {P : hProp} (p : P) : tildehProp := tpair _ P p.


Corollary subtypeInjectivity_prop {A : UU} (B : A -> hProp) :
   (x y : total2 B), (x = y) (pr1 x = pr1 y).
Show proof.
  intros. apply subtypeInjectivity. intro. apply propproperty.

Corollary subtypePath_prop {A : UU} {B : A -> hProp}
   {s s' : total2 (λ x, B x)} : pr1 s = pr1 s' -> s = s'.
Show proof.
  apply invmap. apply subtypeInjectivity_prop.

Corollary impred_prop {T : UU} (P : T -> hProp) : isaprop ( t : T, P t).
Show proof.
  intros. apply impred; intro. apply propproperty.

Corollary isaprop_total2 (X : hProp) (Y : X -> hProp) : isaprop ( x, Y x).
Show proof.
  intros.
  apply (isofhleveltotal2 1).
  - apply propproperty.
  - intro x. apply propproperty.

Lemma isaprop_forall_hProp (X : UU) (Y : X -> hProp) : isaprop ( x, Y x).
Show proof.
  intros. apply impred_isaprop. intro x. apply propproperty.

Definition forall_hProp {X : UU} (Y : X -> hProp) : hProp
  := make_hProp ( x, Y x) (isaprop_forall_hProp X Y).

Notation "∀ x .. y , P"
  := (forall_hProp (λ x, .. (forall_hProp (λ y, P))..))
       (at level 200, x binder, y binder, right associativity) : type_scope.

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.


Definition ishinh_UU (X : UU) : UU := P : hProp, ((X -> P) -> P).

Lemma isapropishinh (X : UU) : isaprop (ishinh_UU X).
Show proof.
  apply impred.
  intro P. apply impred.
  intro. apply (pr2 P).

Definition ishinh (X : UU) : hProp := make_hProp (ishinh_UU X) (isapropishinh X).

Notation nonempty := ishinh (only parsing).

Notation "∥ A ∥" := (ishinh A) (at level 20) : type_scope.

Definition hinhpr {X : UU} : X -> X
  := λ x : X, λ P : hProp, fun f : X -> P => f x.

Definition hinhfun {X Y : UU} (f : X -> Y) : X -> Y :=
  fun isx : X => λ P : _, fun yp : Y -> P => isx P (λ x : X, yp (f x)).

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

Definition hinhuniv {X : UU} {P : hProp} (f : X -> P) (wit : X ) : P
  := wit P f.

Corollary factor_through_squash {X Q : UU} : isaprop Q -> (X -> Q) -> X -> Q.
Show proof.
  intros i f h. exact (@hinhuniv X (Q,,i) f h).

Corollary squash_to_prop {X Q : UU} : X -> isaprop Q -> (X -> Q) -> Q.
Show proof.
  intros h i f. exact (@hinhuniv X (Q,,i) f h).

Definition hinhand {X Y : UU} (inx1 : X ) (iny1 : Y ) : X × Y
  := λ P : _, ddualand (inx1 P) (iny1 P).

Definition hinhuniv2 {X Y : UU} {P : hProp} (f : X -> Y -> P)
           (isx : X ) (isy : Y ) : P
  := hinhuniv (λ xy : X × Y, f (pr1 xy) (pr2 xy)) (hinhand isx isy).

Definition hinhfun2 {X Y Z : UU} (f : X -> Y -> Z)
           (isx : X ) (isy : Y ) : Z
  := hinhfun (λ xy: X × Y, f (pr1 xy) (pr2 xy)) (hinhand isx isy).

Definition hinhunivcor1 (P : hProp) : P -> P := hinhuniv (idfun P).
Notation hinhprinv := hinhunivcor1.

ishinh and negation neg


Lemma weqishinhnegtoneg (X : UU) : ¬ X ¬ X.
Show proof.
  assert (lg : logeq (ishinh (neg X)) (neg X)).
  {
    split.
    - simpl. apply (@hinhuniv _ (make_hProp _ (isapropneg X))).
      simpl. intro nx. apply nx.
    - apply hinhpr.
  }
  apply (weqimplimpl (pr1 lg) (pr2 lg) (pr2 (ishinh _)) (isapropneg X)).

Lemma weqnegtonegishinh (X : UU) : ¬ X ¬ X .
Show proof.
  assert (lg : logeq (neg (ishinh X)) (neg X)).
  {
    split.
    - apply (negf (@hinhpr X)).
    - intro nx. unfold neg. simpl.
      apply (@hinhuniv _ (make_hProp _ isapropempty)).
      apply nx.
  }
  apply (weqimplimpl (pr2 lg) (pr1 lg) (isapropneg _) (isapropneg _)).


Lemma hinhcoprod (X Y : UU) : (∥ X ⨿ Y ∥) -> X ⨿ Y .
Show proof.
  intros is. unfold ishinh. intro P. intro CP.
  set (CPX := λ x : X, CP (ii1 x)).
  set (CPY := λ y : Y, CP (ii2 y)).
  set (is1P := is P).
  assert (f : (ishinh X) ⨿ (ishinh Y) -> P).
  apply (sumofmaps (hinhuniv CPX) (hinhuniv CPY)).
  apply (is1P f).

ishinh and decidability

Lemma decidable_ishinh {X} : decidable X decidable(X).
Show proof.
  intros d.
  unfold decidable in *.
  induction d as [x|x'].
  - apply ii1. apply hinhpr. assumption.
  - apply ii2. intros p.
    apply (squash_to_prop p).
    + exact isapropempty.
    + exact x'.

Images and surjectivity for functions between types

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

Definition image {X Y : UU} (f : X -> Y) : UU
  := total2 (λ y : Y, ishinh (hfiber f y)).
Definition make_image {X Y : UU} (f : X -> Y) :
   (t : Y), (λ y : Y, hfiber f y ) t y : Y, hfiber f y
  := tpair (λ y : Y, ishinh (hfiber f y)).
Definition pr1image {X Y : UU} (f : X -> Y) :
  ( y : Y, hfiber f y ) Y
  := @pr1 _ (λ y : Y, ishinh (hfiber f y)).

Definition prtoimage {X Y : UU} (f : X -> Y) : X -> image f.
Show proof.
  intros X0.
  apply (make_image _ (f X0) (hinhpr (make_hfiber f X0 (idpath _)))).

Definition issurjective {X Y : UU} (f : X -> Y) := y : Y, ishinh (hfiber f y).

Lemma isapropissurjective {X Y : UU} (f : X -> Y) : isaprop (issurjective f).
Show proof.
  intros. apply impred.
  intro t. apply (pr2 (ishinh (hfiber f t))).

Lemma isinclpr1image {X Y : UU} (f : X -> Y): isincl (pr1image f).
Show proof.
  intros. refine (isofhlevelfpr1 _ _ _).
  intro. apply (pr2 (ishinh (hfiber f x))).

Lemma issurjprtoimage {X Y : UU} (f : X -> Y) : issurjective (prtoimage f).
Show proof.
  intros. intro z.
  set (f' := prtoimage f).
  assert (ff: hfiber (funcomp f' (pr1image f)) (pr1 z) -> hfiber f' z)
    by refine (invweq (samehfibers _ _ (isinclpr1image f) z)).
  apply (hinhfun ff).
  exact (pr2 z).

The two-out-of-three properties of surjections


Lemma issurjcomp {X Y Z : UU} (f : X -> Y) (g : Y -> Z)
      (isf : issurjective f) (isg : issurjective g) :
  issurjective (funcomp f g).
Show proof.
  intros. unfold issurjective.
  intro z. apply (λ ff, hinhuniv ff (isg z)).
  intro ye. apply (hinhfun (hfibersftogf f g z ye)).
  apply (isf).

Notation issurjtwooutof3c := issurjcomp.

Lemma issurjtwooutof3b {X Y Z : UU} (f : X -> Y) (g : Y -> Z)
      (isgf : issurjective (funcomp f g)) : issurjective g.
Show proof.
  intros. unfold issurjective.
  intro z. apply (hinhfun (hfibersgftog f g z) (isgf z)).

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


Lemma isweqinclandsurj {X Y : UU} (f : X -> Y) :
  isincl f -> issurjective f -> isweq f.
Show proof.
  intros Hincl Hsurj.
  intro y.
  set (H := make_hProp (iscontr (hfiber f y)) (isapropiscontr _)).
  apply (Hsurj y H).
  intro x.
  simpl.
  apply iscontraprop1.
  - apply Hincl.
  - apply x.

On the other hand, a weak equivalence is surjective

Lemma issurjectiveweq (X Y : UU) (f : X -> Y) : isweq f -> issurjective f.
Show proof.
  intros H y.
  apply hinhpr.
  apply (pr1 (H y)).

Intuitionistic logic on hProp.


Definition htrue : hProp := make_hProp unit isapropunit.

Definition hfalse : hProp := make_hProp empty isapropempty.

Definition hconj (P Q : hProp) : hProp
  := make_hProp (P × Q) (isapropdirprod _ _ (pr2 P) (pr2 Q)).

Notation "A ∧ B" := (hconj A B) (at level 80, right associativity) : type_scope.

Definition hdisj (P Q : UU) : hProp := ishinh (coprod P Q).

Notation "X ∨ Y" := (hdisj X Y) (at level 85, right associativity) : type_scope.

Definition hdisj_in1 {P Q : UU} : P -> P Q.
Show proof.
  intros. apply hinhpr. apply ii1. assumption.

Definition hdisj_in2 {P Q : UU} : Q -> P Q.
Show proof.
  intros. apply hinhpr. apply ii2. assumption.

Lemma disjoint_disjunction (P Q : hProp) : (P -> Q -> ) -> hProp.
Show proof.
  intros n.
  exact (P ⨿ Q,, isapropcoprod P Q (propproperty P) (propproperty Q) n).

Definition hneg (P : UU) : hProp := make_hProp (¬ P) (isapropneg P).


Declare Scope logic.
Notation "'¬' X" := (hneg X) (at level 35, right associativity) : logic.
Delimit Scope logic with logic.

Definition himpl (P : UU) (Q : hProp) : hProp.
Show proof.
  intros. split with (P -> Q). apply impred. intro. apply (pr2 Q).

Local Notation "A ⇒ B" := (himpl A B) : logic.
Local Open Scope logic.

Definition hexists {X : UU} (P : X -> UU) := total2 P .

Notation "'∃' x .. y , P"
  := (ishinh ( x ,.. ( y , P)..))
       (at level 200, x binder, y binder, right associativity) : type_scope.

Definition wittohexists {X : UU} (P : X -> UU) (x : X) (is : P x) : hexists P
  := @hinhpr (total2 P) (tpair _ x is).

Definition total2tohexists {X : UU} (P : X -> UU) : total2 P -> hexists P
  := hinhpr.

Definition weqneghexistsnegtotal2 {X : UU} (P : X -> UU) :
  weq (neg (hexists P)) (neg (total2 P)).
Show proof.
  intros.
  assert (lg : (neg (hexists P)) <-> (neg (total2 P))).
  {
    split.
    - apply (negf (total2tohexists P)).
    - intro nt2. unfold neg. change (ishinh_UU (total2 P) -> hfalse).
      apply (hinhuniv). apply nt2.
  }
  apply (weqimplimpl (pr1 lg) (pr2 lg) (isapropneg _) (isapropneg _)).

Associativity and commutativity of hdisj and hconj up to logical equivalence


Lemma islogeqcommhdisj {P Q : hProp} : hdisj P Q <-> hdisj Q P.
Show proof.
  intros. split.
  - simpl. apply hinhfun. apply coprodcomm.
  - simpl. apply hinhfun. apply coprodcomm.

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/


Lemma hconjtohdisj (P Q : UU) (R : hProp) : (P R) (Q R) -> (P Q) R.
Show proof.
  intros X0.
  assert (s1: hdisj P Q -> R).
  {
    intro X1.
    assert (s2: coprod P Q -> R).
    {
      intro X2.
      induction X2 as [ XP | XQ ].
      - apply X0. apply XP.
      - apply (pr2 X0). apply XQ.
    }
    apply (hinhuniv s2). apply X1.
  }
  unfold himpl. simpl. apply s1.

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 ???.

Lemma hexistsnegtonegforall {X : UU} (F : X -> UU) :
  ( x : X, neg (F x)) -> neg ( x : X, F x).
Show proof.
  simpl.
  apply (@hinhuniv _ (make_hProp _ (isapropneg ( x : X, F x)))).
  simpl. intros t2 f2. induction t2 as [ x d2 ]. apply (d2 (f2 x)).

Lemma forallnegtoneghexists {X : UU} (F : X -> UU) :
  ( x : X, neg (F x)) -> neg ( x, F x).
Show proof.
  intros nf.
  change ((ishinh_UU (total2 F)) -> hfalse).
  apply hinhuniv. intro t2. induction t2 as [ x f ]. apply (nf x f).

Lemma neghexisttoforallneg {X : UU} (F : X -> UU) :
  ¬ ( x, F x) -> x : X, ¬ (F x).
Show proof.
  intros nhe x. intro fx.
  apply (nhe (hinhpr (tpair F x fx))).

Definition weqforallnegtonegexists {X : UU} (F : X -> UU) :
  ( x : X, ¬ F x) (¬ x, F x).
Show proof.
  intros.
  apply (weqimplimpl (forallnegtoneghexists F) (neghexisttoforallneg F)).
  apply impred. intro x. apply isapropneg. apply isapropneg.

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.

Lemma tonegdirprod {X Y : UU} : ¬ X ¬ Y -> ¬ (X × Y).
Show proof.
  simpl.
  apply (@hinhuniv _ (make_hProp _ (isapropneg (X × Y)))).
  intro c. induction c as [ nx | ny ].
  - simpl. intro xy. apply (nx (pr1 xy)).
  - simpl. intro xy. apply (ny (pr2 xy)).

Lemma weak_fromnegdirprod (P Q: hProp) : ¬ (P Q) -> ¬¬(¬ P ¬ Q).
Show proof.
  intros npq k.
  assert (e : ¬¬ Q).
  {
    intro n. apply k. apply hdisj_in2. assumption.
  }
  assert (d : ¬¬ P).
  {
    intro n. apply k. apply hdisj_in1. assumption.
  }
  clear k.
  apply d; clear d. intro p. apply e; clear e. intro q.
  refine (npq _). exact (p,,q).

Lemma tonegcoprod {X Y : UU} : ¬ X × ¬ Y -> ¬ (X ⨿ Y).
Show proof.
  intros is. intro c. induction c as [ x | y ].
  - apply (pr1 is x).
  - apply (pr2 is y).

Lemma toneghdisj {X Y : UU} : ¬ X × ¬ Y -> ¬ (X Y).
Show proof.
  intros is. unfold hdisj.
  apply weqnegtonegishinh.
  apply tonegcoprod.
  apply is.

Lemma fromnegcoprod {X Y : UU} : ¬ (X ⨿ Y) -> ¬X × ¬Y.
Show proof.
  intros is. split.
  - exact (λ x, is (ii1 x)).
  - exact (λ y, is (ii2 y)).

Corollary fromnegcoprod_prop {X Y : hProp} : ¬ (X Y) -> ¬ X ¬ Y.
Show proof.
  intros n.
  simpl in *.
  assert (n' := negf hinhpr n); simpl in n'; clear n.
  apply fromnegcoprod. assumption.

Lemma hdisjtoimpl {P : UU} {Q : hProp} : P Q -> ¬ P -> Q.
Show proof.
  assert (int : isaprop (¬ P -> Q)).
  {
    apply impred. intro.
    apply (pr2 Q).
  }
  simpl. apply (@hinhuniv _ (make_hProp _ int)).
  simpl. intro pq. induction pq as [ p | q ].
  - intro np. induction (np p).
  - intro np. apply q.

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

For being decidable hconj see isdecpropdirprod in uu0.v

Lemma isdecprophdisj {X Y : UU} (isx : isdecprop X) (isy : isdecprop Y) :
  isdecprop (hdisj X Y).
Show proof.
  intros.
  apply isdecpropif. apply (pr2 (hdisj X Y)).
  induction (pr1 isx) as [ x | nx ].
  - apply (ii1 (hinhpr (ii1 x))).
  - induction (pr1 isy) as [ y | ny ].
    + apply (ii1 (hinhpr (ii2 y))).
    + apply (ii2 (toneghdisj (make_dirprod nx ny))).

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


Definition isinhdneg (X : UU) : hProp := make_hProp (dneg X) (isapropdneg X).

Definition inhdnegpr (X : UU) : X -> isinhdneg X := todneg X.

Definition inhdnegfun {X Y : UU} (f : X -> Y) : isinhdneg X -> isinhdneg Y
  := dnegf f.

Definition inhdneguniv (X : UU) (P : UU) (is : isweq (todneg P)) :
  (X -> P) -> ((isinhdneg X) -> P)
  := λ xp : _, λ inx0 : _, (invmap (make_weq _ is) (dnegf xp inx0)).

Definition inhdnegand (X Y : UU) (inx0 : isinhdneg X) (iny0 : isinhdneg Y) :
  isinhdneg (X × Y) := dneganddnegimpldneg inx0 iny0.

Definition hinhimplinhdneg (X : UU) (inx1 : ishinh X) : isinhdneg X
  := inx1 hfalse.

Univalence for hProp


Theorem hPropUnivalence : (P Q : hProp), (P -> Q) -> (Q -> P) -> P = Q.
Show proof.
  intros ? ? f g.
  apply subtypePath.
  - intro X. apply isapropisaprop.
  - apply propositionalUnivalenceAxiom.
    + apply propproperty.
    + apply propproperty.
    + assumption.
    + assumption.

Definition eqweqmaphProp {P P' : hProp} (e : @paths hProp P P') : P P'.
Show proof.
  intros. induction e. apply idweq.

Definition weqtopathshProp {P P' : hProp} (w : P P') : P = P'
  := hPropUnivalence P P' w (invweq w).

Definition weqpathsweqhProp {P P' : hProp} (w : P P') :
  eqweqmaphProp (weqtopathshProp w) = w.
Show proof.
  intros. apply proofirrelevance.
  apply (isapropweqtoprop P P' (pr2 P')).

Theorem univfromtwoaxiomshProp (P P' : hProp) : isweq (@eqweqmaphProp P P').
Show proof.
  intros.

  set (P1 := λ XY : hProp × hProp, paths (pr1 XY) (pr2 XY)).
  set (P2 := λ XY : hProp × hProp, (pr1 XY) (pr2 XY)).
  set (Z1 := total2 P1).
  set (Z2 := total2 P2).
  set (f := (totalfun _ _ (λ XY : hProp × hProp,
                             @eqweqmaphProp (pr1 XY) (pr2 XY)): Z1 -> Z2)).
  set (g := (totalfun _ _ (λ XY : hProp × hProp,
                             @weqtopathshProp (pr1 XY) (pr2 XY)): Z2 -> Z1)).
  assert (efg : z2 : Z2 , paths (f (g z2)) z2).
  {
    intros. induction z2 as [ XY w].
    exact (maponpaths (fun w : (pr1 XY) (pr2 XY) => tpair P2 XY w)
                      (@weqpathsweqhProp (pr1 XY) (pr2 XY) w)).
  }

  set (h := λ a1 : Z1, (pr1 (pr1 a1))).
  assert (egf0 : a1 : Z1, paths (pr1 (g (f a1))) (pr1 a1))
         by (intro; apply idpath).
  assert (egf1 : a1 a1' : Z1, paths (pr1 a1') (pr1 a1) -> a1' = a1).
  {
    intros ? ? X.
    set (X' := maponpaths (@pr1 _ _) X).
    assert (is : isweq h) by apply (isweqpr1pr1 hProp).
    apply (invmaponpathsweq (make_weq h is) _ _ X').
  }
  set (egf := λ a1, (egf1 _ _ (egf0 a1))).
  set (is2 := isweq_iso _ _ egf efg).
  apply (isweqtotaltofib P1 P2 (λ XY : hProp × hProp,
                                  @eqweqmaphProp (pr1 XY) (pr2 XY)) is2
                         (make_dirprod P P')).

Definition weqeqweqhProp (P P' : hProp) : P = P' (P P')
  := make_weq _ (univfromtwoaxiomshProp P P').

Corollary isasethProp : isaset hProp.
Show proof.
  unfold isaset. simpl. intros x x'.
  apply (isofhlevelweqb (S O) (weqeqweqhProp x x')
                        (isapropweqtoprop x x' (pr2 x'))).

Definition weqpathsweqhProp' {P P' : hProp} (e : P = P') :
  weqtopathshProp (eqweqmaphProp e) = e.
Show proof.
  intros. apply isasethProp.

Lemma iscontrtildehProp : iscontr tildehProp.
Show proof.
  split with (tpair _ htrue tt). intro tP. induction tP as [ P p ].
  apply (invmaponpathsincl _ (isinclpr1 (λ P : hProp, P) (λ P, pr2 P))).
  simpl. apply hPropUnivalence. apply (λ x, tt). intro t. apply p.

Lemma isaproptildehProp : isaprop tildehProp.
Show proof.

Lemma isasettildehProp : isaset tildehProp.
Show proof.


Definition logeqweq (P Q : hProp) : (P -> Q) -> (Q -> P) -> P Q :=
  λ f g, weqimplimpl f g (pr2 P) (pr2 Q).

Theorem total2_paths_hProp_equiv {A : UU} (B : A -> hProp)
   (x y : total2 (λ x, B x)) : (x = y) (pr1 x = pr1 y).
Show proof.
  intros.
  apply subtypeInjectivity.
  intro a. apply (pr2 (B a)).