Definition jsonExtension (e : extensionT) : json :=
  JsonObject [
    ("ID",            JsonString (extensionId e));
    ("VersionMajor",  JsonInteger (extensionVersionMajor e));
    ("VersionMinor",  JsonInteger (extensionVersionMinor e));
    ("Name",          JsonString (extensionName e));
    ("Description",   JsonString (extensionDescription e));
    ("Specification", JsonString (extensionSpecificationURI e));
    ("Sections",      JsonArray (map jsonSectionID (extensionSections e)))
  ].
