Apartness in sets with decidable equality (axiom removal)

[DanGrayson]

Consider the natural problem of proving that Σ i, i≠0 and Σ i, i>0 are
equivalent sets. The former set is the complement of 0 in nat, as encapsulated
in the following definition from PartC:

Definition compl (X:UU) (x:X):= Σ x', x ≠ x'.

One easily defines functions in both directions:

p : Σ i, i≠0 -> Σ i, i>0
q : Σ i, i≠0 <- Σ i, i>0

, but then one has to prove that the two composite functions are homotopic to
identity functions, and there one uses the lemmas that show that i≠0 and
i>0 are propositions. The proof that i≠0 is a proposition involves an
axiom, because i≠0 is defined as i=0 -> empty. The axiom funextempty
provides the needed statement:

Axiom funextempty : ∀ (X:UU) (f g : X->empty), f = g. 

Use of that axiom makes its way into the definition of the homotopy
q∘p ~ idfun _, rendering it incomputable. Such homotopies are provided from
any weak equivalence by these functions:

Definition homotweqinvweq {X Y : UU} (w : X ≃ Y) : ∀ y : Y, w (invmap w y) = y.
Definition homotinvweqweq {X Y : UU} (w : X ≃ Y) : ∀ x : X, x = invmap w (w x).

Those homotopies, in turn, make their way into definitions of other maps
and equivalences, rendering them incomputable. For example, consider weqfp,
a useful theorem:

Definition weqfp {X Y : UU} (w : X ≃ Y) (P:Y->UU) : (Σ x : X, P (w x)) ≃ (Σ y, P y).

, where one of the two maps in the equivalence it provides incorporates one of
those potentially incomputable homotopies:

Definition weqfp_invmap { X Y : UU } ( w : X ≃ Y ) (P:Y->UU) : (Σ y, P y) -> (Σ x,P(w x)).
Proof.
  intros ? ? ? ? yp.
  exact (invmap w (pr1 yp),,transportf P (! homotweqinvweq w (pr1 yp)) (pr2 yp)).
Defined.

The route for the propagation of incomputability passes through the following
basic lemma:

Theorem isapropneg (X:UU): isaprop (neg X).
Proof. intro.  apply invproofirrelevance . intros x x' .   apply ( funextempty X x x' ) . Defined .  

, which gets used in the proof of

Theorem isweqrecompl (X:UU)(x:X) (is:isisolated X x): isweq (recompl _ x).

, where recompl is defined this way:

Definition recompl (X:UU) (x:X): compl X x ⨿ unit -> X
  := fun u:_ =>
       match u with
         | ii1 x0 => pr1  x0
         | ii2 t => x
       end.

From there incomputability is transferred into

Definition weqrecompl (X : UU) (x:X) (is:isisolated _ x): compl X x ⨿ unit ≃ X.

and thus into

Definition weqdnicoprod n (j : stn(S n)) : stn n ⨿ unit ≃ stn (S n).

This is unfortunate, because any stn m has an axiom-free proposition
equivalent to x≠y, given by the evident recursive algorithm on nat, which
could have been used instead to define the complement of a set! Yesterday I
started rewriting weqdnicoprod, but this morning I realized there is a better
way, which preserves all the theorems already proved.

I would like to fix this by postponing the decision to appeal to funextempty:

We redefine

Definition isisolated (X:UU) (x:X):= ∀ x':X, x=x' ⨿ x≠x'.

as

Definition isisolated (X:UU) (x:X):=
   Σ (P:X->hProp), ∀ (x':X), iscontr( x=x' ⨿ P x' ).

Using funextempty, one can show that P x' and x=x' are equivalent.
A suitable name for P would be "apartness from x". Similarly, we would redefine

Definition isdecprop ( X : UU ) := iscontr ( X ⨿ ¬ X ).

, any of whose applications would involve funextempty, as

Definition isdecprop (Q:UU) := Σ P:hProp, iscontr ( Q ⨿ P ).

or as

Definition isdecprop (Q:hProp) := Σ P:hProp, iscontr ( Q ⨿ P ).

, and redefine

Definition isdeceq (X:UU) : UU := ∀ (x x':X), (x=x') ⨿ (x!=x').

as

Definition isdeceq (X:UU) : UU :=
   Σ P:X->X->hProp, ∀ (x x':X), iscontr ( x=x' ⨿ P x x' ).

A suitable name for such a P would be "apartness on X". We could even make
the following definition:

Definition isApartness (X:UU) (P:X->X->hProp) :=
   ∀ (x x':X), iscontr ( x=x' ⨿ P x x' ).

Similarly, the P in isdecprop above could be called "a complement of X",
and we could adopt this definition:

Definition areComplementary Q P := iscontr ( Q ⨿ P ).

We could then also, more simply, define isisolated and isdeceq in terms of
isdecprop.

Notice that under this proposal, even though theorems are seemingly weakened,
we lose nothing, because a user of the new definitions is always free to appeal
to funextempty if necessary. In that way, it's just like postponing the use
of LEM until it's needed, by refraining from adopting it as axiom, and
insisting it be used as a hypothesis.

Let me know what you think. I'd like to start working on it immediately, since
it seems necessary.

[DanGrayson]

PS: Another way to bring out the essence of the issue is to point out that the equivalence ¬unit ≃ empty can be established constructively, but proving the equivalence unit ≃ ¬empty requires funextempty. One should simply avoid using negations of propositions, or one will lose computability. Inequality is a negation, hence the need for apartness, even in discrete situations.

[DanGrayson]

PPS: Another proposition defined as a negation and in use by us is the relation
m≤n on nat, defined by

Definition natleh ( n m : nat ) := hProppair ( neg ( natgth n m ) ) ( isapropneg _ )  .
Definition natgeh ( n m : nat ) : hProp := hProppair ( neg ( natgth m n ) ) ( isapropneg _ ) .

We'll have to change that, too. It's easy, because m ≤ n is equivalent to m < S n, which is not a negation.

[DanGrayson]

Here is the branch I will use:
https://github.com/DanGrayson/UniMath/tree/postponing-use-of-funextempty

[cathlelay]

I began to work on apartness the last week : https://github.com/cathlelay/UniMath/blob/dev/UniMath/Dedekind/Apartness.v
I will do a pull request for apartness and division rigs.

[DanGrayson]

I see you use isapropneg once. It should be avoided.

On Mon, Nov 2, 2015 at 9:07 AM, cathlelay notifications@github.com wrote:

I began to work on apartness the last week :
https://github.com/cathlelay/UniMath/blob/dev/UniMath/Dedekind/Apartness.v
https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_cathlelay_UniMath_blob_dev_UniMath_Dedekind_Apartness.v&d=BQMCaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=PAZ_jTPLrSb1btCfAu4RkycWe57N0sGyzbjgeOn2wN0&m=sld8s229YglDis_f5quy0eTknCJy9yJDPZ62JeHf-2E&s=LXmfCOV2iU68Z3uj222pH7-Bt7p-fB7uIVekktZO3cE&e=
I will do a pull request for apartness and division rigs.

—
Reply to this email directly or view it on GitHub
https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_UniMath_UniMath_issues_227-23issuecomment-2D153025644&d=BQMCaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=PAZ_jTPLrSb1btCfAu4RkycWe57N0sGyzbjgeOn2wN0&m=sld8s229YglDis_f5quy0eTknCJy9yJDPZ62JeHf-2E&s=aO34xX-UW80WUrEXEVBw8pYANoZ5Le7hf_D6pl-BZPA&e=
.

[DanGrayson]

Hmm, on second thought, maybe it's unnecessary to avoid it in your
context. I'm not sure.

On Mon, Nov 2, 2015 at 9:10 AM, Daniel R. Grayson dan@math.uiuc.edu wrote:

I see you use isapropneg once. It should be avoided.

On Mon, Nov 2, 2015 at 9:07 AM, cathlelay notifications@github.com
wrote:

I began to work on apartness the last week :
https://github.com/cathlelay/UniMath/blob/dev/UniMath/Dedekind/Apartness.v
https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_cathlelay_UniMath_blob_dev_UniMath_Dedekind_Apartness.v&d=BQMCaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=PAZ_jTPLrSb1btCfAu4RkycWe57N0sGyzbjgeOn2wN0&m=sld8s229YglDis_f5quy0eTknCJy9yJDPZ62JeHf-2E&s=LXmfCOV2iU68Z3uj222pH7-Bt7p-fB7uIVekktZO3cE&e=
I will do a pull request for apartness and division rigs.

—
Reply to this email directly or view it on GitHub
https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_UniMath_UniMath_issues_227-23issuecomment-2D153025644&d=BQMCaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=PAZ_jTPLrSb1btCfAu4RkycWe57N0sGyzbjgeOn2wN0&m=sld8s229YglDis_f5quy0eTknCJy9yJDPZ62JeHf-2E&s=aO34xX-UW80WUrEXEVBw8pYANoZ5Le7hf_D6pl-BZPA&e=
.

[DanGrayson]

I see that the HoTT formalization avoids this problem. Here is their definition of decidability:

Class Decidable (P : Prop) := {
  Decidable_witness : bool;
  Decidable_spec : Decidable_witness = true <-> P
}.

It follows that P is equivalent to Decidable_witness = true and ¬P is equivalent to Decidable_witness = false, so the complementary proposition is built in.

[DanGrayson]

Here's how to say what an apartness relation is, in a nutshell: it's an axiom-free propositional relation that is equivalent, by a proof using consistent axioms, such as LEM, funextfun, or univalence, to x ≠ y.

[DanGrayson]

One more point is that if the user needs a complement P for x=y, then the type x ≠ y is available, and funextempty is available to the user to prove it's a proposition.

[benediktahrens]

On 11/02/2015 11:09 AM, Daniel R. Grayson wrote:

Here's how to say what an apartness relation is, in a nutshell: it's
an axiom-free-propositional relation that is equivalent, by a proof
using consistent axioms, such as LEM, funextfun, or univalence,
to x ≠ y.

Ok, that sounds reasonable!

[andrejbauer]

Here's how to say what an apartness relation is, in a nutshell: it's an axiom-free propositional relation that is equivalent, by a proof using consistent axioms, such as LEM, funextfun, or univalence, to x ≠ y.

I believe that's the same as "apartness is a propostional relation which cannot be shown different from ≠ (no matter what axioms we have, including none, as long as they are consistent)."

[DanGrayson]

Maybe. One way I can imagine proving that apartness differing from inequality is inconsistent would be by proving ∀ x y, ¬ ((x ≠ y ∧ ¬ x # y) ∨ (¬ x ≠ y ∧ x # y)). Perhaps there are no other ways, essentially.