graph:type
Graphr:typeGraphObject(graph(r))
Type{i'}e:Type(evv)Top Type{i'}
t:Graph Representation. t.graph t.typeGrapht:Graph Representation. t.obj r:t.typeGraphObject(t.graph(r))t:Graph Representation. t.type Type| Some definitions of interest. | |
| graphrep | Def Graph Representation == type:Typegraph:typeGraphr:typeGraphObject(graph(r)) |
| Thm* Graph Representation Type{i'} | |
| graph | Def Graph == v:Typee:Type(evv)Top |
| Thm* Graph Type{i'} | |
| grr_graph | Def t.graph == 1of(2of(t)) |
| Thm* t:Graph Representation. t.graph t.typeGraph | |
| grr_obj | Def t.obj == 2of(2of(t)) |
| Thm* t:Graph Representation. t.obj r:t.typeGraphObject(t.graph(r)) | |
| grr_type | Def t.type == 1of(t) |
| Thm* t:Graph Representation. t.type Type |
About:
 |  |  |  |  |  |  |  |  |