Twirl

import Time_translation_covariant
import Quantum_channel

def twirl (ρ : ℋ →ₗ[ℂ] ℋ) [quantum_state ρ] : ℋ →ₗ[ℂ] ℋ :=
∑ x, (Π x) ρ (Π x)

instance : quantum_channel twirl := sorry

theorem twirl_is_time_trans_cov :
time_trans_cov twirl := sorry

lemma twirl_eq_dephase_of_nondegerenate_Hamiltonian :
nondegenerate H → twirl = completely_dephasing_channel :=
begin
  sorry
end