Library UniMath.MoreFoundations.Propositions

Require Export UniMath.MoreFoundations.Notations.
Require Export UniMath.MoreFoundations.PartA.
Require Export UniMath.MoreFoundations.Tactics.
Require Export UniMath.MoreFoundations.DecidablePropositions.

Local Open Scope logic.
Local Open Scope type.

Lemma ishinh_irrel {X:UU} (x:X) (x':∥X ∥) : hinhpr x = x'.
Show proof.

apply proofirrelevance. apply propproperty.

Corollary squash_to_hProp {X:UU} {Q:hProp} : ∥ X ∥ -> (X -> Q ) -> Q.
Show proof.

intros h f. exact (hinhuniv f h).

Lemma hdisj_impl_1 {P Q : hProp} : P ∨Q -> (Q ->P ) -> P.
Show proof.

  intros o f. apply (squash_to_hProp o).
  intros [p|q].
  - exact p.
  - exact (f q).

Lemma hdisj_impl_2 {P Q : hProp} : P ∨Q -> (P ->Q ) -> Q.
Show proof.

  intros o f. apply (squash_to_hProp o).
  intros [p|q].
  - exact (f p).
  - exact q.

Definition weqlogeq (P Q : hProp) : (P = Q ) ≃ (P ⇔ Q ).
Show proof.

  intros.
  apply weqimplimpl.
  - intro e. induction e. apply isrefl_logeq.
  - intro c. apply hPropUnivalence.
    + exact (pr1 c).
    + exact (pr2 c).
  - apply isasethProp.
  - apply propproperty.

Lemma decidable_proof_by_contradiction {P:hProp} : decidable P -> ¬ ¬ P -> P.
Show proof.

  intros dec nnp. induction dec as [p|np].
  - exact p.
  - apply fromempty. exact (nnp np).

Lemma proof_by_contradiction {P:hProp} : LEM -> ¬ ¬ P -> P.
Show proof.

intro lem.
exact (decidable_proof_by_contradiction (lem P)).

Lemma dneg_elim_to_LEM : (∏ P:hProp , ¬ ¬ P -> P ) -> LEM.
Show proof.

  intros dne. intros P. simple refine (dne (_,,_) _).
  simpl. intros n.
  assert (q : ¬ (P ∨ ¬ P)).
  { now apply weqnegtonegishinh. }
  assert (r := fromnegcoprod_prop q).
  exact (pr2 r (pr1 r)).

Lemma negforall_to_existsneg {X:UU} (P:X ->hProp) : LEM -> (¬ ∀ x , P x ) -> (∃ x , ¬ (P x )).
Show proof.

  intros lem nf. apply (proof_by_contradiction lem); intro c. use nf; clear nf. intro x.
  assert (q := neghexisttoforallneg _ c x); clear c; simpl in q.
  exact (proof_by_contradiction lem q).

Lemma negimpl_to_conj (P Q:hProp) : LEM -> ( ¬ (P ⇒ Q ) -> P ∧ ¬ Q ).
Show proof.

intros lem ni. assert (r := negforall_to_existsneg _ lem ni); clear lem ni.
apply (squash_to_hProp r); clear r; intros [p nq]. exact (p,,nq).

Definition hrel_set (X : hSet) : hSet := make_hSet (hrel X) (isaset_hrel X).

Lemma isaprop_assume_it_is {X : UU} : (X -> isaprop X ) -> isaprop X.
Show proof.

intros f. apply invproofirrelevance; intros x y.
apply proofirrelevance. now apply f.

Lemma isaproptotal2 {X : UU} (P : X → UU) :
  isPredicate P →
  (∏ x y : X , P x → P y → x = y ) →
  isaprop (∑ x : X , P x).
Show proof.

  intros HP Heq.
  apply invproofirrelevance.
  intros [x p] [y q].
  induction (Heq x y p q).
  induction (iscontrpr1 (HP x p q)).
  apply idpath.

Lemma squash_rec {X : UU} (P : ∥ X ∥ -> hProp) : (∏ x , P (hinhpr x)) -> (∏ x , P x ).
Show proof.

  intros xp x'. simple refine (hinhuniv _ x'). intro x.
  assert (q : hinhpr x = x').
  { apply propproperty. }
  induction q. exact (xp x).

Goal ∏ {X :UU } {P :∥X ∥ -> hProp } (h : ∏ x , P (hinhpr x )) (x :X ),
squash_rec _ h (hinhpr x ) = h x.
Show proof.

  Fail reflexivity. Abort.

Goal ∏ (X :Type )
     (P := λ x':∥X ∥, ∃ x , (x' = hinhpr x ))
     (h := λ x , (hinhpr (x ,,idpath _) : P (hinhpr x )))
     (x :X ),
  squash_rec _ h (hinhpr x ) = h x.
Proof.
  Fail reflexivity. Abort.

Lemma logeq_if_both_true (P Q : hProp) : P -> Q -> ( P ⇔ Q ).
Proof.
  intros p q.
  split.
  - intros _. exact q.
  - intros _. exact p.

Lemma logeq_if_both_false (P Q : hProp) : ¬P -> ¬Q -> ( P ⇔ Q ).
Show proof.

  intros np nq.
  split.
  - intros p. apply fromempty. exact (np p).
  - intros q. apply fromempty. exact (nq q).

Definition proofirrelevance_hProp (X : hProp) : isProofIrrelevant X
  := proofirrelevance X (propproperty X).

Ltac induction_hProp x y := induction (proofirrelevance_hProp _ x y).

Definition iscontr_hProp (X:UU) : hProp := make_hProp (iscontr X) (isapropiscontr X).

Notation "'∃!' x .. y , P"
  := (iscontr_hProp (∑ x , .. (∑ y , P) ..))
       (at level 200, x binder, y binder, right associativity) : logic.

Various algebraic properties of hProp

Section hProp_logic.

We first state the algebraic properties as bi-implications

Lemma islogeqassochconj {P Q R : hProp} : (P ∧ Q ) ∧ R <-> P ∧ (Q ∧ R ).
Show proof.

split.
- intros PQR.
exact (pr1 (pr1 PQR),,(pr2 (pr1 PQR),,pr2 PQR)).
- intros PQR.
exact ((pr1 PQR,,pr1 (pr2 PQR)),,pr2 (pr2 PQR)).

Lemma islogeqcommhconj {P Q : hProp} : P ∧ Q <-> Q ∧ P.
Show proof.

split.
- intros PQ.
exact (pr2 PQ,,pr1 PQ).
- intros QP.
exact (pr2 QP,,pr1 QP).

Lemma islogeqassochdisj {P Q R : hProp} : (P ∨ Q ) ∨ R <-> P ∨ (Q ∨ R ).
Show proof.

split.
- apply hinhuniv; intros hPQR.
  induction hPQR as [hPQ|hR].
  + use (hinhuniv _ hPQ); clear hPQ; intros hPQ.
    induction hPQ as [hP|hQ].
    * exact (hinhpr (ii1 hP)).
    * exact (hinhpr (ii2 (hinhpr (ii1 hQ)))).
  + exact (hinhpr (ii2 (hinhpr (ii2 hR)))).
- apply hinhuniv; intros hPQR.
  induction hPQR as [hP|hQR].
  + exact (hinhpr (ii1 (hinhpr (ii1 hP)))).
  + use (hinhuniv _ hQR); clear hQR; intros hQR.
    induction hQR as [hQ|hR].
    * exact (hinhpr (ii1 (hinhpr (ii2 hQ)))).
    * exact (hinhpr (ii2 hR)).

Lemma islogeqhconj_absorb_hdisj {P Q : hProp} : P ∧ (P ∨ Q ) <-> P.
Show proof.

split.
- intros hPPQ; apply (pr1 hPPQ).
- intros hP.
split; [ apply hP | apply (hinhpr (ii1 hP)) ].

Lemma islogeqhdisj_absorb_hconj {P Q : hProp} : P ∨ (P ∧ Q ) <-> P.
Show proof.

split.
- apply hinhuniv; intros hPPQ.
  induction hPPQ as [hP|hPQ].
  + exact hP.
  + exact (pr1 hPQ).
- intros hP; apply (hinhpr (ii1 hP)).

Lemma islogeqhfalse_hdisj {P : hProp} : ∅ ∨ P <-> P.
Show proof.

split.
- apply hinhuniv; intros hPPQ.
  induction hPPQ as [hF|hP].
  + induction hF.
  + exact hP.
- intros hP; apply (hinhpr (ii2 hP)).

Lemma islogeqhhtrue_hconj {P : hProp} : htrue ∧ P <-> P.
Show proof.

split.
- intros hP; apply (pr2 hP).
- intros hP.
split; [ apply tt | apply hP ].

We now turn these into equalities using univalence for propositions

Lemma isassoc_hconj (P Q R : hProp) : ((P ∧ Q ) ∧ R ) = (P ∧ (Q ∧ R )).
Show proof.

now apply hPropUnivalence; apply islogeqassochconj.

Lemma iscomm_hconj (P Q : hProp) : (P ∧ Q ) = (Q ∧ P ).
Show proof.

now apply hPropUnivalence; apply islogeqcommhconj.

Lemma isassoc_hdisj (P Q R : hProp) : ((P ∨ Q ) ∨ R ) = (P ∨ (Q ∨ R )).
Show proof.

now apply hPropUnivalence; apply islogeqassochdisj.

Lemma iscomm_hdisj (P Q : hProp) : (P ∨ Q ) = (Q ∨ P ).
Show proof.

now apply hPropUnivalence; apply islogeqcommhdisj.

Lemma hconj_absorb_hdisj (P Q : hProp) : (P ∧ (P ∨ Q )) = P.
Show proof.

now apply hPropUnivalence; apply islogeqhconj_absorb_hdisj.

Lemma hdisj_absorb_hconj (P Q : hProp) : (P ∨ (P ∧ Q )) = P.
Show proof.

now apply hPropUnivalence; apply islogeqhdisj_absorb_hconj.

Lemma hfalse_hdisj (P : hProp) : (∅ ∨ P ) = P.
Show proof.

now apply hPropUnivalence; apply islogeqhfalse_hdisj.

Lemma htrue_hconj (P : hProp) : (htrue ∧ P ) = P.
Show proof.

now apply hPropUnivalence; apply islogeqhhtrue_hconj.

End hProp_logic.

Factoring maps through squash

Lemma squash_uniqueness {X} (x:X) (h:∥ X ∥) : squash_element x = h.
Show proof.

intros. apply propproperty.

Goal ∏ X Q (i :isaprop Q ) (f :X -> Q ) (x :X ),
factor_through_squash i f (squash_element x ) = f x.
Show proof.

reflexivity.

Lemma factor_dep_through_squash {X} {Q:∥ X ∥->UU} :
  (∏ h , isaprop (Q h)) ->
  (∏ x , Q(squash_element x)) ->
  (∏ h , Q h ).
Show proof.

intros i f ?. apply (h (make_hProp (Q h) (i h))).
intro x. simpl. induction (squash_uniqueness x h). exact (f x).

Lemma factor_through_squash_hProp {X} : ∏ hQ:hProp , (X -> hQ ) -> ∥ X ∥ -> hQ.
Show proof.

intros [Q i] f h. refine (h _ _). assumption.

Lemma funspace_isaset {X Y} : isaset Y -> isaset (X -> Y).
Show proof.

intros is. apply (impredfun 2). assumption.

Lemma squash_map_uniqueness {X S} (ip : isaset S) (g g' : ∥ X ∥ -> S) :
g ∘ squash_element ~ g' ∘ squash_element -> g ~ g'.
Show proof.

  intros h.
  set ( Q := λ y , g y = g' y ).
  unfold homot.
  apply (@factor_dep_through_squash X). intros y. apply ip.
  intro x. apply h.

Lemma squash_map_epi {X S} (ip : isaset S) (g g' : ∥ X ∥ -> S) :
g ∘ squash_element = g'∘ squash_element -> g = g'.
Show proof.

  intros e.
  apply funextsec.
  apply squash_map_uniqueness. exact ip.
  intro x. induction e. apply idpath.

Lemma uniqueExists {A : UU} {P : A -> UU} {a b : A}
(Hexists : ∃! a , P a) (Ha : P a) (Hb : P b) : a = b.
Show proof.

  assert (H : tpair _ _ Ha = tpair _ _ Hb).
  { now apply proofirrelevancecontr. }
  exact (base_paths _ _ H).

Connected types

Definition isConnected X : hProp := ∥ X ∥ ∧ ∀ (x y:X ), ∥ x = y ∥.

Lemma predicateOnConnectedType {X:Type} (i : isConnected X) {P:X ->hProp} (x0:X) (p:P x0) :
∏ x , P x.
Show proof.

intros x. apply (squash_to_hProp (pr2 i x x0)); intros e. now induction e.

Definition isBaseConnected (X:PointedType) : hProp := ∀ (y:X ), ∥ basepoint X = y ∥.

Lemma isConnected_isBaseConnected (X:PointedType) : isConnected X <-> isBaseConnected X.
Show proof.

  split.
  - intros [_ ic] x. use ic.
  - intros ibc. split.
    + exact (hinhpr (basepoint X)).
    + intros x y.
      apply (squash_to_hProp (ibc x)); intros p; apply (squash_to_hProp (ibc y)); intros q.
      exact (hinhpr (!p @ q)).

Definition BasePointComponent (X:PointedType) : PointedType :=
pointedType (∑ (y:X ), ∥ basepoint X = y ∥) (basepoint X ,, hinhpr (idpath (basepoint X))).

Definition basePointComponent_inclusion {X:PointedType} (x : BasePointComponent X) : X
:= pr1 x.

Lemma BasePointComponent_isBaseConnected (X:PointedType) : isBaseConnected (BasePointComponent X).
Show proof.

  intros [x' c'].
  change (basepoint (BasePointComponent X))
    with (tpair (λ (y:X), ∥ basepoint X = y ∥) (basepoint X) (hinhpr (idpath (basepoint X)))).
  use (hinhfun _ c'); intro q. induction q.
  apply maponpaths. apply propproperty.

Lemma BasePointComponent_isincl {X:PointedType} : isincl (@basePointComponent_inclusion X).
Show proof.

use isinclpr1. intros x. apply propproperty.

Lemma BasePointComponent_isweq {X:PointedType} (bc : isBaseConnected X) :
isweq (@basePointComponent_inclusion X).
Show proof.

  use isweqpr1.
  intros x.
  apply iscontraprop1.
  - apply propproperty.
  - exact (bc x).

Definition BasePointComponent_weq {X:PointedType} (bc : isBaseConnected X) :
BasePointComponent X ≃ X
:= make_weq (@basePointComponent_inclusion X) (BasePointComponent_isweq bc).

Lemma baseConnectedness X : isBaseConnected X -> isConnected X.
Show proof.

  intros p. split.
  - exact (hinhpr (basepoint X)).
  - intros x y. assert (a := p x); assert (b := p y); clear p.
    apply (squash_to_prop a); [apply propproperty|]; clear a; intros a.
    apply (squash_to_prop b); [apply propproperty|]; clear b; intros b.
    apply hinhpr. exact (!a@b).

Lemma predicateOnBaseConnectedType (X:PointedType) (b:isBaseConnected X)
(P:X ->hProp) (p:P (basepoint X)) :
∏ x , P x.
Show proof.

intros x. apply (squash_to_hProp (b x)); intros e. now induction e.

Goal ∏ (X :PointedType ) (b :isBaseConnected X ) (P :X ->hProp ) (p :P (basepoint X )),
predicateOnBaseConnectedType X b P p (basepoint X ) = p.
Show proof.

  Fail reflexivity.
  intros.
Abort.

Lemma predicateOnBasePointComponent
      (X:PointedType) (X' := BasePointComponent X) (pt' := basepoint X')
      (P:X'->hProp) (p:P pt') :
   ∏ x , P x.
Proof.
  intros x.
  apply (squash_to_hProp (BasePointComponent_isBaseConnected _ x)); intros e.
  now induction e.

Goal ∏ (X :PointedType )
     (X' := BasePointComponent X ) (pt' := basepoint X')
     (P :X'->hProp ) (p :P pt'),
   predicateOnBasePointComponent X P p pt' = p.
Show proof.

  Fail reflexivity.
  intros.
  unfold pt', basepoint, X', BasePointComponent, pointedType, pr2; cbn beta.
Abort.