Homotopy Type Theory rational homotopy type > history (Rev #1)

Definition

A pointed type $(T,t)$ is a rational homotopy type if it is 1-connected and all of its homotopy groups? are divisible groups.

isRational(T,t) \coloneqq \prod_{n:\mathbb{N}} \mathrm{isDivisible}\left(\left[\Omega^n(T,t)\right]_0\right) \times \prod_{f:T \to \mathbb{1}} \prod_{a:\mathbb{1}} \mathrm{isContr}\left(\left[\mathrm{fiber}(f, a)\right]_{1}\right)