Cubical {{Agda}}: {{A}} Dependently Typed Programming Language with Univalence and Higher Inductive Types