diff options
| author | krasimir <krasimir@chalmers.se> | 2010-06-01 06:12:30 +0000 |
|---|---|---|
| committer | krasimir <krasimir@chalmers.se> | 2010-06-01 06:12:30 +0000 |
| commit | 5e0d04d0f59e4ace8df23befcbe8263447611e63 (patch) | |
| tree | 74bc30a8392f81fd587932f4ba54c14b4d0f7888 /examples/category-theory/Equalizer.gf | |
| parent | 19851031e69d05e802eeabfe5db55e58583e1ba0 (diff) | |
El -> Obj in category theory
Diffstat (limited to 'examples/category-theory/Equalizer.gf')
| -rw-r--r-- | examples/category-theory/Equalizer.gf | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/examples/category-theory/Equalizer.gf b/examples/category-theory/Equalizer.gf index 051a19200..4e12bd199 100644 --- a/examples/category-theory/Equalizer.gf +++ b/examples/category-theory/Equalizer.gf @@ -1,49 +1,49 @@ abstract Equalizer = Morphisms ** { -cat Equalizer ({c} : Category) ({x,y,z} : El c) (f,g : Arrow x y) (e : Arrow z x) ; +cat Equalizer ({c} : Category) ({x,y,z} : Obj c) (f,g : Arrow x y) (e : Arrow z x) ; data equalizer : ({c} : Category) - -> ({x,y,z} : El c) + -> ({x,y,z} : Obj c) -> (f,g : Arrow x y) -> (e : Arrow z x) -> EqAr (comp f e) (comp g e) -> Equalizer f g e ; fun idEqualizer : ({c} : Category) - -> ({x,y} : El c) + -> ({x,y} : Obj c) -> (f : Arrow x y) -> Equalizer f f (id x) ; def idEqualizer {c} {x} {y} f = equalizer f f (id x) (eqCompL f (eqRefl (id x))) ; fun equalizer2mono : ({c} : Category) - -> ({x,y,z} : El c) + -> ({x,y,z} : Obj c) -> (f,g : Arrow x y) -> (e : Arrow z x) -> Equalizer f g e -> Mono e ; -- def equalizer2mono = ... -cat CoEqualizer ({c} : Category) ({x,y,z} : El c) (e : Arrow y z) (f,g : Arrow x y) ; +cat CoEqualizer ({c} : Category) ({x,y,z} : Obj c) (e : Arrow y z) (f,g : Arrow x y) ; data coequalizer : ({c} : Category) - -> ({x,y,z} : El c) + -> ({x,y,z} : Obj c) -> (e : Arrow y z) -> (f,g : Arrow x y) -> EqAr (comp e f) (comp e g) -> CoEqualizer e f g ; fun idCoEqualizer : ({c} : Category) - -> ({x,y} : El c) + -> ({x,y} : Obj c) -> (f : Arrow x y) -> CoEqualizer (id y) f f ; def idCoEqualizer {c} {x} {y} f = coequalizer (id y) f f (eqCompR (eqRefl (id y)) f) ; fun coequalizer2epi : ({c} : Category) - -> ({x,y,z} : El c) + -> ({x,y,z} : Obj c) -> ({e} : Arrow y z) -> ({f,g} : Arrow x y) -> CoEqualizer e f g -> Epi e ; -- def coequalizer2epi = ... -}
\ No newline at end of file +} |