Skip to Content.
Sympa Menu

ssreflect - [ssreflect] eqType for records ?

Subject: Ssreflect Users Discussion List

List archive

[ssreflect] eqType for records ?


Chronological Thread 
  • From: Bas Spitters <>
  • To: Ssreflect-mailinglist <>
  • Subject: [ssreflect] eqType for records ?
  • Date: Mon, 18 Jun 2018 17:37:45 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=None
  • Ironport-phdr: 9a23:FKgChh9+Fhyrgf9uRHKM819IXTAuvvDOBiVQ1KB30eMcTK2v8tzYMVDF4r011RmVBdids6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+553ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiCgZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsaS2RPXchfSjJPDZ+nYosTE+YMJ/pUo5Xhq1YMqxa1GAmiBPnoyj9NnnL7wLc10/88Gg/bxAwgHs4OsGjKo9XvL6cZTOe4w7LSwTrZdf9X1y3x6JPQchAgvfGMQax/cdDKyUQ0GAPFi0+fqY3hPz+PyusNtG2b4vNmWOmyhWAnrARxrSKuxscqkoTJiYMVykzE9SVk24k5P8G3SEl+YdOiDZBetDmaOpNoTs8+R2xkoiU3x70ctZKmfSUG1Y4rywPdZvGGdYWD/wjtW/yLIThigXJoYLK/iAi28Uin0uD8U9O70FdOriZcktjNuGwB2wXd6sSaSPZw/12t2TmI1wDU5eFEJV47mbDHJJ4mx748jpsTsULdES/qgEj6krOae0E+9uWr6+nreKjqq56BO4Nulw3zMKUjltS6AesiMwgOW2ab+f671L3m5UD2W69GgecsnqjXqpzaPtwbpq+lAw9JzIkj8Q2/Aiyp0NQdh3YHLVZFdAibgIjuPlHCOOr4Auung1SwjDdrwOjLPqb6ApXXMHfDnrPhcqhh5E5A0wcz1tBe55dMCr4bOv7zW0nxtMbZDhAjKQC0zfznW51B0dYlQniCDKuUO7+XtFaJ4uMpLO2Nf5Nd7C3mMfUr4/PlkVc8gkVYfK+z3JJRaXaiH/0gLV/PMlT2hdJUO24R9jEmTfD2hUeZGWpZIX/0QOQn/jAnFI+8Fq/MQ4mshPqK2yLtTc4eXXxPFl3ZSSSgTI6DQfpZLXvKepYwwAxBbqCoTsoa7T/rsQb7z7R9Ke+No38XsJvi0J5+4OiBzEhupwwxNNyU1iS2d08xhnkBHmZk06V2oEg7wVCGg/Ah3q5oUOdL7vYMaT8UcJ7Ry+sgVYL3UwPFO8aWEBOoG4r4Rz42Sd01zpkFZEMvQ9g=

Is there an established way to obtain an eqType on a Record?

I'd imagine first proving that eqTypes are closed under Sigma-types
and then converting records to Sigma-types, as e.g. is done in the
HoTT library:

https://github.com/HoTT/HoTT/blob/master/theories/Types/Record.v

Thanks,

Bas



Archive powered by MHonArc 2.6.18.

Top of Page