The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Vladimir Voevodsky wrote:
> Suppose for example that T= Prop. Then, a function from I1 to T should 
> be a triple (P_1, P_2, prf) where P_1, P_2: Prop and prf: P_1 <-> P_2 
> is a proof of their equivalence.

If what you care about is "functions over T," then why not go directly 
to defining a type of "functions over T"?  It's easy to define a record 
type whose values are exactly the triples of the form you describe.

I'm still pretty confused as to what you're trying to do, and I expect 
I'm not alone, so context that is about applications, not just 
"algebraic structures," would be a good thing to provide if you want 
further help.