Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
let’s give all HoTT-related entries the context menus for “Type theory” and for “Homotopy theory”:
+-- {: .rightHandSide}
+-- {: .toc .clickDown tabindex="0"}
### Context
#### Type theory
+-- {: .hide}
[[!include type theory - contents]]
=--
#### Homotopy theory
+--{: .hide}
[[!include homotopy - contents]]
=--
=--
=--
By the way, I like a minimum of whitespace in type-theoretic formulas to avoid them looking like symbol soup, with standard equivalence- and equality-symbols used in a way that non-insiders cannot parse.
In the case at hand I have introduced whitespace as follows:
\mathrm{equivext}(f, g)
\;\;\colon\;\;
\big(f =_{A \simeq B} g\big)
\;\simeq\;
\prod_{x \colon A}
\;
f(x) =_{B} g(x)
But if this were my entry, I would go further, since I find that using sub-scripted equality signs for identification types is both conceptually ill-conceived as well as a ill-typeset (at least as soon as the subscript has more than one symbol). What I would type is:
\mathrm{equivext}(f, g)
\;\colon\;
Equiv
\bigg(
Id_{A \simeq B}\big(
f,\,g
\big)
,\,
\prod_{x \colon A}
\,
Id_B\big(
f(x)
,\,
g(x)
\big)
\bigg)
which renders intelligibly as:
1 to 2 of 2