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.
Created on April 19, 2018 at 21:16:58
by
Univalent foundations special year 2012