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.

## Notation

## Definitional/judgmental equality

Con: we might want to save this for propositional equalityPro:maybe that in informal type theory we can completely avoid talking about judgemental equalityCon: maybe notPropositional equality / pathsPro: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 equalityPro: simple notation for chaining labeled equalities togetherCon:gets unwieldy if p is a long expressionCon: hard to chain togetherPro:in directed HoTT that might be a good notationCon:we only have undirected HoTT so farCon: 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

Pro: similar to existing mathematical notation for functorsCon: might be confusing to newcomersCon: doesn't suggest that p is a structure rather than a propertyCon: the word "map" doesn't really convey the intended meaning## Transport of u : P(x) along p to P(y)

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

Pro:up to computation rules that should be definitional, map on paths is a special case of dependent mapCon:That’s not true in MLTT because the required computation rule is not definitional## Path composition, diagrammatic order

Con:may look weird to a mathematician## Path composition, applicative order

Pro:in directed HoTT, function composition is a special case of composition of directed pathsCon:conflicts with notation for function composition## n-truncation of a type A

Con:brackets are used for other thingsCon:hard to pronouncePro:sometimes used in higher category theoryPro:easy to pronounce## Terminology

## x : A

Pro: matches set-theoretic terminologyCon: matches set-theoretic terminologyCon: "term" is too syntactic of a notionCon: conflicts with established type-theoretical jargon## Propositional reflection / (-1)-truncation of P

## Truncation and h-levels

- 0 is hSets, (-1) is hProp, etc

- 2 is hSets, 1 is hProp, etc

We could moreover drop the "h" from hSet. Also, we can use 1-Type instead of hlevel 3.Pro: matches the numbering in homotopy theory and higher category theoryPro: easy to remember: a 1-type is a 1-groupoid.Con: VV has defined "h-levels" differentlyPro:starts at zeroCon: confusing at least for homotopy theorists and higher category theorists