chore: gardening

[ncfavier]

Expose the Finite→H-Level instance (but mark it INCOHERENT) and other trivial fixes.

Most typos were found using typos.

_typos.toml

[files]
extend-exclude = ["support", "*.scss", "*.bibtex"]

[default.extend-words]
identicals = "identicals"
intensional = "intensional"
operad = "operad"
projectives = "projectives"
raison = "raison"
substituters = "substituters"

# parts of identifiers
ba = "ba"
cancell = "cancell"
DNE = "DNE"
fo = "fo"
Iy = "Iy"
hom = "hom"
lits = "lits"
ment = "ment"
mor = "mor"
nam = "nam"
nto = "nto"
padd = "padd"
pn = "pn"
Singl = "Singl"
SinglP = "SinglP"
som = "som"
toi = "toi"
ue = "ue"
unitl = "unitl"

[Lavenza]

Pull request preview

Changed pages

• Cat.Internal.Base (± 6)
• Cat.Displayed.Cocartesian.Weak (± 5)

[ncfavier]

Oh never mind then.

[plt-amy]

Should we set up typos in CI?

[ncfavier]

Your call; I could see that getting annoying.

[plt-amy]

I guess we'll stick without it but it'd be nice to have the config file checked in so we can run it periodically.