> | However this would not be compatible with existing PropositionalFormula
> | and it would not be closed. That is I would like:
> | PropositionalFormula Product(A,B)
> | PropositionalFormula Sum(A,B)
> | PropositionalFormula Exponent(A,B)
> | all to be treated as: PropositionalFormula SetCategory
Martin Baker writes:
| Since Waldek is reviewing Product domain I thought this might be the time to
| raise another question.
|
| I would like to model the equivalence between logic and Cartesian closed
| categories.
OK. One thing to realize is that the equivalence is through an
*interpretat
Since Waldek is reviewing Product domain I thought this might be the time to
raise another question.
I would like to model the equivalence between logic and Cartesian closed
categories.
What I would like to do is something like this (where A,B are different
types):
(1) -> conjunction(a:A,b:B)
