nat : type. z : nat. s : nat -> nat.
sum : nat -> nat -> nat -> type.
prod : nat -> nat -> nat -> type.
comp : type.
comp_rule : {x : nat} {a / nat} {b / nat}
{p / prod (s(s a)) (s(s b)) x} comp.
is no good because in the context where a and b are -irrelevant- nats, prod (s(s a)) (s(s b)) x isn't really a type! This manifests itself as the fact that although we would want
comp_rule 12 3 4 (proof that 3 x 4 = 12) comp_rule 12 2 6 (proof that 2 x 6 = 12)
to be equal, the respective third arguments cannot even be equal in the irrelevant equality judgment because they don't have the same type. But there is a fix, thankfully. I just need to encapsulate "x is composite" as a predicate:
is_comp : nat -> type.
is_comp_rule : {x : nat} {a : nat} {b : nat}
{p : prod (s(s a)) (s(s b))}
is_comp x.
and say
comp_rule : {x : nat} {p / is_comp x} comp.
