Comment by deltaonenine

No he wants two things. Those 6 different things have isomorphisms and can be reduced down to two things.

Think of it like 1*2 && 2. Both expressions are isomorphic. Dependent types literally encompasses everything he wants.