Homotopy type theory in Agda

Samuel Mimram

1 HoTT book vs Agda conventions

1.1 Identity types

HoTT book	Agda
=	`≡`
\(p^{-1}\)	`sym`
transport / \(p_*\)	`subst`
transportconst	`substConst`
transport \((A ↦ A → A)\)	`transport`
ap	`cong`
apd	`congP`
happly	`funExt⁻`

1.2 Products

HoTT book	Agda
pr₁	`fst`
pr₂	`snd`
pair⁼	`Σ≡` or `ΣPathP`