The WG on Informal Type Theory has discussed the merits and demerits of various notations and terminologies in HoTT. This page serves as a place to collect this feedback, especially to inform editorial decisions in The book.

Notation

Definitional/judgmental equality

  • x = y
    • Con: we might want to save this for propositional equality
  • x \equiv y
  • x := y
  • nothing
    • Pro: maybe that in informal type theory we can completely avoid talking about judgemental equality
    • Con: maybe not

Propositional equality / paths
  • x =_A y
  • x = y
    • Pro: at least for hsets, this is the closest we get to what mathematicians are used to call "="
    • Con: for non-hsets, it doesn't behave as much like equality
  • x \overset{p}{=} y
    • Pro: simple notation for chaining labeled equalities together
    • Con: gets unwieldy if p is a long expression
  • Id_A(x,y)
    • Con: hard to chain together
  • Eq_A(x,y)
  • x ~> y
    • Pro: in directed HoTT that might be a good notation
    • Con: we only have undirected HoTT so far
  • Paths_A(x,y)
    • Con: Potential conflict with actual continuous paths, when we start doing actual topology in HoTT

Map on paths / action of f : A -> B on a path p in A

  • f[p]
  • f(p)
    • Pro: similar to existing mathematical notation for functors
    • Con: might be confusing to newcomers
  • f_1(p)
  • resp f p
    • Con: doesn't suggest that p is a structure rather than a property
  • map f p
    • Con: the word "map" doesn't really convey the intended meaning
  • ap f p (for "APply" or "Action on Paths")

Transport of u : P(x) along p to P(y)

  • p^*_P u
  • p_* u
  • p_\# u
  • transport^P(p,u)
  • (ap P p) u (implicit use of univalence)

Dependent map / action of f : \Pi x:A.P(x) on a path p in A

  • f⟦A⟧
  • same as non dependent map
    • Pro: up to computation rules that should be definitional, map on paths is a special case of dependent map
    • Con: That’s not true in MLTT because the required computation rule is not definitional

Path composition, diagrammatic order

  • p\cdot q
  • p; q
    • Con: may look weird to a mathematician

Path composition, applicative order

  • p\circ q
    • Pro: in directed HoTT, function composition is a special case of composition of directed paths
    • Con: conflicts with notation for function composition
  • pq

n-truncation of a type A

  • ⟦A⟧_n, with elements [x]_n
    • Con: brackets are used for other things
  • ||A||_n, with elements |x|_n
    • Con: hard to pronounce
  • \tau_n(A), with elements ?
    • Pro: sometimes used in higher category theory
    • Pro: easy to pronounce
  • ?, with elements \tau_n(x)

Terminology

x : A

  • x is an element of A
    • Pro: matches set-theoretic terminology
    • Con: matches set-theoretic terminology
  • x is a term of type A
    • Con: "term" is too syntactic of a notion
  • x is an object in A
  • x is a point in A
  • x is a value in A
    • Con: conflicts with established type-theoretical jargon

Propositional reflection / (-1)-truncation of P

  • It is merely the case that P

Truncation and h-levels

  • 0 is hSets, (-1) is hProp, etc
    • Pro: matches the numbering in homotopy theory and higher category theory
    • Pro: easy to remember: a 1-type is a 1-groupoid.
    • Con: VV has defined "h-levels" differently
  • 2 is hSets, 1 is hProp, etc
    • Pro: starts at zero
    • Con: confusing at least for homotopy theorists and higher category theorists
We could moreover drop the "h" from hSet. Also, we can use 1-Type instead of hlevel 3.