T:Type, E:(T
TProp). (EquivRel x,y:T. E(x,y)) 
(a:T. [a]{x,y:T//E(x,y)} 
x,y:T//E(x,y))| No other cites to report in MarkB_generic | |
| type_inj | Def [x]{T} == x |
| Thm* T:Type, E:(TTProp). (EquivRel x,y:T. E(x,y)) (a:T. [a]{x,y:T//E(x,y)} x,y:T//E(x,y)) |
| Syntax: | [x]{T} | has structure: | type_inj(x; T) |
About:
 |  |  |  |  |  |  |  |