[Agda] chatgpt and agda
warrick scott
wmacmil at gmail.com
Mon Dec 19 22:25:14 CET 2022
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
More information about the Agda
mailing list