Library UniMath.MoreFoundations.NegativePropositions
Definition negProp P := ∑ Q, isaprop Q × (¬P <-> Q).
Definition negProp_to_isaprop {P} (nP : negProp P) : isaprop (pr1 nP)
:= pr1 (pr2 nP).
Definition negProp_to_hProp {P : UU} (Q : negProp P) : hProp.
Show proof.
Coercion negProp_to_hProp : negProp >-> hProp.
Definition negProp_to_iff {P} (nP : negProp P) : ¬P <-> nP
:= pr2 (pr2 nP).
Definition negProp_to_neg {P} {nP : negProp P} : nP -> ¬P.
Show proof.
Coercion negProp_to_neg : negProp >-> Funclass.
Definition neg_to_negProp {P} {nP : negProp P} : ¬P -> nP.
Show proof.
Definition negPred {X:UU} (x :X) (P:∏ y:X, UU) := ∏ y , negProp (P y).
Definition negReln {X:UU} (P:∏ (x y:X), UU) := ∏ x y, negProp (P x y).
Definition neqProp {X:UU} (x y:X) := negProp (x=y).
Definition neqPred {X:UU} (x :X) := ∏ y, negProp (x=y).
Definition neqReln (X:UU) := ∏ (x y:X), negProp (x=y).
Lemma negProp_to_complementary P : ∏ (Q : negProp P), P ⨿ Q <-> complementary P Q.
Show proof.
intros [Q [i [r s]]]; simpl in *.
split.
* intros pq. split.
- intros p q. apply s.
+ assumption.
+ assumption.
- assumption.
* intros [j c].
assumption.
split.
* intros pq. split.
- intros p q. apply s.
+ assumption.
+ assumption.
- assumption.
* intros [j c].
assumption.
Lemma negProp_to_uniqueChoice P : ∏ (Q:negProp P), (isaprop P × (P ⨿ Q)) <-> iscontr (P ⨿ Q).
Show proof.
intros [Q [j [r s]]]; simpl in *. split.
* intros [i v]. exists v. intro w.
induction v as [v|v].
- induction w as [w|w].
+ apply maponpaths, i.
+ contradicts (s w) v.
- induction w as [w|w].
+ contradicts (s v) w.
+ apply maponpaths, j.
* intros [c e]. split.
- induction c as [c|c].
+ apply invproofirrelevance; intros p p'.
exact (equality_by_case (e (ii1 p) @ !e (ii1 p'))).
+ apply invproofirrelevance; intros p p'.
contradicts (s c) p.
- exact c.
* intros [i v]. exists v. intro w.
induction v as [v|v].
- induction w as [w|w].
+ apply maponpaths, i.
+ contradicts (s w) v.
- induction w as [w|w].
+ contradicts (s v) w.
+ apply maponpaths, j.
* intros [c e]. split.
- induction c as [c|c].
+ apply invproofirrelevance; intros p p'.
exact (equality_by_case (e (ii1 p) @ !e (ii1 p'))).
+ apply invproofirrelevance; intros p p'.
contradicts (s c) p.
- exact c.
Rework some foundational material using negative propositions.
Definition isisolated_ne (X:UU) (x:X) (neq_x:neqPred x) := ∏ y:X, (x=y) ⨿ neq_x y.
Definition isisolated_to_isisolated_ne {X x neq_x} :
isisolated X x -> isisolated_ne X x neq_x.
Show proof.
intros i y. induction (i y) as [eq|ne].
- exact (ii1 eq).
- apply ii2. apply neg_to_negProp. assumption.
- exact (ii1 eq).
- apply ii2. apply neg_to_negProp. assumption.
Definition isisolated_ne_to_isisolated {X x neq_x} :
isisolated_ne X x neq_x -> isisolated X x.
Show proof.
intros i y. induction (i y) as [eq|ne].
- exact (ii1 eq).
- apply ii2. use negProp_to_neg.
+ exact (neq_x y).
+ exact ne.
- exact (ii1 eq).
- apply ii2. use negProp_to_neg.
+ exact (neq_x y).
+ exact ne.
Definition isolated_ne ( T : UU ) (neq:neqReln T) := ∑ t:T, isisolated_ne _ t (neq t).
Definition make_isolated_ne (T : UU) (t:T) (neq:neqReln T) (i:isisolated_ne _ t (neq t)) :
isolated_ne T neq
:= (t,,i).
Definition pr1isolated_ne ( T : UU ) (neq:neqReln T) (x:isolated_ne T neq) : T := pr1 x.
Theorem isaproppathsfromisolated_ne (X : UU) (x : X) (neq_x : neqPred x)
(is : isisolated_ne X x neq_x) (y : X)
: isaprop (x = y).
Show proof.
intros. unfold isisolated_ne in is. apply invproofirrelevance; intros m n.
set (Q y := (x = y) ⨿ (neq_x y)).
assert (a := (transport_section is m) @ !(transport_section is n)).
induction (is x) as [j|k].
- assert (b := transport_map (λ y p, ii1 p : Q y) m j); simpl in b;
assert (c := transport_map (λ y p, ii1 p : Q y) n j); simpl in c.
assert (d := equality_by_case (!b @ a @ c)); simpl in d.
rewrite 2? transportf_id1 in d. apply (pathscomp_cancel_left j). assumption.
- contradicts (neq_x x k) (idpath x).
set (Q y := (x = y) ⨿ (neq_x y)).
assert (a := (transport_section is m) @ !(transport_section is n)).
induction (is x) as [j|k].
- assert (b := transport_map (λ y p, ii1 p : Q y) m j); simpl in b;
assert (c := transport_map (λ y p, ii1 p : Q y) n j); simpl in c.
assert (d := equality_by_case (!b @ a @ c)); simpl in d.
rewrite 2? transportf_id1 in d. apply (pathscomp_cancel_left j). assumption.
- contradicts (neq_x x k) (idpath x).
Definition compl_ne (X:UU) (x:X) (neq_x : neqPred x) := ∑ y, neq_x y.
Definition make_compl_ne (X : UU) (x : X) (neq_x : neqPred x) (y : X)
(ne :neq_x y) :
compl_ne X x neq_x := (y,,ne).
Definition pr1compl_ne (X : UU) (x : X) (neq_x : neqPred x)
(c : compl_ne X x neq_x) :
X := pr1 c.
Definition make_negProp {P : UU} : negProp P.
Show proof.
Definition make_neqProp {X : UU} (x y : X) : neqProp x y.
Show proof.
Lemma isinclpr1compl_ne (X : UU) (x : X) (neq_x : neqPred x) :
isincl (pr1compl_ne X x neq_x).
Show proof.
Lemma compl_ne_weq_compl (X : UU) (x : X) (neq_x : neqPred x) :
compl X x ≃ compl_ne X x neq_x.
Show proof.
intros. apply weqfibtototal; intro y. apply weqiff.
- apply negProp_to_iff.
- apply isapropneg.
- apply negProp_to_isaprop.
- apply negProp_to_iff.
- apply isapropneg.
- apply negProp_to_isaprop.
Lemma compl_weq_compl_ne (X : UU) (x : X) (neq_x : neqPred x) :
compl_ne X x neq_x ≃ compl X x.
Show proof.
intros. apply weqfibtototal; intro y. apply weqiff.
- apply issymm_logeq. apply negProp_to_iff.
- apply negProp_to_isaprop.
- apply isapropneg.
- apply issymm_logeq. apply negProp_to_iff.
- apply negProp_to_isaprop.
- apply isapropneg.
Definition recompl_ne (X : UU) (x : X) (neq_x:neqPred x) :
compl_ne X x neq_x ⨿ unit -> X.
Show proof.
Definition maponcomplincl_ne {X Y : UU} (f : X -> Y) (is : isincl f) (x : X)
(neq_x : neqPred x) (neq_fx : neqPred (f x))
: compl_ne X x neq_x -> compl_ne Y (f x) neq_fx.
Show proof.
intros c.
set (x' := pr1 c).
set (neqx := pr2 c).
exact (f x',,neg_to_negProp (nP := neq_fx (f x'))
(negf (invmaponpathsincl _ is x x') (negProp_to_neg neqx))).
set (x' := pr1 c).
set (neqx := pr2 c).
exact (f x',,neg_to_negProp (nP := neq_fx (f x'))
(negf (invmaponpathsincl _ is x x') (negProp_to_neg neqx))).
Definition weqoncompl_ne {X Y : UU} (w : X ≃ Y) (x : X) (neq_x : neqPred x)
(neq_wx : neqPred (w x))
: compl_ne X x neq_x ≃ compl_ne Y (w x) neq_wx.
Show proof.
intros. intermediate_weq (∑ x', neq_wx (w x')).
- apply weqfibtototal; intro x'.
apply weqiff.
{apply (logeq_trans (Y := x != x')).
{apply issymm_logeq, negProp_to_iff. }
apply (logeq_trans (Y := w x != w x')).
{apply logeqnegs. apply weq_to_iff. apply weqonpaths. }
apply negProp_to_iff. }
{apply negProp_to_isaprop. }
{apply negProp_to_isaprop. }
- refine (weqfp _ _).
- apply weqfibtototal; intro x'.
apply weqiff.
{apply (logeq_trans (Y := x != x')).
{apply issymm_logeq, negProp_to_iff. }
apply (logeq_trans (Y := w x != w x')).
{apply logeqnegs. apply weq_to_iff. apply weqonpaths. }
apply negProp_to_iff. }
{apply negProp_to_isaprop. }
{apply negProp_to_isaprop. }
- refine (weqfp _ _).
Definition weqoncompl_ne_compute {X Y : UU}
(w : X ≃ Y) (x : X) (neq_x : neqPred x) (neq_wx : neqPred (w x)) x' :
pr1 (weqoncompl_ne w x neq_x neq_wx x') = w (pr1 x').
Show proof.
Definition invrecompl_ne (X : UU) (x : X) (neq_x : neqPred x)
(is : isisolated X x) : X -> compl_ne X x neq_x ⨿ unit.
Show proof.
intros y. induction (is y) as [k|k].
- exact (ii2 tt).
- exact (ii1 (make_compl_ne X x neq_x y (neg_to_negProp k))).
- exact (ii2 tt).
- exact (ii1 (make_compl_ne X x neq_x y (neg_to_negProp k))).
Theorem isweqrecompl_ne (X : UU) (x : X) (is : isisolated X x)
(neq_x : neqPred x) : isweq (recompl_ne _ x neq_x).
Show proof.
intros.
set (f := recompl_ne X x neq_x). set (g := invrecompl_ne X x neq_x is).
refine (isweq_iso f g _ _).
{intro u. induction (is (f u)) as [ eq | ne ].
- induction u as [ c | u].
+ simpl. induction c as [ t neq ]; simpl; simpl in eq.
contradicts (negProp_to_neg neq) eq.
+ induction u.
intermediate_path (g x).
{apply maponpaths. exact (pathsinv0 eq). }
{unfold g, invrecompl_ne. induction (is x) as [ i | e ].
{apply idpath. }
{simpl. contradicts e (idpath x). }}
- induction u as [ c | u ]. simpl.
+ induction c as [ y neq ]; simpl. unfold g, invrecompl_ne.
induction (is y) as [ eq' | ne' ].
{contradicts (negProp_to_neg neq) eq'. }
{induction (ii2 ne') as [eq|neq'].
{simpl. contradicts eq ne'. }
{simpl. apply maponpaths. unfold make_compl_ne. apply maponpaths.
apply proofirrelevance. exact (pr1 (pr2 (neq_x y))). }}
+ induction u. unfold f,g,invrecompl_ne;simpl.
induction (is x) as [eq|neq].
{simpl. apply idpath. }
{apply fromempty. apply neq. apply idpath. }}
{intro y. unfold f,g,invrecompl_ne;simpl.
induction (is y) as [eq|neq].
- induction eq. apply idpath.
- simpl. apply idpath. }
set (f := recompl_ne X x neq_x). set (g := invrecompl_ne X x neq_x is).
refine (isweq_iso f g _ _).
{intro u. induction (is (f u)) as [ eq | ne ].
- induction u as [ c | u].
+ simpl. induction c as [ t neq ]; simpl; simpl in eq.
contradicts (negProp_to_neg neq) eq.
+ induction u.
intermediate_path (g x).
{apply maponpaths. exact (pathsinv0 eq). }
{unfold g, invrecompl_ne. induction (is x) as [ i | e ].
{apply idpath. }
{simpl. contradicts e (idpath x). }}
- induction u as [ c | u ]. simpl.
+ induction c as [ y neq ]; simpl. unfold g, invrecompl_ne.
induction (is y) as [ eq' | ne' ].
{contradicts (negProp_to_neg neq) eq'. }
{induction (ii2 ne') as [eq|neq'].
{simpl. contradicts eq ne'. }
{simpl. apply maponpaths. unfold make_compl_ne. apply maponpaths.
apply proofirrelevance. exact (pr1 (pr2 (neq_x y))). }}
+ induction u. unfold f,g,invrecompl_ne;simpl.
induction (is x) as [eq|neq].
{simpl. apply idpath. }
{apply fromempty. apply neq. apply idpath. }}
{intro y. unfold f,g,invrecompl_ne;simpl.
induction (is y) as [eq|neq].
- induction eq. apply idpath.
- simpl. apply idpath. }
Theorem isweqrecompl_ne' (X : UU) (x : X) (is : isisolated X x)
(neq_x : neqPred x) : isweq (recompl_ne _ x neq_x).
Show proof.
intros. set (f := recompl_ne X x neq_x). intro y.
unfold neqPred,negProp in neq_x; unfold isisolated in is.
apply (iscontrweqb (weqtotal2overcoprod _)). induction (is y) as [eq|ne].
{induction eq. refine (iscontrweqf (weqii2withneg _ _) _).
{intros z; induction z as [z e]; induction z as [z neq]; simpl in *.
contradicts (!e) (negProp_to_neg neq). }
{change x with (f (ii2 tt)). simple refine ((_,,_),,_).
{exact tt. }
{apply idpath. }
{intro w. induction w as [t e]. unfold f in *; simpl in *. induction t.
apply maponpaths. apply isaproppathsfromisolated. exact is. }}}
{refine (iscontrweqf (weqii1withneg _ _) _).
{intros z; induction z as [z e]; simpl in *. contradicts ne e. }
{simple refine ((_,,_),,_).
{exists y. apply neg_to_negProp. assumption. }
{simpl. apply idpath. }
intros z; induction z as [z e]; induction z as [z neq];
induction e; simpl in *.
induction (proofirrelevance _ (pr1 (pr2 (neq_x z))) neq
(neg_to_negProp ne)).
apply idpath.
}}
unfold neqPred,negProp in neq_x; unfold isisolated in is.
apply (iscontrweqb (weqtotal2overcoprod _)). induction (is y) as [eq|ne].
{induction eq. refine (iscontrweqf (weqii2withneg _ _) _).
{intros z; induction z as [z e]; induction z as [z neq]; simpl in *.
contradicts (!e) (negProp_to_neg neq). }
{change x with (f (ii2 tt)). simple refine ((_,,_),,_).
{exact tt. }
{apply idpath. }
{intro w. induction w as [t e]. unfold f in *; simpl in *. induction t.
apply maponpaths. apply isaproppathsfromisolated. exact is. }}}
{refine (iscontrweqf (weqii1withneg _ _) _).
{intros z; induction z as [z e]; simpl in *. contradicts ne e. }
{simple refine ((_,,_),,_).
{exists y. apply neg_to_negProp. assumption. }
{simpl. apply idpath. }
intros z; induction z as [z e]; induction z as [z neq];
induction e; simpl in *.
induction (proofirrelevance _ (pr1 (pr2 (neq_x z))) neq
(neg_to_negProp ne)).
apply idpath.
}}
Definition weqrecompl_ne (X : UU) (x : X) (is : isisolated X x)
(neq_x : neqPred x) : compl_ne X x neq_x ⨿ unit ≃ X
:= make_weq _ (isweqrecompl_ne X x is neq_x).
Theorem isweqrecompl' (X : UU) (x : X) (is : isisolated X x) :
isweq (recompl _ x).
Show proof.
intros. set (neq_x := λ y, make_neqProp x y).
apply (isweqhomot (weqrecompl_ne X x is neq_x
∘ weqcoprodf (compl_ne_weq_compl X x neq_x)
(idweq unit))%weq).
{intro y. induction y as [y|t]; apply idpath. }
apply weqproperty.
apply (isweqhomot (weqrecompl_ne X x is neq_x
∘ weqcoprodf (compl_ne_weq_compl X x neq_x)
(idweq unit))%weq).
{intro y. induction y as [y|t]; apply idpath. }
apply weqproperty.
Lemma iscotrans_to_istrans_negReln {X : UU} {R : hrel X} (NR : negReln R) :
isdeccotrans R -> istrans NR.
Show proof.
intros i ? ? ? nxy nyz. apply neg_to_negProp.
apply (negf (i x1 x2 x3)). intro c. induction c as [c|c].
- exact (negProp_to_neg nxy c).
- exact (negProp_to_neg nyz c).
apply (negf (i x1 x2 x3)). intro c. induction c as [c|c].
- exact (negProp_to_neg nxy c).
- exact (negProp_to_neg nyz c).
Definition natneq (m n : nat) : negProp (m = n).
Show proof.
Notation " x ≠ y " := (natneq x y) (at level 70, no associativity) : nat_scope.
Definition nat_compl (i : nat) := compl_ne _ i (λ j, i ≠ j).
Theorem weqdicompl (i : nat) : nat ≃ nat_compl i.
Show proof.
use weq_iso.
- intro j. exists (di i j). apply di_neq_i.
- intro j. exact (si i (pr1 j)).
- simpl. intro j. unfold di. induction (natlthorgeh j i) as [lt|ge].
+ unfold si. induction (natlthorgeh i j) as [lt'|ge'].
* contradicts (isasymmnatlth _ _ lt') lt.
* apply idpath.
+ unfold si. induction (natlthorgeh i (S j)) as [lt'|ge'].
* change (S j) with (1 + j). rewrite natpluscomm. apply plusminusnmm.
* unfold natgeh,natleh in ge. contradicts (natlehneggth ge') ge.
- simpl. intro j. induction j as [j ne]; simpl.
apply subtypePath.
+ intro k. apply negProp_to_isaprop.
+ simpl. unfold si. induction (natlthorgeh j i) as [lt|ge].
* clear ne.
induction (natlthorgeh i j) as [lt'|_].
{ contradicts (isasymmnatlth _ _ lt') lt. }
{ unfold di. induction (natlthorgeh j i) as [lt'|ge'].
- apply idpath.
- contradicts (natgehtonegnatlth _ _ ge') lt. }
* assert (lt := natleh_neq ge ne); clear ne ge.
induction (natlthorgeh i j) as [_|ge'].
{ unfold di. induction (natlthorgeh (j - 1) i) as [lt'|ge'].
- apply fromempty. induction j as [|j _].
+ exact (negnatlthn0 _ lt).
+ change (S j) with (1 + j) in lt'.
rewrite natpluscomm in lt'.
rewrite plusminusnmm in lt'.
change (i < S j) with (i ≤ j) in lt.
exact (natlehneggth lt lt').
- induction j as [|j _].
+ contradicts (negnatlthn0 i) lt.
+ simpl. apply maponpaths. apply natminuseqn. }
contradicts (natgehtonegnatlth _ _ ge') lt.
- intro j. exists (di i j). apply di_neq_i.
- intro j. exact (si i (pr1 j)).
- simpl. intro j. unfold di. induction (natlthorgeh j i) as [lt|ge].
+ unfold si. induction (natlthorgeh i j) as [lt'|ge'].
* contradicts (isasymmnatlth _ _ lt') lt.
* apply idpath.
+ unfold si. induction (natlthorgeh i (S j)) as [lt'|ge'].
* change (S j) with (1 + j). rewrite natpluscomm. apply plusminusnmm.
* unfold natgeh,natleh in ge. contradicts (natlehneggth ge') ge.
- simpl. intro j. induction j as [j ne]; simpl.
apply subtypePath.
+ intro k. apply negProp_to_isaprop.
+ simpl. unfold si. induction (natlthorgeh j i) as [lt|ge].
* clear ne.
induction (natlthorgeh i j) as [lt'|_].
{ contradicts (isasymmnatlth _ _ lt') lt. }
{ unfold di. induction (natlthorgeh j i) as [lt'|ge'].
- apply idpath.
- contradicts (natgehtonegnatlth _ _ ge') lt. }
* assert (lt := natleh_neq ge ne); clear ne ge.
induction (natlthorgeh i j) as [_|ge'].
{ unfold di. induction (natlthorgeh (j - 1) i) as [lt'|ge'].
- apply fromempty. induction j as [|j _].
+ exact (negnatlthn0 _ lt).
+ change (S j) with (1 + j) in lt'.
rewrite natpluscomm in lt'.
rewrite plusminusnmm in lt'.
change (i < S j) with (i ≤ j) in lt.
exact (natlehneggth lt lt').
- induction j as [|j _].
+ contradicts (negnatlthn0 i) lt.
+ simpl. apply maponpaths. apply natminuseqn. }
contradicts (natgehtonegnatlth _ _ ge') lt.