Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: applied category theory

Topic: HoTT GeoML

Ryan Wisnesky (Jun 14 2023 at 23:01):

I'm interested in trying to translate GeoML (GML: https://en.wikipedia.org/wiki/Geography_Markup_Language), a coordinate-based markup language for expressing 3d shapes, into homotopy type theory, in such a way that the topological structure of the GML is reflected in the proof theory (the groupoids induced by propositional equality) of the resulting HoTT code. In the same way that in https://arxiv.org/pdf/1301.3443.pdf the authors calculated the homotopy groups of spheres using HoTT, I'm wondering if we could e.g. calculate some simpler thing about a real world structure for which GML exists (like a famous Church etc) using HoTT methods. Any thoughts?

Ryan Wisnesky (Jun 15 2023 at 00:03):

To elaborate, I know how to write individual shapes such as toruses in HoTT, and I have coordinate lists for shapes in the GeoML file format, such as toruses, I’m just not sure what to do to corresponding HoTT code when those shapes are found to e.g. intersect or touch. Presumably, I should push them out or create suspensions or sewing or do other topological things, but I don't know what these would be. I think there's probably a cool quick demo here (perhaps a 'functional pearl') if this can be worked out.

Spencer Breiner (Jun 15 2023 at 00:55):

Looks cool!

As far as I know, actually extracting computation from a HoTT proof is still intractable. From a 2022 blog post

This result is quite remarkable in that even though it is a constructive proof, it is not at all obvious how to actually compute this n. At the time of writing, we still haven’t managed to extract its value from its definition.

Spencer Breiner (Jun 15 2023 at 00:57):

On the plus side, the "coverages" in GML (geospatial/temporal data) look like (sections of) sheaves :harvest::harvest:

Ryan Wisnesky (Jun 15 2023 at 00:58):

there's a lot of good stuff in GML, imo

Spencer Breiner (Jun 15 2023 at 01:01):

I just glanced over the Wikipedia page briefly. Are you thinking more about the feature set or the available data sets (or both)

Ryan Wisnesky (Jun 15 2023 at 01:01):

Here's an even more precise statement of my "ask". GML defines the concept of polygon, and assume we know how to translate polygons into HoTT (they are like e.g. squares but more so). I'm asking for help exhaustively enumerating all the ways two polygons can overlap, and for each such way, figuring out what to do with the associated HoTT code. For example, assume we have six squares that form a cube. This gives six HoTT inductive types. Based on the fact that the squares overlap on edges, these six types should get merged into one type with six "square" constructors, resulting in the HoTT code for the cube. Presumably, there is some systematic way of doing this that I'm asking for help finding.

Ryan Wisnesky (Jun 15 2023 at 01:03):

btw not all GML is topologically "consistent" (meaning it deviates from ISO spec as well as not specifying anything mathematical). https://www.researchgate.net/publication/333795484_Evaluation_of_Topological_Consistency_in_CityGML

Spencer Breiner (Jun 15 2023 at 01:04):

Do you want intersections in general or shared faces (as in CW-complexes)

Ryan Wisnesky (Jun 15 2023 at 01:07):

whatever would be given by coordinate lists

Ryan Wisnesky (Jun 15 2023 at 01:07):

all that comes out of GML is a bunch of polygon definitions, each with a coordinate list. everything else has to be computed. Other formats like CityML have keywords to specify such relationships, such as "disjoint from"

Ryan Wisnesky (Jun 15 2023 at 01:08):

To be hyper concrete, I can see how to go from six of
**data Square {A : Type} {a00 : A} :
{a01 a10 a11 : A} → a00 == a01 -> a00 == a10 -> a01 == a11 -> a10 == a11 -> Type where
id : Square id id id id**
to one of
**data Cube {A : Type} {a000 : A} :
{a010 a100 a110 a001 a011 a101 a111 : A}
{p0-0 : a000 == a010}
{p-00 : a000 == a100}
{p-10 : a010 == a110}
{p1-0 : a100 == a110}
(f--0 : Square p0-0 p-00 p-10 p1-0) -- left
{p0-1 : a001 == a011}
{p-01 : a001 == a101}
{p-11 : a011 == a111}
{p1-1 : a101 == a111}
(f--1 : Square p0-1 p-01 p-11 p1-1) -- right
{p00- : a000 == a001}
{p01- : a010 == a011}
{p10- : a100 == a101}
{p11- : a110 == a111}
(f0-- : Square p0-0 p00- p01- p0-1) -- back
(f-0- : Square p-00 p00- p10- p-01) -- top
(f-1- : Square p-10 p01- p11- p-11) -- bot
(f1-- : Square p1-0 p10- p11- p1-1) -- front
→ Type where
id : Cube id id id id id id**

when squares match exactly by coordinates (not shown), but there must be a general way to do this for all shapes. No doubt something like this already exists for scene reconstruction, just not targeting HoTT

Spencer Breiner (Jun 15 2023 at 01:11):

In this case, the squares share edges, but in general they might pass through each other, or overlap in a 2-dimensional patch.

You would like to recognize that there is an intersection, even though this is not part of any boundary path

Spencer Breiner (Jun 15 2023 at 01:12):

You could also get families of polygons if the initial patches are not convex

Ryan Wisnesky (Jun 15 2023 at 01:12):

right, and I have no idea how to do geometry or topology or whatever this would be called. would anyone like to figure all this out for the glory of writing a paper?

Spencer Breiner (Jun 15 2023 at 01:18):

I once audited a cool course in computational geometry, but I think I've forgotten everything (except a dim memory of present wrapping making an appearance)

Ryan Wisnesky (Jun 15 2023 at 01:20):

anyone on zulip we might ask?

Ryan Wisnesky (Jun 15 2023 at 01:32):

I think we can assume that given two polygons there is an algorithm to say 'disjoint' or produce a polygon of their intersection (presumably one dimension lower but I can see how two squares might overlap in the same plane). For example http://www.csun.edu/~ctoth/Handbook/chap42.pdf . The part that is tricky, that I think requires topology, is figuring out how to act on the corresponding HoTT code. For example, if the six squares touch in a way that forms a chain, then they become a single bigger rectangle, which in my mind would be implemented by e.g. simplification of a presentation. In other words, from a topological perspective, how many ways are there for two shapes to intersect, and how would each of these yield a presentation of the combined object from presentations of the input objects?

Ryan Wisnesky (Jun 15 2023 at 02:04):

perhaps what is needed is https://en.wikipedia.org/wiki/Surgery_theory but with arbitrary shapes, not spheres, and in terms of presentations

Emilio Minichiello (Jun 15 2023 at 13:28):

It sounds to me like you want something like a proof assistant but with tools to manipulate simplicial complexes, something like https://polymake.org/doku.php/user_guide/tutorials/latest/apps_topaz . Is there a specific homotopical thing you want to exploit using HoTT?

Ryan Wisnesky (Jun 15 2023 at 14:37):

I don't have a clue what to do with the HoTT code that would arise from the GML, but I'm sure we could think of something cool :-)

Alex Gryzlov (Jun 15 2023 at 18:11):

Spencer Breiner said:

As far as I know, actually extracting computation from a HoTT proof is still intractable.

There is some recent work on speeding this stuff up, like https://github.com/AndrasKovacs/cctt :

we have two variations of the Brunerie number. These can be both computed here but only one can be computed in Agda

Spencer Breiner (Jun 15 2023 at 18:26):

Nice! Glad to hear about that

Ryan Wisnesky (Jun 16 2023 at 19:55):

Looks like there is a standard for describing all the ways shapes can overlap, called DE-9IM. https://en.wikipedia.org/wiki/DE-9IM . It defines predicates like "touches" and "crosses" and "covers"

John Baez (Jun 16 2023 at 19:59):

By the way, I'm curious to know how homotopy type theory might help here: I don't see it. For example homotopy type theory has a slick way of defining the circle, but as far as I know the really quick thing to define is the homotopy type of the circle, not the circle as a topological space or the circle as a manifold with a geometry like a Riemannian metric.

John Baez (Jun 16 2023 at 20:00):

Of course you must be able to define the usual round circle in $\mathbb{R}^2$ using homotopy type theory, but I'm not seeing how that offers advantages over the usual way of working with it.... at least not in relatively "mundane" applications like GeoML.

Steve Awodey (Jun 16 2023 at 20:15):

Spencer Breiner said:

Looks cool!

As far as I know, actually extracting computation from a HoTT proof is still intractable. From a 2022 blog post

This result is quite remarkable in that even though it is a constructive proof, it is not at all obvious how to actually compute this n. At the time of writing, we still haven’t managed to extract its value from its definition.

The big news since a year or so is that HoTT now does compute, using cubical Agda.
See:
https://homotopytypetheory.org/2022/06/09/the-brunerie-number-is-2/
It's very impressive!

Steve Awodey (Jun 16 2023 at 20:20):

the 2022 blog post that @Spencer Breiner linked to is quoting from Brunerie's 2016 thesis in order to say that the problem referred to there has now been solved.

Ryan Wisnesky (Jun 16 2023 at 22:21):

I'm not really sure if there will be any interesting information left as a result of this GML to HoTT translation; I don't really know if computing the homotopy type of the EU parliament will be useful for anything more than a cool demo (to, say, the EU parliament). My interest here is actually about automated deduction: I'm keen to explore 'correct-by-construction' ways of manipulating not just coordinate data but things derived from it (such as topologies or homotopy types). The realization that GML needs to be checked for consistency was eye-opening, for example. As another example people can prove SQL queries equivalent using HoTT (https://homotopytypetheory.org/2016/09/26/hottsql-proving-query-rewrites-with-univalent-sql-semantics/) and this kind of trick might work for e.g. GeoSPARQL too, which use primitives based on homotopy type (connectedness and whatnot), in addition to coordinates. (And don't get me started about trying to use RDF/OWL for this purpose).