Some intuition on HoTT in Agda [hca/H00C.lagda]

HoTT is a foundation for mathematics based on MLTT. In HoTT we don’t have sets like in ZFC, but elements of types.

A is a type and x : A is an element of type A.

data A : Type where
  a : A

Pi Types / Dependent function types

id : A -> A
id a = a