2. A: Type
3. R: A
AProp4.
n ~ A5. EquivRel x,y:A. x R y
6.
x,y:A. Dec(x R y)
m:(n+1). m ~ (x,y:A//(x R y)) n:{1...}, A:Type, R:(AAProp).
(n ~ A) 
(EquivRel x,y:A. x R y) (x,y:A. Dec(x R y)) (m:(n+1). m ~ (x,y:A//(x R y)))| 1 | 1. n: {1...} 2. A: Type 3. R: A AProp4. n ~ A5. EquivRel x,y:A. x R y 6. x,y:A. Dec(x R y) m:(n+1). m ~ (x,y:A//(x R y)) |
About:
 |  |  |  |  |
 |  |  |  |