q:, E:(q*q*Prop). (EquivRel x,y:q*. x E y) & (x,y:q*. Dec(x E y)) (h:(q*q*). (x,y:q*. (x E y) h(x) = h(y)) & (x:q*. x E (h(x))))

1	1. q: 2. E: q*q*Prop 3. EquivRel x,y:q*. x E y 4. x,y:q*. Dec(x E y) h:(q*q*). (x,y:q*. (x E y) h(x) = h(y)) & (x:q*. x E (h(x)))

About: