Which would be better for programming using Homotopy type theory Agda or Idris
Agda is definitely the better choice if you're doing Homotopy Type Theory.

Idris has several features that are specifically incompatible with HoTT. Specifically, you can use dependent pattern matching to prove Uniqueness of Identity Proofs (UIP), which, when combined with Univalence, allows you to prove False. There's also a type-case feature which you can use to directly prove False from univalence.
Agda has some features that are specifically designed to enable HoTT. Namely, it has a --without-K option, which ensures that you can't prove UIP or the related Axiom K. There's also a whole language extension for Cubical Type Theory, which uses a special notion of equality gives computational meaning to univalence.

Relevant reading:
Introduction to Univalent Foundations in Agda
Pattern Matching without K
Proof-relevant Unification in Agda
Cubical Agda Paper
Cubical Agda documentation
Cubical Agda tutorial