blob: b8a9f00c996b4510dd3cdbb71036f327091ccd98 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
abstract InitialAndTerminal = Morphisms ** {
cat Initial ({c} : Category) (Obj c) ;
data initial : ({c} : Category)
-> (x : Obj c)
-> ((y : Obj c) -> Arrow x y)
-> Initial x ;
fun initAr : ({c} : Category)
-> ({x} : Obj c)
-> Initial x
-> (y : Obj c)
-> Arrow x y ;
-- def initAr {~c} {~x} (initial {c} x f) y = f y ;
{-
fun initials2iso : ({c} : Category)
-> ({x,y} : Obj c)
-> (ix : Initial x)
-> (iy : Initial y)
-> Iso (initAr ix y) (initAr iy x) ;
-}
-- def initials2iso = .. ;
cat Terminal ({c} : Category) (Obj c) ;
data terminal : ({c} : Category)
-> (y : Obj c)
-> ((x : Obj c) -> Arrow x y)
-> Terminal y ;
fun terminalAr : ({c} : Category)
-> (x : Obj c)
-> ({y} : Obj c)
-> Terminal y
-> Arrow x y ;
-- def terminalAr {c} x {~y} (terminal {~c} y f) = f x ;
{-
fun terminals2iso : ({c} : Category)
-> ({x,y} : Obj c)
-> (tx : Terminal x)
-> (ty : Terminal y)
-> Iso (terminalAr x ty) (terminalAr y tx) ;
-}
-- def terminals2iso = .. ;
}
|
