Irrelevant!
More outline progress. Avi Silterra gave me a good example to work with - the subset type of composite naturals. A very natural instance of there being more than one proof of the relevant property. Every factorization is a different proof. Moreover, the naive way of coding it up fails the valid-type-in-unpromoted-gamma check! Namely:
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
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:
and say
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.