examples/one_simplex.makkai


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

let signature Graph = theory {
    Vertex :: Set,
    Edge :: (s : set-of(Vertex)) (t : set-of(Vertex)) -> Set
}

let set Empty = variant[]
let set Unit = record{}
let element pt : Unit = {}
let set F1 = variant [ one0 : Unit ]
let set F2 = variant [ two0 : Unit | two1 : Unit ]
let set F3 = variant [ three0 : Unit | three1 : Unit  | three2: Unit ]

let instance oneSimplex :: Graph = {
    .Vertex = F3 :: Set,
    .Edge = for (s : set-of(Vertex)) (t : set-of(Vertex)),
              case s of [
                three0. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Unit :: Set | three2. pt => Unit :: Set ]
                | three1. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Empty :: Set | three2. pt => Unit :: Set ]
                | three2. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Empty :: Set | three2. pt => Empty :: Set ]
              ]
}

let set OneSimplexEdges = record {
  source: set-of(oneSimplex .Vertex),
  target: set-of(oneSimplex .Vertex),
  connected: set-of(oneSimplex .Edge source target)
}

let element vertex0 : F3 = three0. {}
let element vertex1 : F3 = three1. {}
let element edge01 : set-of(oneSimplex .Edge vertex0 vertex1) = pt