<div dir="ltr"><div>Sorry, I've been a bit sloppy with what I'm saying.<br></div><br><div class="gmail_quote"><div class="gmail-m_8017141348248689813WordSection1"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><p class="MsoNormal"><span>Btw, I don’t know what “(Foo , Foo)” is supposed to mean. We are not doing Haskell here. I guess you mean Foo x Foo?</span></p></blockquote>
<p class="MsoNormal"><span><br></span></p><p class="MsoNormal"><span>Yes, that's exactly what I mean. <br></span></p><p class="MsoNormal"><span><br></span></p>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><p class="MsoNormal"><span>You say that you want to show that “P holds for Foo”? What is P? It seems that you are thinking of a property of types. <br></span></p></blockquote>
<p class="MsoNormal"><span><br></span></p><p class="MsoNormal"><span>What I mean is that "P Foo" is inhabited. The specific P I'm using is a record type that's basically describing operations over P, so it's less of a property and more of an interface.  I'm just being sloppy with what I mean under Curry-Howard.<br></span></p><p class="MsoNormal"><span><br></span></p>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><p class="MsoNormal"><span>What does it mean that “P holds under isomorphism”?
</span></p></blockquote>
<p class="MsoNormal"><span> </span></p><p class="MsoNormal"><span>What I mean is find a function "(A B : Set) -> (A <-> B) -> P A -> P B", where <-> is isomorphism<br></span></p><p class="MsoNormal"><span><br></span></p>Thanks!</div><div class="gmail-m_8017141348248689813WordSection1">Joey<pre></pre></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">

</blockquote></div></div>