examples/category-theory/InitialAndTerminal.gf


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

abstract InitialAndTerminal = Morphisms ** {

cat  Initial  (c : Category) ;
data initial  : ({c} : Category)
              -> (x : El c)
              -> ((y : El c) -> Arrow x y)
              -> Initial c ;

fun initEl : ({c} : Category)
              -> Initial c
              -> El c ;
def initEl (initial x f) = x ;

fun initials2iso :  ({c} : Category)
                 -> ({x,y} : Initial c)
                 -> Iso (initEl x) (initEl y) ;
-- def initials2iso = .. ;

cat  Terminal (c : Category) ;
data terminal : ({c} : Category)
              -> (y : El c)
              -> ((x : El c) -> Arrow x y)
              -> Terminal c ;

fun termEl : ({c} : Category)
             -> Terminal c
             -> El c ;
def termEl (terminal x f) = x ;

fun terminals2iso :  ({c} : Category)
                  -> ({x,y} : Terminal c)
                  -> Iso (termEl x) (termEl y) ;
-- def terminals2iso = .. ;

}