(P : amal_type -> Type) `{forall x, IsHSet (P x)} (e : forall w, P (amal_eta w)) (mh : forall (x y : Words) (h1 h2 : H), DPath P (amal_mu_H x y h1 h2) (e (x ++ (inl h1 :: [inl h2]) ++ y)) (e (x ++ [inl (h1 * h2)] ++ y))) (mk : forall (x y : Words) (k1 k2 : K), DPath P (amal_mu_K x y k1 k2) (e (x ++ (inr k1 :: [inr k2]) ++ y)) (e (x ++ [inr (k1 * k2)] ++ y))) (t : forall (x y : Words) (z : G), DPath P (amal_tau x y z) (e (x ++ [inl (f z)] ++ y)) (e (x ++ [inr (g z)] ++ y))) (oh : forall (x y : Words), DPath P (amal_omega_H x y) (e (x ++ [inl mon_unit] ++ y)) (e (x ++ y))) (ok : forall (x y : Words), DPath P (amal_omega_K x y) (e (x ++ [inr mon_unit] ++ y)) (e (x ++ y))) : forall x, P x. Proof. snrapply Trunc_ind; [exact _|]. snrapply Coeq_ind. 1: exact e. intro a. destruct a as [ [ [ [a | a ] | a] | a ] | a ]. + destruct a as [[[x h1] h2] y]. apply dp_compose. exact (mh x y h1 h2). + destruct a as [[[x k1] k2] y]. apply dp_compose. exact (mk x y k1 k2). + destruct a as [[x z] y]. apply dp_compose. exact (t x y z). + destruct a as [x y]. apply dp_compose. exact (oh x y). + destruct a as [x y]. apply dp_compose. exact (ok x y). 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.