Homotopy type theory (HoTT) is usually presented as Martin-Löf’s dependent type theory together with Voevodsky’s univalence axiom and various other axioms for higher inductive types. In particular, the presence of axioms makes it non-constructive in that one can find closed terms of type ℕ which do not reduce to canonical natural numbers. But with Thierry Coquand’s constructive cubical model, it becomes possible to compute with univalence and higher inductive types. In this talk, I will present various examples of such closed natural numbers that we would like to compute, extracted from the proof of π₄(S³)=ℤ/2ℤ in HoTT that I recently completed.