< [[nlab:rational homotopy type]] ## Definition ## A pointed type $(T,t)$ is a **rational homotopy type** if it is 1-connected and all of its [[homotopy groups]] are [[torsion-free divisible groups]]. $$isRational(T,t) \coloneqq \prod_{n:\mathbb{N}} \mathrm{isTorsionFree}\left(\left[\Omega^n(T,t)\right]_0\right) \times \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)$$ ## See also ## * [[rational homotopy theory]] * [[rationalization of a simply connected type]] category: not redirected to nlab yet