| NOTE: | EquivRel(A)(R(_1;_2)) is | alpha-equivalent | to EquivRel x,y:A. R(x;y). |
| Who Cites equiv rel? | |
| equiv_rel | Def EquivRel x,y:T. E(x;y) == Refl(T;x,y.E(x;y)) & (Sym x,y:T. E(x;y)) & (Trans x,y:T. E(x;y)) |
Thm*  T:Type, E:(T  TProp). (EquivRel x,y:T. E(x,y))  Prop | |
| trans | Def Trans x,y:T. E(x;y) == a,b,c:T. E(a;b)   E(b;c) E(a;c) |
| Thm* T:Type, E:(TTProp). (Trans x,y:T. E(x,y)) Prop | |
| sym | Def Sym x,y:T. E(x;y) == a,b:T. E(a;b) E(b;a) |
| Thm* T:Type, E:(TTProp). (Sym x,y:T. E(x,y)) Prop | |
| refl | Def Refl(T;x,y.E(x;y)) == a:T. E(a;a) |
| Thm* T:Type, E:(TTProp). Refl(T;x,y.E(x,y)) Prop |
| Syntax: | EquivRel x,y:T. E(x;y) | has structure: | equiv_rel(T; x,y.E(x;y)) |
About:
 |  |  |  |  |  |  |  |