Automating generation of category from structure type

Stream: lean4

[James Randolf]

I was wondering if there's any way I might be able to automate generating a category from a type definition. For example, I can define what a graph is:

structure Graph where
  Vertex : Type
  Edge : Type
  source : Edge → Vertex
  target : Edge → Vertex

and then define what a graph homomorphism is:

structure GraphHomomorphism (G H : Graph) where
  mapVertex : G.Vertex → H.Vertex
  mapEdge : G.Edge → H.Edge
  mapSource : H.source ∘ mapEdge = mapVertex ∘ G.source
  mapTarget : H.target ∘ mapEdge = mapVertex ∘ G.target

and then define composition of homomorphisms, prove it's associative, and prove each graph has an identity homomorphism.

But this whole process could be automated by code to generate a category out of any structure type: the homomorphism type would get a mapXfield for each field x in the original structure, whose type is the homomorphism type for the field type (with Type-homomorphisms being functions, and X -> Y-homomorphisms being commutative squares).

Ideally I could then just do def graphCategory : Category := generateCategory Graph and it would auto-generate everything.

Has something like this been done before?

[Kevin Buzzard]

I think that the nearest we have to this is docs#CategoryTheory.Bundled .

One issue with pushing this further is that you can't guess the morphisms in general. For example let's say I gave you the definition of a topological space or a scheme. It's not at all obvious what the definition of a morphism should be just from a definition of the objects.

[Trebor Huang]

Also when there are contravariant or mixed stuff there's no clear way forward

[Yury G. Kudryashov]

Kevin Buzzard said:

I think that the nearest we have to this is docs#CategoryTheory.Bundled .

One issue with pushing this further is that you can't guess the morphisms in general. For example let's say I gave you the definition of a topological space or a scheme. It's not at all obvious what the definition of a morphism should be just from a definition of the objects.

While it is possible to guess that morphisms of topological spaces are continuous functions by looking at the type of the only data field IsOpen (though I'm not sure that one can guess the right implication), if you look at metric spaces, the task becomes impossible because one can define several meaningful types of morphisms: continuous maps, Lipschitz continuous maps, maps that are Lipschitz continuous with constant 1, isometric maps, dilations, probably more.

[Apurva Nakade]

A middle ground would be to define the morphisms and have a tactic check composition, associativity, and identity properties (when trivial).

[Kevin Buzzard]

We already have aesop for that :-)

[Adam Topaz]

For algebraic-like categories, meaning structures where the data fields are operations on some type, this is certainly possible to automate

[Adam Topaz]

Ideally such automation would become part of a hierarchy builder in the spirit of https://github.com/math-comp/hierarchy-builder

[Scott Morrison]

I think the payoff does not come from automating the construction of the category itself, but all the stuff that comes later "for free" for algebraic categories: limits, filtered colimits preserved by forget, internal objects, etc.

[Scott Morrison]

That would be a cool project!

[Tanner Swett]

As it happens, I've started working on some stuff that will automatically generate a category from a type definition. See: https://github.com/tswett/leanstuff/blob/main/Menagerie/Meta/VarietyInfo/Extract.lean and https://github.com/tswett/leanstuff/blob/main/Menagerie/Meta/VarietyInfo/Synthesize.lean

I've only just barely started; I have a thing that will look at a structure and see what the types in it are, but that's about it. Maybe in a few weeks I'll have something that can automatically generate a category in at least one circumstance.

It's true that in general, you can't guess which way the functions are supposed to do. Initially, I'm just going to assume that all sorts are covariant, and so it won't be possible to define a topological space. Eventually, I'll probably add a mechanism for specifying whether a sort is covariant (a morphism A -> B contains a function A.whatever -> B.whatever), contravariant (a morphism A -> B contains a function B.whatever -> A.whatever), or invariant (a morphism A -> B contains a bijection A.whatever <-> B.whatever).