q*
6. g:
q*7. g o f = Id
8. f o g = Id
h:(q*q*). (
x,y:q*. (x E y) 
h(x) = h(y)) & (x:q*. x E (h(x)))
q*q*Propq*. x E yx,y:q*. Dec(x E y)q*) ~ h:(q*q*). (x,y:q*. (x E y) h(x) = h(y)) & (x:q*. x E (h(x)))| 1 | 5. f: q* 6. g: q*7. g o f = Id 8. f o g = Id h:(q*q*). (x,y:q*. (x E y) h(x) = h(y)) & (x:q*. x E (h(x))) |
About:
 |  |  |  |  |
 |  |  |  |