<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">I was at the meeting in Logroño and my impression was that we had to live with these different formalisations. There was no way to unify them and the best one could hope to transfer certain results from one formalisation to another using local types in some incredibly complicated way.<br class=""><br class="">If there really is a common basis for formalising linear algebra than I would be thrilled to see it, and I'm sure we could figure out a way to implement this.<div class=""><br class=""><div class="">
Larry
</div>
<div><br class=""><blockquote type="cite" class=""><div class="">On 26 Feb 2018, at 14:57, Fabian Immler <<a href="mailto:immler@in.tum.de" class="">immler@in.tum.de</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><span style="font-family: Consolas; font-size: 13px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">We do have the problem that AFP/Jordan_Normal_Form/Matrix and Analysis/Finite_Cartesian_Product both formalize vectors and matrices and that there are formalizations of (aspects of) linear algebra for both of them. Last year in Logrono, there was the proposal to put all linear algebra on the common foundation of a locale for modules, but apparently nobody has found the time and motivation to push this much further.</span><br style="font-family: Consolas; font-size: 13px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br style="font-family: Consolas; font-size: 13px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><span style="font-family: Consolas; font-size: 13px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">Perhaps a more humble first step towards unifying the existing theories would be to move AFP/Jordan_Normal_Form/Matrix to the distribution and do the construction of Finite_Cartesian_Product.vec as a subtype of Matrix.vec.</span><br style="font-family: Consolas; font-size: 13px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br style="font-family: Consolas; font-size: 13px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><span style="font-family: Consolas; font-size: 13px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">Any opinions on that?</span><br style="font-family: Consolas; font-size: 13px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""></div></blockquote></div><br class=""></div></body></html>