[#14935] feat: add Html type

[downstream-lean4]

This is the adaptation PR for leanprover/lean4#14935. Breakage of verso-web-components is expected to be fixed by upstream Verso changes in leanprover/verso#974.

[downstream-lean4]

Build report for Merge remote-tracking branch 'origin/green' into adaptation-14935

Stayed green

Repo	Critical	Build	Test	Lint
aesop	✅	✅ in 0s	✅ in 4s	⏭️
batteries	✅	✅ in 0s	✅ in 4s	✅ in 2s
import-graph	✅	✅ in 2s	✅ in 4s	⏭️
lean4-cli	✅	✅ in 0s	✅ in 0s	⏭️
mathlib4	✅	✅ in 17m 8s	✅ in 45s	✅ in 1m 36s
plausible	✅	✅ in 0s	✅ in 2s	⏭️
ProofWidgets4	✅	✅ in 1s	✅ in 1s	⏭️
quote4	✅	✅ in 0s	✅ in 1s	⏭️
reference-manual	✅	✅ in 1m 14s	⏭️	⏭️
BibtexQuery		✅ in 3s	⏭️	⏭️
comparator		✅ in 2s	⏭️	⏭️
cslib		✅ in 2s	✅ in 10s	✅ in 3s
doc-gen4		✅ in 7s	⏭️	⏭️
illuminate		✅ in 1s	✅ in 10s	⏭️
lean4-unicode-basic		✅ in 0s	⏭️	⏭️
lean4export		✅ in 0s	✅ in 8s	⏭️
LeanSearchClient		✅ in 0s	✅ in 0s	⏭️
leansqlite		✅ in 7s	✅ in 20s	⏭️
nerodia		✅ in 1s	✅ in 21s	⏭️
repl		✅ in 0s	✅ in 51s	⏭️
verso		✅ in 1m 21s	✅ in 2m 59s	⏭️
verso-slides		✅ in 45s	✅ in 9s	⏭️
verso-web-components		✅ in 15s	⏭️	⏭️

View run