(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. Proof. snrapply amal_type_ind. 1: exact _. 1: exact e. all: intros; apply dp_const. 1: apply eh. 1: apply ek. 1: apply t. 1: apply oh. apply ok. Defined.
Require Import Basics Types. Require Import Cubical.DPath. Require Import Spaces.List.Core Spaces.List.Theory. Require Import Colimits.Pushout. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Algebra.Groups.Group. Require Import WildCat.