Search TypeTopology

• Type a name, a fragment of one, a concept, or a contributor.
• Several words must all match, so "compact ordinal" asks for both.
• Wildcards: * for any run of characters, ? for one, \* for a literal star.
• "compact in Ordinals.Comp", using the keyword in, searches inside a directory or file.
• Unicode is entered the way it is in the Agda emacs mode, so \to and \MCU are "→" and "𝓤", though \to itself needs a space right after it, since \top could still follow.

20,967 definitions and 236 concepts, in 988 modules.

Currently indexed concepts: