{"action":"created","issue":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/227","labels_url":"https://api.github.com/repos/UniMath/UniMath/issues/227/labels{/name}","comments_url":"https://api.github.com/repos/UniMath/UniMath/issues/227/comments","events_url":"https://api.github.com/repos/UniMath/UniMath/issues/227/events","html_url":"https://github.com/UniMath/UniMath/issues/227","id":114592100,"number":227,"title":"Apartness in sets with decidable equality (axiom removal)","user":{"login":"DanGrayson","id":700228,"avatar_url":"https://avatars.githubusercontent.com/u/700228?v=3","gravatar_id":"","url":"https://api.github.com/users/DanGrayson","html_url":"https://github.com/DanGrayson","followers_url":"https://api.github.com/users/DanGrayson/followers","following_url":"https://api.github.com/users/DanGrayson/following{/other_user}","gists_url":"https://api.github.com/users/DanGrayson/gists{/gist_id}","starred_url":"https://api.github.com/users/DanGrayson/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/DanGrayson/subscriptions","organizations_url":"https://api.github.com/users/DanGrayson/orgs","repos_url":"https://api.github.com/users/DanGrayson/repos","events_url":"https://api.github.com/users/DanGrayson/events{/privacy}","received_events_url":"https://api.github.com/users/DanGrayson/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-11-02T13:20:06Z","updated_at":"2015-11-02T13:39:42Z","closed_at":"2015-11-02T13:39:42Z","body":"Consider the natural problem of proving that `Σ i, i≠0` and `Σ i, i>0` are\r\nequivalent sets.  The former set is the complement of `0` in `nat`, as encapsulated\r\nin the following definition from PartC:\r\n```\r\nDefinition compl (X:UU) (x:X):= Σ x', x ≠ x'.\r\n```\r\nOne easily defines functions in both directions:\r\n```\r\np : Σ i, i≠0 -> Σ i, i>0\r\nq : Σ i, i≠0 <- Σ i, i>0\r\n```\r\n\r\n, but then one has to prove that the two composite functions are homotopic to\r\nidentity functions, and there one uses the lemmas that show that `i≠0` and\r\n`i>0` are propositions.  The proof that `i≠0` is a proposition involves an\r\naxiom, because `i≠0` is defined as `i=0 -> empty`.  The axiom `funextempty`\r\nprovides the needed statement:\r\n\r\n```\r\nAxiom funextempty : ∀ (X:UU) (f g : X->empty), f = g. \r\n```\r\n\r\nUse of that axiom makes its way into the definition of the homotopy\r\n`q∘p ~ idfun _`, rendering it incomputable.  Such homotopies are provided from\r\nany weak equivalence by these functions:\r\n\r\n```\r\nDefinition homotweqinvweq {X Y : UU} (w : X ≃ Y) : ∀ y : Y, w (invmap w y) = y.\r\nDefinition homotinvweqweq {X Y : UU} (w : X ≃ Y) : ∀ x : X, x = invmap w (w x).\r\n```\r\nThose homotopies, in turn, make their way into definitions of other maps\r\nand equivalences, rendering them incomputable.  For example, consider `weqfp`,\r\na useful theorem:\r\n```\r\nDefinition weqfp {X Y : UU} (w : X ≃ Y) (P:Y->UU) : (Σ x : X, P (w x)) ≃ (Σ y, P y).\r\n```\r\n, where one of the two maps in the equivalence it provides incorporates one of\r\nthose potentially incomputable homotopies:\r\n```\r\nDefinition weqfp_invmap { X Y : UU } ( w : X ≃ Y ) (P:Y->UU) : (Σ y, P y) -> (Σ x,P(w x)).\r\nProof.\r\n  intros ? ? ? ? yp.\r\n  exact (invmap w (pr1 yp),,transportf P (! homotweqinvweq w (pr1 yp)) (pr2 yp)).\r\nDefined.\r\n```\r\nThe route for the propagation of incomputability passes through the following\r\nbasic lemma:\r\n```\r\nTheorem isapropneg (X:UU): isaprop (neg X).\r\nProof. intro.  apply invproofirrelevance . intros x x' .   apply ( funextempty X x x' ) . Defined .  \r\n```\r\n, which gets used in the proof of\r\n```\r\nTheorem isweqrecompl (X:UU)(x:X) (is:isisolated X x): isweq (recompl _ x).\r\n```\r\n, where `recompl` is defined this way:\r\n```\r\nDefinition recompl (X:UU) (x:X): compl X x ⨿ unit -> X\r\n  := fun u:_ =>\r\n       match u with\r\n         | ii1 x0 => pr1  x0\r\n         | ii2 t => x\r\n       end.\r\n```\r\nFrom there incomputability is transferred into\r\n```\r\nDefinition weqrecompl (X : UU) (x:X) (is:isisolated _ x): compl X x ⨿ unit ≃ X.\r\n```\r\nand thus into\r\n```\r\nDefinition weqdnicoprod n (j : stn(S n)) : stn n ⨿ unit ≃ stn (S n).\r\n```\r\nThis is unfortunate, because any `stn m` has an axiom-free proposition\r\nequivalent to `x≠y`, given by the evident recursive algorithm on nat, which\r\ncould have been used instead to define the complement of a set!  Yesterday I\r\nstarted rewriting `weqdnicoprod`, but this morning I realized there is a better\r\nway, which preserves all the theorems already proved.\r\n\r\nI would like to fix this by postponing the decision to appeal to `funextempty`:\r\n\r\nWe redefine\r\n```\r\nDefinition isisolated (X:UU) (x:X):= ∀ x':X, x=x' ⨿ x≠x'.\r\n```\r\nas\r\n```\r\nDefinition isisolated (X:UU) (x:X):=\r\n   Σ (P:X->hProp), ∀ (x':X), iscontr( x=x' ⨿ P x' ).\r\n```\r\nUsing `funextempty`, one can show that `P x'` and `x=x'` are equivalent.\r\nA suitable name for `P` would be \"apartness from x\".  Similarly, we would redefine\r\n```\r\nDefinition isdecprop ( X : UU ) := iscontr ( X ⨿ ¬ X ).\r\n```\r\n, any of whose applications would involve `funextempty`, as\r\n```\r\nDefinition isdecprop (Q:UU) := Σ P:hProp, iscontr ( Q ⨿ P ).\r\n```\r\nor as\r\n```\r\nDefinition isdecprop (Q:hProp) := Σ P:hProp, iscontr ( Q ⨿ P ).\r\n```\r\n, and redefine\r\n```\r\nDefinition isdeceq (X:UU) : UU := ∀ (x x':X), (x=x') ⨿ (x!=x').\r\n```\r\nas\r\n```\r\nDefinition isdeceq (X:UU) : UU :=\r\n   Σ P:X->X->hProp, ∀ (x x':X), iscontr ( x=x' ⨿ P x x' ).\r\n```\r\nA suitable name for such a `P` would be \"apartness on X\".  We could even make\r\nthe following definition:\r\n```\r\nDefinition isApartness (X:UU) (P:X->X->hProp) :=\r\n   ∀ (x x':X), iscontr ( x=x' ⨿ P x x' ).\r\n```\r\nSimilarly, the `P` in `isdecprop` above could be called \"a complement of X\",\r\nand we could adopt this definition:\r\n```\r\nDefinition areComplementary Q P := iscontr ( Q ⨿ P ).\r\n```\r\n\r\nWe could then also, more simply, define `isisolated` and `isdeceq` in terms of\r\n`isdecprop`.\r\n\r\nNotice that under this proposal, even though theorems are seemingly weakened,\r\nwe lose nothing, because a user of the new definitions is always free to appeal\r\nto `funextempty` if necessary.  In that way, it's just like postponing the use\r\nof LEM until it's needed, by refraining from adopting it as axiom, and\r\ninsisting it be used as a hypothesis.\r\n\r\nLet me know what you think.  I'd like to start working on it immediately, since\r\nit seems necessary.\r\n"},"comment":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/comments/153019019","html_url":"https://github.com/UniMath/UniMath/issues/227#issuecomment-153019019","issue_url":"https://api.github.com/repos/UniMath/UniMath/issues/227","id":153019019,"user":{"login":"DanGrayson","id":700228,"avatar_url":"https://avatars.githubusercontent.com/u/700228?v=3","gravatar_id":"","url":"https://api.github.com/users/DanGrayson","html_url":"https://github.com/DanGrayson","followers_url":"https://api.github.com/users/DanGrayson/followers","following_url":"https://api.github.com/users/DanGrayson/following{/other_user}","gists_url":"https://api.github.com/users/DanGrayson/gists{/gist_id}","starred_url":"https://api.github.com/users/DanGrayson/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/DanGrayson/subscriptions","organizations_url":"https://api.github.com/users/DanGrayson/orgs","repos_url":"https://api.github.com/users/DanGrayson/repos","events_url":"https://api.github.com/users/DanGrayson/events{/privacy}","received_events_url":"https://api.github.com/users/DanGrayson/received_events","type":"User","site_admin":false},"created_at":"2015-11-02T13:39:42Z","updated_at":"2015-11-02T13:39:42Z","body":"PPS: Another proposition defined as a negation and in use by us is the relation\r\n`m≤n` on `nat`, defined by\r\n```\r\nDefinition natleh ( n m : nat ) := hProppair ( neg ( natgth n m ) ) ( isapropneg _ )  .\r\nDefinition natgeh ( n m : nat ) : hProp := hProppair ( neg ( natgth m n ) ) ( isapropneg _ ) .\r\n```\r\nWe'll have to change that, too.  It's easy, beucase `m ≤ n` is equivalent to `m\r\n< S n`, which is not a negation.\r\n"}}