Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Silly question about decidable equality and inequality

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Silly question about decidable equality and inequality


Chronological Thread 
    < Chronological >      < Thread >
  • From: Talia Ringer <tringer AT cs.washington.edu>
  • To: Coq-Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Silly question about decidable equality and inequality
  • Date: Tue, 23 Jun 2020 19:25:07 -0700
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=Pass smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-wr1-f53.google.com
  • Ironport-phdr: 9a23:0ZAVHhTTUjjlMYT+tQMiQdZpbtpsv+yvbD5Q0YIujvd0So/mwa6yZhGN2/xhgRfzUJnB7Loc0qyK6v2mADxeqsvf+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi2oAnLq8UbgopvJqkxxxbIv3BFZ/lYyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7ULJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5LplRRP0lCsKMSMy/WfKgcJyka1bugqsqBN/zYDaY4+bKeRwcb/GcNwAWWZMRNxcWzBdDo6+aYYEEuoPPfxfr4n4v1YAswGxBQ2tBOz11zRGmn723as10+s/CwHNwQstH84UsHTVqtX1O7kdUfquwabU1jXPdf1X1i3m6IjIcxAhp/6MXa53ccrX00UgCR7KjkiJpIHjIjia2fgDvXKB4Op8SeKglXQnqwdprzWg2sshjofEiI0bxF7K8Sh13Jg5KMCkRUB0fNKpFIZduSGHO4Z5XM4vTH1ltSg1x7AEt5O2fSsHxYk6yxPdavGKdZWD7BH7VOuJPzt0mHZodKi8ihuy60Ss1PPwWtSu3FtKoCdIlMTHuGoX2BzJ8MeHT+Nw/ke/1jaL0ADe8uRELlo1larfMpIgzKQwmocKvUTNHiL7ll/6jKCRdkUj9eio7/robq/6qZ+bMo94kgD+MqIwlcyjGek0LBQCUmyB9em/1LDv51P1TKtXgvEskqTUvojWJcEBqa64Bw9V3Jwj6xG6Dzq+zNQYh3gHLFRKeB2ZlYjkIE3BIOviAfaxmVusizdrx/HAPr3uHpXNKX7DnK3/crlg9k5Q0BAzwsxH55JIFrEBJ+r+VVP2tNzBFxM2Lwi0w/v8B9hmzYMfWWePAreDP6/IsF+I4PgvI+iWa4MPtjb9Matt2/m7pngg3HQZYKPhiZAQcTWzGulsC0Sfe3vlxNkbRzQkpA07GdDjjFyLGQRSYXm/Repo+is6Do2rF6/IXcayiaeB3SG0AppQIG1KFwbfQj/Ta4yYVqJUO2qpKch7n2lcDOXze8oazRir8TTC5f9nI+7ToHBKsJvi0J1q/bSWm0xpszNzCMuZ3ieGSGQmxjpUFQ9z57h2pAlG8nnGybJx2q0KHscV+PpSUgY8OoLbyap3B82gAluQLOfMc06vR5CdOR90S9swx9EUZEMkSoeplVbc1jGqArkai7uNQpE47/CF0g==
Hi all,

I think this should be obvious, but I'm having trouble thinking right now. I figure I'll ask in case somebody knows the answer.

Suppose I have a type with decidable equality, like nat. Then provably I have that all proofs of n = m for n m : nat are equal to each other, without assuming UIP as an axiom. That much I know.

From this, can I say anything about proofs of n <> m for n m : nat without assuming functional extensionality? For example, are all proofs of 0 <> 1 equal to each other? If not, are they provably related in any interesting way?

Talia

Archive powered by MHonArc 2.6.19+.

Top of Page