1

Persistent homology can be used to transform a point-cloud into a simplical complex.

Do such simplical complexes have a first-class representation:

  1. Conceptually, within HoTT?
  2. Concretely, within some existing programming language (e.g. Agda)?
YCor
  • 60,149
NietzscheanAI
  • 261
  • 1
    You can certainly represent a simplicial complex in HoTT or in Agda in essentially the same way you can in ZFC or in C. So, I think this isn't your real question. Related: https://mathoverflow.net/questions/289711/defining-sun-in-hott – Reid Barton Oct 04 '20 at 14:58

0 Answers0