Characters for mathematical texts/theorem provers

For mathematical texts (mainly in theorem provers) the following characters would be desirable:

• Uppercase and lowercase Greek letters including several letter variants (\varbeta, \varepsilon, \vartheta, \varkappa, \varpi, \varrho, \varsigma, \varphi, and inverted delda and omega): Α α, Β β/ϐ, Γ γ, Δ δ, Ε ε/ϵ, Ζ ζ, Η η, Θ θ/ϑ, Ι ι, Κ κ/ϰ, Λ λ, Μ μ, Ν ν, Ξ ξ, Ο ο, Π π/ϖ, Ρ ρ/ϱ, Σ σ/ς, Τ τ, Υ υ, Φ φ/ϕ, Χ χ, Ψ ψ, and Ω ω, and ∇, ℧.
• Quantifiers, large sum and large product characters: ∀, ∃, ∄, optionally also ∏, ∐, ∑, ⋂, ⋃.
• Brackets: ‹›, ⌈⌉, ⌊⌋, ⁽⁾, ₍₎,〈〉, optionally also ⁅⁆, ❬❭, ❲❳, ⟦⟧, ⧘⧙.
• Logical symbols: ⊥, ¬, ∧, ∨, ⊢, ⊣, ⅋, ⊸, optionally also ⊤, ⊨, ⊼, ⊻, ⫤.
• Basic operators: ⋅, ×, ∘, ∗, ⋆, ⊗, ⊕, optionally also ⋉, ⋊, ⊙, ⊖, ⊛, ⊚.
• Letterlikes: ∅, ∂, ∞, optionally also: 𝔹, ℂ, 𝔻, 𝔼, 𝔽, ℍ, ℕ, ℙ, ℚ, ℝ, and ℤ; ℑ, ℜ, ℵ, ℶ, ℘, ℬ.
• Modals: ◊, □, ♦, ʃ, ♯, ♭, ♮, optionally also ⬖, ⬗, ■, ◯, ⬤.
• Relations: ≠, ≟, ≐, ≅, ≈, ≡, ∈, optionally also ⥬, ⋈, ≺, ≼, ≻, ≽, ⊂, ⊃, ⊏, ⊐, ⊲, ⊳, ⩽, ⩾, ⩻.
• Optionally, a great variety of arrows: ordinary, double-stroke, dotted, squiggle, with hook, with double arrowhead, harpoons, from bar, all of them combined with not, tilde, dot above, vertical stroke or double vertical stroke. Examples: ⇏, ⇸, ↠̃, ↦, ⇀̇.

Rarely, combining diacritics for latin and greek letters are also used, namely dot, right arrow, right harpoon, tilde, overline and underline: vector v⃑ or or v⃗., and its derivative v⃗̇.

Originally posted by @akuklev in https://github.com/tonsky/FiraCode/issues/36#issuecomment-808945004

No files or tests are named. Start by reviewing the requested Unicode character groups and the font's current glyph coverage, then define a feasible scope; done means the agreed mathematical characters are added and rendered correctly.