2. R: A*
A*Prop3. EquivRel x,y:A*. x R y
4.
x,y,z:A*. (x R y) 
((z @ x) R (z @ y))5. g: (x,y:A*//(x R y))
Refl(x,y:A*//(x R y);u,v.u Rg v)
& Sym u,v:x,y:A*//(x R y). u Rg v
& Trans u,v:x,y:A*//(x R y). u Rg v A:Type, R:(A*A*Prop).
(EquivRel x,y:A*. x R y)
(x,y,z:A*. (x R y) ((z @ x) R (z @ y)))
(g:((x,y:A*//(x R y))). EquivRel u,v:x,y:A*//(x R y). u Rg v)| 1 | 1. A: Type 2. R: A* A*Prop3. EquivRel x,y:A*. x R y 4. x,y,z:A*. (x R y) ((z @ x) R (z @ y))5. g: (x,y:A*//(x R y)) Refl(x,y:A*//(x R y);u,v.u Rg v)
& Sym u,v:x,y:A*//(x R y). u Rg v
& Trans u,v:x,y:A*//(x R y). u Rg v |
About:
 |  |  |  |  |
 |  |  |  |