Agda-2.6.0: A dependently typed functional programming language and proof assistant

Tries to primTransp a whole telescope of arguments, following the rule for Σ types. If a type in the telescope does not support transp, transpTel throws it as an exception.
Like transpTel but performing a transpFill.