[Agda] chatgpt and agda

[warrick scott]

Below is me playing around with chatgpt. Dunno if anyone else has had 
the chance to try this? It says an error occurs after my last question.

  attached is a .txt of the convo.

  curious to see what y'all come up with.


define a simplicial complex in agda

In the context of homotopy theory and algebraic topology, a simplicial 
complex is a combinatorial structure that is used to represent a 
topological space. It consists of a set of vertices, a set of edges, and 
a set of higher-dimensional simplices (triangles, tetrahedra, etc.), 
with the property that the vertices of any simplex are also vertices of 
the complex, and the edges of any simplex are also edges of the complex.

In Agda, a simplicial complex can be defined as a data type with three 
indices: one for the vertices, one for the edges, and one for the 
higher-dimensional simplices. The vertices and edges are represented as 
lists of integers, while the higher-dimensional simplices are 
represented as lists of lists of integers.

Here is an example of how a simplicial complex could be defined in Agda:

Copy code
|data SimplicialComplex (V : ℕ) (E : ℕ) (S : ℕ) : Set where 
mkSimplicialComplex : (vertices : List V) (edges : List (List 2)) 
(simplices : List (List (S + 1))) → SimplicialComplex V E S |

This definition specifies that a |SimplicialComplex| consists of a list 
of vertices (represented by |V|), a list of edges (represented by |E|), 
and a list of simplices (represented by |S|). The vertices and edges are 
represented as lists of integers, while the simplices are represented as 
lists of lists of integers.

To use this data type, you would need to provide concrete values for the 
indices |V|, |E|, and |S|. For example, you could define a simplicial 
complex with 3 vertices, 3 edges, and 2 triangles as follows:

Copy code
|exampleComplex : SimplicialComplex 3 3 2 exampleComplex = 
mkSimplicialComplex [0, 1, 2] [[0, 1], [1, 2], [2, 0]] [[0, 1, 2], [0, 
2, 1]] |

This simplicial complex consists of 3 vertices (numbered 0, 1, and 2), 3 
edges (connecting the vertices 0 and 1, 1 and 2, and 2 and 0), and 2 
triangles (formed by the vertices 0, 1, and 2, and 0, 2, and 1).

wmacmil at gmail.com
i just tried this and it didnt type check. it says List V is wrong 
because the numbers aren't of type set. can you help me correct the program?

In the definition of |SimplicialComplex|, |V| is defined as a type-level 
natural number (using the |ℕ| type), but |vertices| is defined as a list 
of elements of type |V|. However, in Agda, elements of a list must be of 
type |Set|, not |ℕ|. Therefore, you need to change the type of |V| from 
|ℕ| to |Set|.

Here is how you can modify the definition of |SimplicialComplex| to fix 
this error:

Copy code
|data SimplicialComplex (V : Set) (E : ℕ) (S : ℕ) : Set where 
mkSimplicialComplex : (vertices : List V) (edges : List (List 2)) 
(simplices : List (List (S + 1))) → SimplicialComplex V E S |

With this change, the type of |vertices| will be |List V|, where |V| is 
a type of type |Set|. This means that you can use any type as the vertex 
type, as long as it is of type |Set|.

For example, you could define a simplicial complex with vertices of type 
|String| as follows:

Copy code
|exampleComplex : SimplicialComplex String 3 2 exampleComplex = 
mkSimplicialComplex ["A", "B", "C"] [[0, 1], [1, 2], [2, 0]] [[0, 1, 2], 
[0, 2, 1]] |

This simplicial complex consists of 3 vertices (labeled "A", "B", and 
"C"), 3 edges (connecting the vertices "A" and "B", "B" and "C", and "C" 
and "A"), and 2 triangles (formed by the vertices "A", "B", and "C", and 
"A", "C", and "B").

wmacmil at gmail.com
but now List 2 doesn't typecheck for the same reason. and the edges in 
your example don't necessarily refer to the vertices. how can we fix this?

You are correct that the definition of |SimplicialComplex| still has an 
error in the type of |edges|. In the current definition, |edges| is 
defined as a list of lists of size 2, but the elements of this list 
should actually be pairs of vertices.

To fix this error, you can define the type of |edges| as a list of pairs 
of vertices. Here is how you can modify the definition of 
|SimplicialComplex| to do this:

Copy code
|data SimplicialComplex (V : Set) (E : ℕ) (S : ℕ) : Set where 
mkSimplicialComplex : (vertices : List V) (edges : List (V × V)) 
(simplices : List (List (S + 1))) → SimplicialComplex V E S |

With this change, the type of |edges| will be |List (V × V)|, which is a 
list of pairs of vertices. This means that each element of the list 
|edges| will be a pair of vertices, rather than a list of size 2.

For example, you could define a simplicial complex with 3 vertices and 3 
edges as follows:

Copy code
|exampleComplex : SimplicialComplex String 3 0 exampleComplex = 
mkSimplicialComplex ["A", "B", "C"] [("A", "B"), ("B", "C"), ("C", "A")] 
[] |

This simplicial complex consists of 3 vertices (labeled "A", "B", and 
"C") and 3 edges (connecting the vertices "A" and "B", "B" and "C", and 
"C" and "A"). It does not have any higher-dimensional simplices.

I hope this helps! Let me know if you have any further questions.

wmacmil at gmail.com
ok, now List (S + 1) is failing to typecheck, again for the same reason.

You are correct that the definition of |SimplicialComplex| still has an 
error in the type of |simplices|. In the current definition, |simplices| 
is defined as a list of lists of size |S + 1|, but the elements of this 
list should actually be lists of vertices.

To fix this error, you can define the type of |simplices| as a list of 
lists of vertices. Here is how you can modify the definition of 
|SimplicialComplex| to do this:

Copy code
|data SimplicialComplex (V : Set) (E : ℕ) (S : ℕ) : Set where 
mkSimplicialComplex : (vertices : List V) (edges : List (V × V)) 
(simplices : List (List V)) → SimplicialComplex V E S |

With this change, the type of |simplices| will be |List (List V)|, which 
is a list of lists of vertices. This means that each element of the list 
|simplices| will be a list of vertices, rather than a list of size |S + 1|.

For example, you could define a simplicial complex with 3 vertices, 3 
edges, and 2 triangles as follows:

Copy code
|exampleComplex : SimplicialComplex String 3 2 exampleComplex = 
mkSimplicialComplex ["A", "B", "C"] [("A", "B"), ("B", "C"), ("C", "A")] 
[["A", "B", "C"], ["A", "C", "B"]] |

This simplicial complex consists of 3 vertices (labeled "A", "B", and 
"C"), 3 edges (connecting the vertices "A" and "B", "B" and "C", and "C" 
and "A"), and 2 triangles (formed by the vertices "A", "B", and "C", and 
"A", "C", and "B").

I hope this helps! Let me know if you have any further questions.

wmacmil at gmail.com
now you SimplicialComplex definition typechecks! although, the 
parameters E and S no longer seem relevant - we can substitute any 
numbers for them in exampleComplex. how can we improve the definition so 
that the parameters more accurately indicate the shape of the complex?

You are correct that the current definition of |SimplicialComplex| does 
not use the indices |E| and |S| in a meaningful way. In particular, the 
indices |E| and |S| do not necessarily reflect the number of edges and 
higher-dimensional simplices in the simplicial complex.

To make the definition of |SimplicialComplex| more accurate, you could 
remove the indices |E| and |S| entirely, and simply specify the number 
of edges and higher-dimensional simplices directly in the definition. 
Here is how you could modify the definition of |SimplicialComplex| to do 
this:

Copy code
|data SimplicialComplex (V : Set) : Set where mkSimplicialComplex : 
(vertices : List V) (edges : List (V × V)) (simplices : List (List V)) → 
SimplicialComplex V |

With this change, the type of |SimplicialComplex V| will represent a 
simplicial complex with vertices of type |V|, and the number of edges 
and higher-dimensional simplices will be determined by the lengths of 
the lists |edges| and |simplices|.

For example, you could define a simplicial complex with 3 vertices, 3 
edges, and 2 triangles as follows:

Copy code
|exampleComplex : SimplicialComplex String exampleComplex = 
mkSimplicialComplex ["A", "B", "C"] [("A", "B"), ("B", "C"), ("C", "A")] 
[["A", "B", "C"], ["A", "C", "B"]] |

This simplicial complex consists of 3 vertices (labeled "A", "B", and 
"C"), 3 edges (connecting the vertices "A" and "B", "B" and "C", and "C" 
and "A"), and 2 triangles (formed by the vertices "A", "B", and "C", and 
"A", "C", and "B").

I hope this helps! Let me know if you have any further questions.

wmacmil at gmail.com
great. but what if we still want to keep E and S as indices to indicate 
the size of the lists, whereby the sized lists are actually vectors of 
fixed length? can you keep these indexes to get a more informative 
simplicial complex? and, couldn't you just port your current version to 
haskell?

If you still want to keep the indices |E| and |S| as a way to indicate 
the size of the lists |edges| and |simplices|, you can define 
|SimplicialComplex| as a dependent data type, where the indices |E| and 
|S| are used to specify the lengths of the lists |edges| and |simplices|.

Here is how you can define |SimplicialComplex| as a dependent data type:

Copy code
|data SimplicialComplex (V : Set) (E : ℕ) (S : ℕ) : Set where 
mkSimplicialComplex : (vertices : List V) (edges : Vector E (V × V)) 
(simplices : Vector S (List V)) → SimplicialComplex V E S |

With this definition, the type of |SimplicialComplex V E S| represents a 
simplicial complex with vertices of type |V|, and |E| edges and |S| 
higher-dimensional simplices. The lists |edges| and |simplices| are 
replaced with vectors of fixed length |E| and |S|, respectively, which 
means that each |SimplicialComplex| will have exactly |E| edges and |S| 
higher-dimensional simplices.

For example, you could define a simplicial complex with 3 vertices, 3 
edges, and 2 triangles as follows:

Copy code
|exampleComplex : SimplicialComplex String 3 2 exampleComplex = 
mkSimplicialComplex ["A", "B", "C"] (vector [("A", "B"), ("B", "C"), 
("C", "A")]) (vector [["A", "B", "C"], ["A", "C", "B"]]) |

This simplicial complex consists of 3 vertices (labeled "A", "B", and 
"C"), 3 edges (connecting the vertices "A" and "B", "B" and "C", and "C" 
and "A"), and 2 triangles (formed by the vertices "A", "B", and "C", and 
"A", "C", and "B").

As for your second question, it is possible to port the definition of 
|SimplicialComplex| from Agda to Haskell. Here is how the definition 
would look in Haskell:

Copy code
|data SimplicialComplex v e s = SimplicialComplex { vertices :: [v] , 
edges :: Vector e (v, v) , simplices :: Vector s [v] } |

This definition of |SimplicialComplex| in Haskell is similar to the 
definition in Agda, with the exception that the indices |e| and |s| are 
replaced with type variables |e| and |s|, and the lists |edges| and 
|simplices| are replaced with vectors of type |Vector e (v, v)| and 
|Vector s [v]|, respectively.

I hope this helps! Let me know if you have any further questions.

wmacmil at gmail.com
regarding our simplicial complex in agda, how can one distinguish 
between triangular and tetrahedral simplices? our definition kind of 
squashes them together, right?

In the current definition of |SimplicialComplex|, all higher-dimensional 
simplices are represented as lists of vertices, regardless of their 
dimension. This means that it is not possible to distinguish between 
triangular and tetrahedral simplices (or simplices of any other 
dimension) based on the type alone.

To distinguish between simplices of different dimensions, you could add 
an extra parameter to the definition of |SimplicialComplex| that 
specifies the dimension of each simplex. Here is how you could modify 
the definition of |SimplicialComplex| to do this:

Copy code
|data SimplicialComplex (V : Set) : Set where mkSimplicialComplex : 
(vertices : List V) (edges : List (V × V)) (simplices : List (ℕ × List 
V)) → SimplicialComplex V |

With this change, the type of |simplices| will be |List (ℕ × List V)|, 
which is a list of pairs where the first element is an integer 
representing the dimension of the simplex, and the second element is a 
list of vertices.

For example, you could define a simplicial complex with 3 vertices, 3 
edges, and 2 triangles as follows:

Copy code
|exampleComplex : SimplicialComplex String exampleComplex = 
mkSimplicialComplex ["A", "B", "C"] [("A", "B"), ("B", "C"), ("C", "A")] 
[(2, ["A", "B", "C"]), (2, ["A", "C", "B"])] |

This simplicial complex consists of 3 vertices (labeled "A", "B", and 
"C"), 3 edges (connecting the vertices "A" and "B", "B" and "C", and "C" 
and "A"), and 2 triangles (formed by the vertices "A", "B", and "C", and 
"A", "C", and "B").

With this definition of |SimplicialComplex|, it is possible to 
distinguish between simplices of different dimensions based on the value 
of the first element in each pair. For example, you could define a 
tetrahedron as follows:

Copy code
|tetrahedron : SimplicialComplex String tetrahedron = 
mkSimplicialComplex ["A", "B", "C", "D"] [("A", "B"), ("A", "C"), ("A", 
"D"), ("B", "C"), ("B", "D"), ("C", "D")] [(3, ["A", "B", "C", "D"])] |

This simplicial complex consists of 4 vertices (labeled "A", "B", "C", 
and "D"), 6 edges (connecting the vertices "A" and "B", "A

wmacmil at gmail.com
but can't we do better by restricting the triangular simplices to take 
vectors of length 3, and the tetrahedral simplices to have 4 elements?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20221219/1d959dcd/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: image/svg+xml
Size: 78 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20221219/1d959dcd/attachment-0001.svg>
-------------- next part --------------
define a simplicial complex in agda

In the context of homotopy theory and algebraic topology, a simplicial complex is a combinatorial structure that is used to represent a topological space. It consists of a set of vertices, a set of edges, and a set of higher-dimensional simplices (triangles, tetrahedra, etc.), with the property that the vertices of any simplex are also vertices of the complex, and the edges of any simplex are also edges of the complex.

In Agda, a simplicial complex can be defined as a data type with three indices: one for the vertices, one for the edges, and one for the higher-dimensional simplices. The vertices and edges are represented as lists of integers, while the higher-dimensional simplices are represented as lists of lists of integers.

Here is an example of how a simplicial complex could be defined in Agda:

Copy code
data SimplicialComplex (V : ℕ) (E : ℕ) (S : ℕ) : Set where
  mkSimplicialComplex :
    (vertices : List V)
    (edges : List (List 2))
    (simplices : List (List (S + 1)))
    → SimplicialComplex V E S
This definition specifies that a SimplicialComplex consists of a list of vertices (represented by V), a list of edges (represented by E), and a list of simplices (represented by S). The vertices and edges are represented as lists of integers, while the simplices are represented as lists of lists of integers.

To use this data type, you would need to provide concrete values for the indices V, E, and S. For example, you could define a simplicial complex with 3 vertices, 3 edges, and 2 triangles as follows:

Copy code
exampleComplex : SimplicialComplex 3 3 2
exampleComplex =
  mkSimplicialComplex
    [0, 1, 2]
    [[0, 1], [1, 2], [2, 0]]
    [[0, 1, 2], [0, 2, 1]]
This simplicial complex consists of 3 vertices (numbered 0, 1, and 2), 3 edges (connecting the vertices 0 and 1, 1 and 2, and 2 and 0), and 2 triangles (formed by the vertices 0, 1, and 2, and 0, 2, and 1).




wmacmil at gmail.com
i just tried this and it didnt type check. it says List V is wrong because the numbers aren't of type set. can you help me correct the program?
In the definition of SimplicialComplex, V is defined as a type-level natural number (using the ℕ type), but vertices is defined as a list of elements of type V. However, in Agda, elements of a list must be of type Set, not ℕ. Therefore, you need to change the type of V from ℕ to Set.

Here is how you can modify the definition of SimplicialComplex to fix this error:

Copy code
data SimplicialComplex (V : Set) (E : ℕ) (S : ℕ) : Set where
  mkSimplicialComplex :
    (vertices : List V)
    (edges : List (List 2))
    (simplices : List (List (S + 1)))
    → SimplicialComplex V E S
With this change, the type of vertices will be List V, where V is a type of type Set. This means that you can use any type as the vertex type, as long as it is of type Set.

For example, you could define a simplicial complex with vertices of type String as follows:

Copy code
exampleComplex : SimplicialComplex String 3 2
exampleComplex =
  mkSimplicialComplex
    ["A", "B", "C"]
    [[0, 1], [1, 2], [2, 0]]
    [[0, 1, 2], [0, 2, 1]]
This simplicial complex consists of 3 vertices (labeled "A", "B", and "C"), 3 edges (connecting the vertices "A" and "B", "B" and "C", and "C" and "A"), and 2 triangles (formed by the vertices "A", "B", and "C", and "A", "C", and "B").




wmacmil at gmail.com
but now List 2 doesn't typecheck for the same reason. and the edges in your example don't necessarily refer to the vertices. how can we fix this?
You are correct that the definition of SimplicialComplex still has an error in the type of edges. In the current definition, edges is defined as a list of lists of size 2, but the elements of this list should actually be pairs of vertices.

To fix this error, you can define the type of edges as a list of pairs of vertices. Here is how you can modify the definition of SimplicialComplex to do this:

Copy code
data SimplicialComplex (V : Set) (E : ℕ) (S : ℕ) : Set where
  mkSimplicialComplex :
    (vertices : List V)
    (edges : List (V × V))
    (simplices : List (List (S + 1)))
    → SimplicialComplex V E S
With this change, the type of edges will be List (V × V), which is a list of pairs of vertices. This means that each element of the list edges will be a pair of vertices, rather than a list of size 2.

For example, you could define a simplicial complex with 3 vertices and 3 edges as follows:

Copy code
exampleComplex : SimplicialComplex String 3 0
exampleComplex =
  mkSimplicialComplex
    ["A", "B", "C"]
    [("A", "B"), ("B", "C"), ("C", "A")]
    []
This simplicial complex consists of 3 vertices (labeled "A", "B", and "C") and 3 edges (connecting the vertices "A" and "B", "B" and "C", and "C" and "A"). It does not have any higher-dimensional simplices.

I hope this helps! Let me know if you have any further questions.




wmacmil at gmail.com
ok, now List (S + 1) is failing to typecheck, again for the same reason. 
You are correct that the definition of SimplicialComplex still has an error in the type of simplices. In the current definition, simplices is defined as a list of lists of size S + 1, but the elements of this list should actually be lists of vertices.

To fix this error, you can define the type of simplices as a list of lists of vertices. Here is how you can modify the definition of SimplicialComplex to do this:

Copy code
data SimplicialComplex (V : Set) (E : ℕ) (S : ℕ) : Set where
  mkSimplicialComplex :
    (vertices : List V)
    (edges : List (V × V))
    (simplices : List (List V))
    → SimplicialComplex V E S
With this change, the type of simplices will be List (List V), which is a list of lists of vertices. This means that each element of the list simplices will be a list of vertices, rather than a list of size S + 1.

For example, you could define a simplicial complex with 3 vertices, 3 edges, and 2 triangles as follows:

Copy code
exampleComplex : SimplicialComplex String 3 2
exampleComplex =
  mkSimplicialComplex
    ["A", "B", "C"]
    [("A", "B"), ("B", "C"), ("C", "A")]
    [["A", "B", "C"], ["A", "C", "B"]]
This simplicial complex consists of 3 vertices (labeled "A", "B", and "C"), 3 edges (connecting the vertices "A" and "B", "B" and "C", and "C" and "A"), and 2 triangles (formed by the vertices "A", "B", and "C", and "A", "C", and "B").

I hope this helps! Let me know if you have any further questions.




wmacmil at gmail.com
now you SimplicialComplex definition typechecks! although, the parameters E and S no longer seem relevant - we can substitute any numbers for them in exampleComplex. how can we improve the definition so that the parameters more accurately indicate the shape of the complex? 
You are correct that the current definition of SimplicialComplex does not use the indices E and S in a meaningful way. In particular, the indices E and S do not necessarily reflect the number of edges and higher-dimensional simplices in the simplicial complex.

To make the definition of SimplicialComplex more accurate, you could remove the indices E and S entirely, and simply specify the number of edges and higher-dimensional simplices directly in the definition. Here is how you could modify the definition of SimplicialComplex to do this:

Copy code
data SimplicialComplex (V : Set) : Set where
  mkSimplicialComplex :
    (vertices : List V)
    (edges : List (V × V))
    (simplices : List (List V))
    → SimplicialComplex V
With this change, the type of SimplicialComplex V will represent a simplicial complex with vertices of type V, and the number of edges and higher-dimensional simplices will be determined by the lengths of the lists edges and simplices.

For example, you could define a simplicial complex with 3 vertices, 3 edges, and 2 triangles as follows:

Copy code
exampleComplex : SimplicialComplex String
exampleComplex =
  mkSimplicialComplex
    ["A", "B", "C"]
    [("A", "B"), ("B", "C"), ("C", "A")]
    [["A", "B", "C"], ["A", "C", "B"]]
This simplicial complex consists of 3 vertices (labeled "A", "B", and "C"), 3 edges (connecting the vertices "A" and "B", "B" and "C", and "C" and "A"), and 2 triangles (formed by the vertices "A", "B", and "C", and "A", "C", and "B").

I hope this helps! Let me know if you have any further questions.




wmacmil at gmail.com
great. but what if we still want to keep  E and S as indices to indicate the size of the lists, whereby the sized lists are actually vectors of fixed length? can you keep these indexes to get a more informative simplicial complex? and, couldn't you just port your current version to haskell? 
If you still want to keep the indices E and S as a way to indicate the size of the lists edges and simplices, you can define SimplicialComplex as a dependent data type, where the indices E and S are used to specify the lengths of the lists edges and simplices.

Here is how you can define SimplicialComplex as a dependent data type:

Copy code
data SimplicialComplex (V : Set) (E : ℕ) (S : ℕ) : Set where
  mkSimplicialComplex :
    (vertices : List V)
    (edges : Vector E (V × V))
    (simplices : Vector S (List V))
    → SimplicialComplex V E S
With this definition, the type of SimplicialComplex V E S represents a simplicial complex with vertices of type V, and E edges and S higher-dimensional simplices. The lists edges and simplices are replaced with vectors of fixed length E and S, respectively, which means that each SimplicialComplex will have exactly E edges and S higher-dimensional simplices.

For example, you could define a simplicial complex with 3 vertices, 3 edges, and 2 triangles as follows:

Copy code
exampleComplex : SimplicialComplex String 3 2
exampleComplex =
  mkSimplicialComplex
    ["A", "B", "C"]
    (vector [("A", "B"), ("B", "C"), ("C", "A")])
    (vector [["A", "B", "C"], ["A", "C", "B"]])
This simplicial complex consists of 3 vertices (labeled "A", "B", and "C"), 3 edges (connecting the vertices "A" and "B", "B" and "C", and "C" and "A"), and 2 triangles (formed by the vertices "A", "B", and "C", and "A", "C", and "B").

As for your second question, it is possible to port the definition of SimplicialComplex from Agda to Haskell. Here is how the definition would look in Haskell:

Copy code
data SimplicialComplex v e s =
  SimplicialComplex
    { vertices :: [v]
    , edges :: Vector e (v, v)
    , simplices :: Vector s [v]
    }
This definition of SimplicialComplex in Haskell is similar to the definition in Agda, with the exception that the indices e and s are replaced with type variables e and s, and the lists edges and simplices are replaced with vectors of type Vector e (v, v) and Vector s [v], respectively.

I hope this helps! Let me know if you have any further questions.




wmacmil at gmail.com
regarding our simplicial complex in agda, how can one distinguish between triangular and tetrahedral simplices? our definition kind of squashes them together, right?
In the current definition of SimplicialComplex, all higher-dimensional simplices are represented as lists of vertices, regardless of their dimension. This means that it is not possible to distinguish between triangular and tetrahedral simplices (or simplices of any other dimension) based on the type alone.

To distinguish between simplices of different dimensions, you could add an extra parameter to the definition of SimplicialComplex that specifies the dimension of each simplex. Here is how you could modify the definition of SimplicialComplex to do this:

Copy code
data SimplicialComplex (V : Set) : Set where
  mkSimplicialComplex :
    (vertices : List V)
    (edges : List (V × V))
    (simplices : List (ℕ × List V))
    → SimplicialComplex V
With this change, the type of simplices will be List (ℕ × List V), which is a list of pairs where the first element is an integer representing the dimension of the simplex, and the second element is a list of vertices.

For example, you could define a simplicial complex with 3 vertices, 3 edges, and 2 triangles as follows:

Copy code
exampleComplex : SimplicialComplex String
exampleComplex =
  mkSimplicialComplex
    ["A", "B", "C"]
    [("A", "B"), ("B", "C"), ("C", "A")]
    [(2, ["A", "B", "C"]), (2, ["A", "C", "B"])]
This simplicial complex consists of 3 vertices (labeled "A", "B", and "C"), 3 edges (connecting the vertices "A" and "B", "B" and "C", and "C" and "A"), and 2 triangles (formed by the vertices "A", "B", and "C", and "A", "C", and "B").

With this definition of SimplicialComplex, it is possible to distinguish between simplices of different dimensions based on the value of the first element in each pair. For example, you could define a tetrahedron as follows:

Copy code
tetrahedron : SimplicialComplex String
tetrahedron =
  mkSimplicialComplex
    ["A", "B", "C", "D"]
    [("A", "B"), ("A", "C"), ("A", "D"), ("B", "C"), ("B", "D"), ("C", "D")]
    [(3, ["A", "B", "C", "D"])]
This simplicial complex consists of 4 vertices (labeled "A", "B", "C", and "D"), 6 edges (connecting the vertices "A" and "B", "A