From 90e451893671ceebaa37fcb634b5d7a3f153ba70 Mon Sep 17 00:00:00 2001 From: tslil Date: Mon, 4 May 2026 17:52:04 +0100 Subject: almost done --- examples/one_simplex.makkai | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 examples/one_simplex.makkai (limited to 'examples/one_simplex.makkai') diff --git a/examples/one_simplex.makkai b/examples/one_simplex.makkai new file mode 100644 index 0000000..590cf04 --- /dev/null +++ b/examples/one_simplex.makkai @@ -0,0 +1,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 -- cgit v1.3.1