[Agda] Induction from Sigma?

[Joey Eremondi]

Sorry, I've been a bit sloppy with what I'm saying.

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?
>

Yes, that's exactly what I mean.


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.
>

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.


What does it mean that “P holds under isomorphism”?
>


What I mean is find a function "(A B : Set) -> (A <-> B) -> P A -> P B",
where <-> is isomorphism


Thanks!
Joey
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200409/39dcc029/attachment.html>