def iscoh_wmap {A:Type _}{B:Type _} : (A -> B) -> Type _ :=
  fun f => @Subtype (B -> A) fun r => ∀ a , a = r (f a)
def wmap : Type _ -> Type _ -> Type _ :=
  fun A B => @Sigma (A -> B) fun f => iscoh_wmap f

def hgroup : Nat -> Type _ -> Type _
| .zero , T => wmap T T
| .succ a, T => wmap (hgroup a T) (hgroup a T)

example : hgroup 0 Unit := by
  unfold hgroup
  admit

-- TODO: we should improve univere inference. It should be
-- hgroup.{u} : Nat → Type u → Type u
/--
info: hgroup.{u_1, u_2} : Nat → Type (max u_1 u_2) → Type (max u_1 u_2)
-/
#guard_msgs in
#check hgroup