fact: Definition amal_type_rec (P : Type) `{IsHSet P} (e : Words -> P) (eh : forall (x y : Words) (h1 h2 : H), e (x ++ (cons (inl h1) [inl h2]) ++ y) = e (x ++ [inl (h1 * h2)] ++ y)) (ek : forall (x y : Words) (k1 k2 : K), e (x ++ (cons (inr k1) [inr k2]) ++ y) = e (x ++ [inr (k1 * k2)] ++ y)) (t : forall (x y : Words) (z : G), e (x ++ [inl (f z)] ++ y) = e (x ++ [inr (g z)] ++ y)) (oh : forall (x y : Words), e (x ++ [inl mon_unit] ++ y) = e (x ++ y)) (ok : forall (x y : Words), e (x ++ [inr mon_unit] ++ y) = e (x ++ y)) : amal_type -> P.
imports: Basics Types Cubical Spaces.List Colimits.Pushout Truncations.Core Truncations.SeparatedTrunc Algebra.Groups.Group WildCat