Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Cubical.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.LocalOpen Scope list_scope.LocalOpen Scope mc_scope.LocalOpen Scope mc_mult_scope.(** In this file we define the amalgamated free product of a span of group homomorphisms as a HIT. *)(** We wish to define the amalgamated free product of a span of group homomorphisms f : G -> H, g : G -> K as the following HIT: HIT M(f,g) | amal_eta : list (H + K) -> M(f,g) | mu_H : forall (x y : list (H + K)) (h1 h2 : H), amal_eta (x ++ [inl h1, inl h2] ++ y) = amal_eta (x ++ [inl (h1 * h2)] ++ y) | mu_K : forall (x y : list (H + K)) (k1 k2 : K), amal_eta (x ++ [inr k1, inr k2] ++ y) = amal_eta (x ++ [inr (k1 * k2)] ++ y) | tau : forall (x y : list (H + K)) (z : G), amal_eta (x ++ [inl (f z)] ++ y) = amal_eta (x ++ [inr (g z)] ++ y) | omega_H : forall (x y : list (H + K)), amal_eta (x ++ [inl mon_unit] ++ y) = amal_eta (x ++ y) | omega_K : forall (x y : list (H + K)), amal_eta (x ++ [inr mon_unit] ++ y) = amal_eta (x ++ y). We will build this HIT up sucessively out of coequalizers. *)(** We will call M [amal_type] and prefix all the constructors with [amal_] (for amalgmated free product). *)SectionFreeProduct.Context (GHK : Group)
(f : GroupHomomorphism G H) (g : GroupHomomorphism G K).Local DefinitionWords : Type := list (H + K).LocalNotation"[ x ]" := (cons x nil).
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words
x ++ nil = x
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words
x ++ nil = x
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K a: (H + K)%type x: list (H + K) IHx: x ++ nil = x
(a :: x) ++ nil = a :: x
cbn; f_ap.Defined.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, y, z: Words
x ++ y ++ z = (x ++ y) ++ z
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, y, z: Words
x ++ y ++ z = (x ++ y) ++ z
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K y: Words
forallxz : Words, x ++ y ++ z = (x ++ y) ++ z
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, z: Words
x ++ nil ++ z = (x ++ nil) ++ z
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K a: (H + K)%type y: list (H + K) IHy: forallxz : Words, x ++ y ++ z = (x ++ y) ++ z x, z: Words
x ++ (a :: y) ++ z = (x ++ a :: y) ++ z
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, z: Words
x ++ nil ++ z = (x ++ nil) ++ z
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, z: Words
x ++ nil = x
apply word_concat_w_nil.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K a: (H + K)%type y: list (H + K) IHy: forallxz : Words, x ++ y ++ z = (x ++ y) ++ z x, z: Words
x ++ (a :: y) ++ z = (x ++ a :: y) ++ z
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K a: (H + K)%type x: Words
forall (z : Words) (y : list (H + K)),
(forallxz0 : Words, x ++ y ++ z0 = (x ++ y) ++ z0) ->
x ++ a :: y ++ z = (x ++ a :: y) ++ z
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K a, a0: (H + K)%type x: list (H + K) IHx: forall (z : Words) (y : list (H + K)),
(forallxz0 : Words, x ++ y ++ z0 = (x ++ y) ++ z0) ->
x ++ a :: y ++ z = (x ++ a :: y) ++ z
forall (z : Words) (y : list (H + K)),
(forallxz0 : Words, x ++ y ++ z0 = (x ++ y) ++ z0) ->
(a0 :: x) ++ a :: y ++ z = ((a0 :: x) ++ a :: y) ++ z
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K a, a0: (H + K)%type x: list (H + K) IHx: forall (z : Words) (y : list (H + K)),
(forallxz0 : Words, x ++ y ++ z0 = (x ++ y) ++ z0) ->
x ++ a :: y ++ z = (x ++ a :: y) ++ z z: Words y: list (H + K) IHy: forallxz : Words, x ++ y ++ z = (x ++ y) ++ z
(a0 :: x) ++ a :: y ++ z = ((a0 :: x) ++ a :: y) ++ z
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K a, a0: (H + K)%type x: list (H + K) IHx: forall (z : Words) (y : list (H + K)),
(forallxz0 : Words, x ++ y ++ z0 = (x ++ y) ++ z0) ->
x ++ a :: y ++ z = (x ++ a :: y) ++ z z: Words y: list (H + K) IHy: forallxz : Words, x ++ y ++ z = (x ++ y) ++ z
x ++ a :: y ++ z = (x ++ a :: y) ++ z
apply IHx, IHy.Defined.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K word_inverse: Words -> Words x: Words
Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K word_inverse: Words -> Words x: Words
Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K word_inverse: Words -> Words
Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K word_inverse: Words -> Words x: (H + K)%type xs: list (H + K)
Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K word_inverse: Words -> Words x: (H + K)%type xs: list (H + K)
Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K word_inverse: Words -> Words h: H xs: list (H + K)
Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K word_inverse: Words -> Words k: K xs: list (H + K)
Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K word_inverse: Words -> Words h: H xs: list (H + K)
Words
exact ((word_inverse xs) ++ [inl (- h)]).
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K word_inverse: Words -> Words k: K xs: list (H + K)
Words
exact ((word_inverse xs) ++ [inr (- k)]).Defined.(** Inversion changes order of concatenation. *)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, y: Words
word_inverse (x ++ y) =
word_inverse y ++ word_inverse x
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, y: Words
word_inverse (x ++ y) =
word_inverse y ++ word_inverse x
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K y: Words
word_inverse (nil ++ y) =
word_inverse y ++ word_inverse nil
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: (H + K)%type xs: list (H + K) y: Words IHxs: word_inverse (xs ++ y) =
word_inverse y ++ word_inverse xs
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K y: Words
word_inverse (nil ++ y) =
word_inverse y ++ word_inverse nil
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K y: Words
word_inverse y ++ word_inverse nil =
word_inverse (nil ++ y)
apply word_concat_w_nil.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: (H + K)%type xs: list (H + K) y: Words IHxs: word_inverse (xs ++ y) =
word_inverse y ++ word_inverse xs
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: (H + K)%type xs: list (H + K) y: Words IHxs: word_inverse (xs ++ y) =
word_inverse y ++ word_inverse xs
match x with
| inl g => word_inverse (xs ++ y) ++ [inl (- g)]
| inr g => word_inverse (xs ++ y) ++ [inr (- g)]
end =
word_inverse y ++
match x with
| inl g => word_inverse xs ++ [inl (- g)]
| inr g => word_inverse xs ++ [inr (- g)]
end
destruct x; refine (_ @ (word_concat_w_ww _ _ _)^); f_ap.Defined.(** There are five source types for the path constructors. We will construct this HIT as the colimit of five forks going into [Words]. We can bundle up this colimit as a single coequalizer. *)(** Source types of path constructors *)Local Definitionpc1 : Type := Words * H * H * Words.Local Definitionpc2 : Type := Words * K * K * Words.Local Definitionpc3 : Type := Words * G * Words.Local Definitionpc4 : Type := Words * Words.Local Definitionpc5 : Type := Words * Words.(** End points of the first path constructor *)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc1 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc1 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words h1, h2: H y: Words
Words
exact (x ++ (inl h1 :: [inl h2]) ++ y).Defined.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc1 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc1 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words h1, h2: H y: Words
Words
exact (x ++ [inl (h1 * h2)] ++ y).Defined.(** End points of the second path construct *)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc2 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc2 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words k1, k2: K y: Words
Words
exact (x ++ (inr k1 :: [inr k2]) ++ y).Defined.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc2 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc2 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words k1, k2: K y: Words
Words
exact (x ++ [inr (k1 * k2)] ++ y).Defined.(** End points of the third path constructor *)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc3 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc3 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words z: G y: Words
Words
exact (x ++ [inl (f z)] ++ y).Defined.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc3 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc3 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words z: G y: Words
Words
exact (x ++ [inr (g z)] ++ y).Defined.(** End points of the fourth path constructor *)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc4 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc4 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, y: Words
Words
exact (x ++ [inl mon_unit] ++ y).Defined.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc4 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc4 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, y: Words
Words
exact (x ++ y).Defined.(** End points of the fifth path constructor *)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc5 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc5 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, y: Words
Words
exact (x ++ [inr mon_unit] ++ y).Defined.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc5 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc5 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, y: Words
Words
exact (x ++ y).Defined.(** We can then define maps going into words consisting of the corresponding endpoints of the path constructors. *)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc1 + pc2 + pc3 + pc4 + pc5 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc1 + pc2 + pc3 + pc4 + pc5 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: pc1
Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: pc2
Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: pc3
Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: pc4
Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: pc5
Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: pc1
Words
exact (m1 x).
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: pc2
Words
exact (m2 x).
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: pc3
Words
exact (m3 x).
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: pc4
Words
exact (m4 x).
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: pc5
Words
exact (m5 x).Defined.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc1 + pc2 + pc3 + pc4 + pc5 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
pc1 + pc2 + pc3 + pc4 + pc5 -> Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: pc1
Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: pc2
Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: pc3
Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: pc4
Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: pc5
Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: pc1
Words
exact (m1' x).
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: pc2
Words
exact (m2' x).
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: pc3
Words
exact (m3' x).
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: pc4
Words
exact (m4' x).
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: pc5
Words
exact (m5' x).Defined.(** Finally we can define our type as the 0-truncation of the coequalizer of these maps *)Definitionamal_type : Type := Tr 0 (Coeq map1 map2).(** We can define the constructors *)Definitionamal_eta : Words -> amal_type := tr o coeq.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, y: Words h1, h2: H
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, y: Words
coeq (x ++ [inr mon_unit] ++ y) = coeq (x ++ y)
exact (cglue (inr (x,y))).Defined.(** Now we can derive the dependent eliminator *)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y))
forallx : amal_type, P x
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y))
forallx : amal_type, P x
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y))
foralla : Coeq map1 map2, P (tr a)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y))
foralla : Words,
(funw : Coeq map1 map2 => P (tr w)) (coeq a)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y))
forallb : pc1 + pc2 + pc3 + pc4 + pc5,
transport (funw : Coeq map1 map2 => P (tr w))
(cglue b) (?coeq' (map1 b)) = ?coeq' (map2 b)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y))
forallb : pc1 + pc2 + pc3 + pc4 + pc5,
transport (funw : Coeq map1 map2 => P (tr w))
(cglue b) (e (map1 b)) = e (map2 b)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) a: (pc1 + pc2 + pc3 + pc4 + pc5)%type
transport (funw : Coeq map1 map2 => P (tr w))
(cglue a) (e (map1 a)) = e (map2 a)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) a: pc1
transport (funw : Coeq map1 map2 => P (tr w))
(cglue (inl (inl (inl (inl a)))))
(e (map1 (inl (inl (inl (inl a)))))) =
e (map2 (inl (inl (inl (inl a)))))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) a: pc2
transport (funw : Coeq map1 map2 => P (tr w))
(cglue (inl (inl (inl (inr a)))))
(e (map1 (inl (inl (inl (inr a)))))) =
e (map2 (inl (inl (inl (inr a)))))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) a: pc3
transport (funw : Coeq map1 map2 => P (tr w))
(cglue (inl (inl (inr a))))
(e (map1 (inl (inl (inr a))))) =
e (map2 (inl (inl (inr a))))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) a: pc4
transport (funw : Coeq map1 map2 => P (tr w))
(cglue (inl (inr a))) (e (map1 (inl (inr a)))) =
e (map2 (inl (inr a)))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) a: pc5
transport (funw : Coeq map1 map2 => P (tr w))
(cglue (inr a)) (e (map1 (inr a))) =
e (map2 (inr a))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) a: pc1
transport (funw : Coeq map1 map2 => P (tr w))
(cglue (inl (inl (inl (inl a)))))
(e (map1 (inl (inl (inl (inl a)))))) =
e (map2 (inl (inl (inl (inl a)))))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) x: Words h1, h2: H y: Words
transport (funw : Coeq map1 map2 => P (tr w))
(cglue (inl (inl (inl (inl (x, h1, h2, y))))))
(e (map1 (inl (inl (inl (inl (x, h1, h2, y))))))) =
e (map2 (inl (inl (inl (inl (x, h1, h2, y))))))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) x: Words h1, h2: H y: Words
DPath P
(ap tr
(cglue (inl (inl (inl (inl (x, h1, h2, y)))))))
(e (map1 (inl (inl (inl (inl (x, h1, h2, y)))))))
(e (map2 (inl (inl (inl (inl (x, h1, h2, y)))))))
exact (mh x y h1 h2).
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) a: pc2
transport (funw : Coeq map1 map2 => P (tr w))
(cglue (inl (inl (inl (inr a)))))
(e (map1 (inl (inl (inl (inr a)))))) =
e (map2 (inl (inl (inl (inr a)))))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) x: Words k1, k2: K y: Words
transport (funw : Coeq map1 map2 => P (tr w))
(cglue (inl (inl (inl (inr (x, k1, k2, y))))))
(e (map1 (inl (inl (inl (inr (x, k1, k2, y))))))) =
e (map2 (inl (inl (inl (inr (x, k1, k2, y))))))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) x: Words k1, k2: K y: Words
DPath P
(ap tr
(cglue (inl (inl (inl (inr (x, k1, k2, y)))))))
(e (map1 (inl (inl (inl (inr (x, k1, k2, y)))))))
(e (map2 (inl (inl (inl (inr (x, k1, k2, y)))))))
exact (mk x y k1 k2).
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) a: pc3
transport (funw : Coeq map1 map2 => P (tr w))
(cglue (inl (inl (inr a))))
(e (map1 (inl (inl (inr a))))) =
e (map2 (inl (inl (inr a))))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) x: Words z: G y: Words
transport (funw : Coeq map1 map2 => P (tr w))
(cglue (inl (inl (inr (x, z, y)))))
(e (map1 (inl (inl (inr (x, z, y)))))) =
e (map2 (inl (inl (inr (x, z, y)))))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) x: Words z: G y: Words
DPath P (ap tr (cglue (inl (inl (inr (x, z, y))))))
(e (map1 (inl (inl (inr (x, z, y))))))
(e (map2 (inl (inl (inr (x, z, y))))))
exact (t x y z).
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) a: pc4
transport (funw : Coeq map1 map2 => P (tr w))
(cglue (inl (inr a))) (e (map1 (inl (inr a)))) =
e (map2 (inl (inr a)))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) x, y: Words
transport (funw : Coeq map1 map2 => P (tr w))
(cglue (inl (inr (x, y))))
(e (map1 (inl (inr (x, y))))) =
e (map2 (inl (inr (x, y))))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) x, y: Words
DPath P (ap tr (cglue (inl (inr (x, y)))))
(e (map1 (inl (inr (x, y)))))
(e (map2 (inl (inr (x, y)))))
exact (oh x y).
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) a: pc5
transport (funw : Coeq map1 map2 => P (tr w))
(cglue (inr a)) (e (map1 (inr a))) =
e (map2 (inr a))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) x, y: Words
transport (funw : Coeq map1 map2 => P (tr w))
(cglue (inr (x, y))) (e (map1 (inr (x, y)))) =
e (map2 (inr (x, y)))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHSet (P x) e: forallw : Words, P (amal_eta w) mh: forall (xy : Words) (h1h2 : 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 (xy : Words) (k1k2 : 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 (xy : Words) (z : G),
DPath P (amal_tau x y z)
(e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y)) oh: forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y)) x, y: Words
DPath P (ap tr (cglue (inr (x, y))))
(e (map1 (inr (x, y)))) (e (map2 (inr (x, y))))
exact (ok x y).Defined.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHProp (P x) e: forallw : Words, P (amal_eta w)
forallx : amal_type, P x
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHProp (P x) e: forallw : Words, P (amal_eta w)
forallx : amal_type, P x
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHProp (P x) e: forallw : Words, P (amal_eta w)
forallw : Words, P (amal_eta w)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHProp (P x) e: forallw : Words, P (amal_eta w)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHProp (P x) e: forallw : Words, P (amal_eta w)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHProp (P x) e: forallw : Words, P (amal_eta w)
forall (xy : Words) (z : G),
DPath P (amal_tau x y z) (?e (x ++ [inl (f z)] ++ y))
(?e (x ++ [inr (g z)] ++ y))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHProp (P x) e: forallw : Words, P (amal_eta w)
forallxy : Words,
DPath P (amal_omega_H x y)
(?e (x ++ [inl mon_unit] ++ y)) (?e (x ++ y))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHProp (P x) e: forallw : Words, P (amal_eta w)
forallxy : Words,
DPath P (amal_omega_K x y)
(?e (x ++ [inr mon_unit] ++ y)) (?e (x ++ y))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHProp (P x) e: forallw : Words, P (amal_eta w)
forall (xy : Words) (h1h2 : H),
DPath P (amal_mu_H x y h1 h2)
(e (x ++ [inl h1; inl h2] ++ y))
(e (x ++ [inl (h1 * h2)] ++ y))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHProp (P x) e: forallw : Words, P (amal_eta w)
forall (xy : Words) (k1k2 : K),
DPath P (amal_mu_K x y k1 k2)
(e (x ++ [inr k1; inr k2] ++ y))
(e (x ++ [inr (k1 * k2)] ++ y))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHProp (P x) e: forallw : Words, P (amal_eta w)
forall (xy : Words) (z : G),
DPath P (amal_tau x y z) (e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHProp (P x) e: forallw : Words, P (amal_eta w)
forallxy : Words,
DPath P (amal_omega_H x y)
(e (x ++ [inl mon_unit] ++ y)) (e (x ++ y))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: amal_type -> Type H0: forallx : amal_type, IsHProp (P x) e: forallw : Words, P (amal_eta w)
forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr mon_unit] ++ y)) (e (x ++ y))
all: intros; apply path_ishprop.Defined.(** From which we can derive the non-dependent eliminator / recursion principle *)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y)
amal_type -> P
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y)
amal_type -> P
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y)
forall (xy : Words) (h1h2 : H),
DPath (fun_ : amal_type => P) (amal_mu_H x y h1 h2)
(e (x ++ [inl h1; inl h2] ++ y))
(e (x ++ [inl (h1 * h2)] ++ y))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y)
forall (xy : Words) (k1k2 : K),
DPath (fun_ : amal_type => P)
(amal_mu_K x y k1 k2)
(e (x ++ [inr k1; inr k2] ++ y))
(e (x ++ [inr (k1 * k2)] ++ y))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y)
forall (xy : Words) (z : G),
DPath (fun_ : amal_type => P)
(amal_tau x y z) (e (x ++ [inl (f z)] ++ y))
(e (x ++ [inr (g z)] ++ y))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y)
forallxy : Words,
DPath (fun_ : amal_type => P)
(amal_omega_H x y) (e (x ++ [inl mon_unit] ++ y))
(e (x ++ y))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y)
forallxy : Words,
DPath (fun_ : amal_type => P)
(amal_omega_K x y) (e (x ++ [inr mon_unit] ++ y))
(e (x ++ y))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y) x, y: Words h1, h2: H
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y) x, y: Words k1, k2: K
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y) x, y: Words z: G
e (x ++ [inl (f z)] ++ y) = e (x ++ [inr (g z)] ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y) x, y: Words
e (x ++ [inl mon_unit] ++ y) = e (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y) x, y: Words
e (x ++ [inr mon_unit] ++ y) = e (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y) x, y: Words k1, k2: K
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y) x, y: Words z: G
e (x ++ [inl (f z)] ++ y) = e (x ++ [inr (g z)] ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y) x, y: Words
e (x ++ [inl mon_unit] ++ y) = e (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y) x, y: Words
e (x ++ [inr mon_unit] ++ y) = e (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y) x, y: Words z: G
e (x ++ [inl (f z)] ++ y) = e (x ++ [inr (g z)] ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y) x, y: Words
e (x ++ [inl mon_unit] ++ y) = e (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y) x, y: Words
e (x ++ [inr mon_unit] ++ y) = e (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y) x, y: Words
e (x ++ [inl mon_unit] ++ y) = e (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y) x, y: Words
e (x ++ [inr mon_unit] ++ y) = e (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Type IsHSet0: IsHSet P e: Words -> P eh: forall (xy : Words) (h1h2 : H),
e (x ++ [inl h1; inl h2] ++ y) =
e (x ++ [inl (h1 * h2)] ++ y) ek: forall (xy : Words) (k1k2 : K),
e (x ++ [inr k1; inr k2] ++ y) =
e (x ++ [inr (k1 * k2)] ++ y) t: forall (xy : Words) (z : G),
e (x ++ [inl (f z)] ++ y) =
e (x ++ [inr (g z)] ++ y) oh: forallxy : Words,
e (x ++ [inl mon_unit] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr mon_unit] ++ y) = e (x ++ y) x, y: Words
e (x ++ [inr mon_unit] ++ y) = e (x ++ y)
apply ok.Defined.(** Now for the group structure *)(** The group operation is concatenation of the underlying list. Most of the work is spent showing that it respects the path constructors. *)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
SgOp amal_type
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
SgOp amal_type
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K y: amal_type
amal_type -> amal_type
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words
amal_type -> amal_type
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words
forall (y : amal_type) (y0 : Words) (z : G),
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z0 : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl h1; inl h2] ++ z0)) @
amal_mu_H (x ++ y1) z0 h1 h2) @
ap amal_eta
(word_concat_w_ww x y1 ([inl (h1 * h2)] ++ z0))^)
(fun (y1z0 : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr k1; inr k2] ++ z0)) @
amal_mu_K (x ++ y1) z0 k1 k2) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (k1 * k2)] ++ z0))^)
(fun (y1w : Words) (z0 : G) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl (f z0)] ++ w)) @
amal_tau (x ++ y1) w z0) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (g z0)] ++ w))^)
(funy1z0 : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl mon_unit] ++ z0)) @
amal_omega_H (x ++ y1) z0) @
ap amal_eta (word_concat_w_ww x y1 z0)^)
(funy1z0 : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr mon_unit] ++ z0)) @
amal_omega_K (x ++ y1) z0) @
ap amal_eta (word_concat_w_ww x y1 z0)^) y)
(x ++ [inl (f z)] ++ y0) =
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z0 : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl h1; inl h2] ++ z0)) @
amal_mu_H (x ++ y1) z0 h1 h2) @
ap amal_eta
(word_concat_w_ww x y1 ([inl (h1 * h2)] ++ z0))^)
(fun (y1z0 : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr k1; inr k2] ++ z0)) @
amal_mu_K (x ++ y1) z0 k1 k2) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (k1 * k2)] ++ z0))^)
(fun (y1w : Words) (z0 : G) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl (f z0)] ++ w)) @
amal_tau (x ++ y1) w z0) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (g z0)] ++ w))^)
(funy1z0 : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl mon_unit] ++ z0)) @
amal_omega_H (x ++ y1) z0) @
ap amal_eta (word_concat_w_ww x y1 z0)^)
(funy1z0 : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr mon_unit] ++ z0)) @
amal_omega_K (x ++ y1) z0) @
ap amal_eta (word_concat_w_ww x y1 z0)^) y)
(x ++ [inr (g z)] ++ y0)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words
forall (y : amal_type) (y0 : Words),
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl h1; inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(word_concat_w_ww x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr k1; inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^) y)
(x ++ [inl mon_unit] ++ y0) =
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl h1; inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(word_concat_w_ww x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr k1; inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^) y)
(x ++ y0)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words
forall (y : amal_type) (y0 : Words),
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl h1; inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(word_concat_w_ww x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr k1; inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^) y)
(x ++ [inr mon_unit] ++ y0) =
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl h1; inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(word_concat_w_ww x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr k1; inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^) y)
(x ++ y0)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words
forall (y : amal_type) (y0 : Words) (z : G),
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z0 : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl h1; inl h2] ++ z0)) @
amal_mu_H (x ++ y1) z0 h1 h2) @
ap amal_eta
(word_concat_w_ww x y1 ([inl (h1 * h2)] ++ z0))^)
(fun (y1z0 : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr k1; inr k2] ++ z0)) @
amal_mu_K (x ++ y1) z0 k1 k2) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (k1 * k2)] ++ z0))^)
(fun (y1w : Words) (z0 : G) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl (f z0)] ++ w)) @
amal_tau (x ++ y1) w z0) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (g z0)] ++ w))^)
(funy1z0 : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl mon_unit] ++ z0)) @
amal_omega_H (x ++ y1) z0) @
ap amal_eta (word_concat_w_ww x y1 z0)^)
(funy1z0 : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr mon_unit] ++ z0)) @
amal_omega_K (x ++ y1) z0) @
ap amal_eta (word_concat_w_ww x y1 z0)^) y)
(x ++ [inl (f z)] ++ y0) =
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z0 : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl h1; inl h2] ++ z0)) @
amal_mu_H (x ++ y1) z0 h1 h2) @
ap amal_eta
(word_concat_w_ww x y1 ([inl (h1 * h2)] ++ z0))^)
(fun (y1z0 : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr k1; inr k2] ++ z0)) @
amal_mu_K (x ++ y1) z0 k1 k2) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (k1 * k2)] ++ z0))^)
(fun (y1w : Words) (z0 : G) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl (f z0)] ++ w)) @
amal_tau (x ++ y1) w z0) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (g z0)] ++ w))^)
(funy1z0 : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl mon_unit] ++ z0)) @
amal_omega_H (x ++ y1) z0) @
ap amal_eta (word_concat_w_ww x y1 z0)^)
(funy1z0 : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr mon_unit] ++ z0)) @
amal_omega_K (x ++ y1) z0) @
ap amal_eta (word_concat_w_ww x y1 z0)^) y)
(x ++ [inr (g z)] ++ y0)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, y: Words z: G
forallr : amal_type,
(funx : Words =>
amal_type_rec amal_type
(funy : Words => amal_eta (x ++ y))
(fun (yz : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y ([inl h1; inl h2] ++ z)) @
amal_mu_H (x ++ y) z h1 h2) @
ap amal_eta
(word_concat_w_ww x y ([inl (h1 * h2)] ++ z))^)
(fun (yz : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y ([inr k1; inr k2] ++ z)) @
amal_mu_K (x ++ y) z k1 k2) @
ap amal_eta
(word_concat_w_ww x y ([inr (k1 * k2)] ++ z))^)
(fun (yw : Words) (z : G) =>
(ap amal_eta
(word_concat_w_ww x y ([inl (f z)] ++ w)) @
amal_tau (x ++ y) w z) @
ap amal_eta
(word_concat_w_ww x y ([inr (g z)] ++ w))^)
(funyz : Words =>
(ap amal_eta
(word_concat_w_ww x y ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y) z) @
ap amal_eta (word_concat_w_ww x y z)^)
(funyz : Words =>
(ap amal_eta
(word_concat_w_ww x y ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y) z) @
ap amal_eta (word_concat_w_ww x y z)^) r)
(x ++ [inl (f z)] ++ y) =
(funx : Words =>
amal_type_rec amal_type
(funy : Words => amal_eta (x ++ y))
(fun (yz : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y ([inl h1; inl h2] ++ z)) @
amal_mu_H (x ++ y) z h1 h2) @
ap amal_eta
(word_concat_w_ww x y ([inl (h1 * h2)] ++ z))^)
(fun (yz : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y ([inr k1; inr k2] ++ z)) @
amal_mu_K (x ++ y) z k1 k2) @
ap amal_eta
(word_concat_w_ww x y ([inr (k1 * k2)] ++ z))^)
(fun (yw : Words) (z : G) =>
(ap amal_eta
(word_concat_w_ww x y ([inl (f z)] ++ w)) @
amal_tau (x ++ y) w z) @
ap amal_eta
(word_concat_w_ww x y ([inr (g z)] ++ w))^)
(funyz : Words =>
(ap amal_eta
(word_concat_w_ww x y ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y) z) @
ap amal_eta (word_concat_w_ww x y z)^)
(funyz : Words =>
(ap amal_eta
(word_concat_w_ww x y ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y) z) @
ap amal_eta (word_concat_w_ww x y z)^) r)
(x ++ [inr (g z)] ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, y: Words z: G
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words
forall (y : amal_type) (y0 : Words),
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl h1; inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(word_concat_w_ww x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr k1; inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^) y)
(x ++ [inl mon_unit] ++ y0) =
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl h1; inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(word_concat_w_ww x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr k1; inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^) y)
(x ++ y0)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words
forall (y : amal_type) (y0 : Words),
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl h1; inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(word_concat_w_ww x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr k1; inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^) y)
(x ++ [inr mon_unit] ++ y0) =
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl h1; inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(word_concat_w_ww x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr k1; inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^) y)
(x ++ y0)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words
forall (y : amal_type) (y0 : Words),
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl h1; inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(word_concat_w_ww x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr k1; inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^) y)
(x ++ [inl mon_unit] ++ y0) =
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl h1; inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(word_concat_w_ww x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr k1; inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^) y)
(x ++ y0)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, z: Words
forallr : amal_type,
(funx : Words =>
amal_type_rec amal_type
(funy : Words => amal_eta (x ++ y))
(fun (yz : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y ([inl h1; inl h2] ++ z)) @
amal_mu_H (x ++ y) z h1 h2) @
ap amal_eta
(word_concat_w_ww x y ([inl (h1 * h2)] ++ z))^)
(fun (yz : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y ([inr k1; inr k2] ++ z)) @
amal_mu_K (x ++ y) z k1 k2) @
ap amal_eta
(word_concat_w_ww x y ([inr (k1 * k2)] ++ z))^)
(fun (yw : Words) (z : G) =>
(ap amal_eta
(word_concat_w_ww x y ([inl (f z)] ++ w)) @
amal_tau (x ++ y) w z) @
ap amal_eta
(word_concat_w_ww x y ([inr (g z)] ++ w))^)
(funyz : Words =>
(ap amal_eta
(word_concat_w_ww x y ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y) z) @
ap amal_eta (word_concat_w_ww x y z)^)
(funyz : Words =>
(ap amal_eta
(word_concat_w_ww x y ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y) z) @
ap amal_eta (word_concat_w_ww x y z)^) r)
(x ++ [inl mon_unit] ++ z) =
(funx : Words =>
amal_type_rec amal_type
(funy : Words => amal_eta (x ++ y))
(fun (yz : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y ([inl h1; inl h2] ++ z)) @
amal_mu_H (x ++ y) z h1 h2) @
ap amal_eta
(word_concat_w_ww x y ([inl (h1 * h2)] ++ z))^)
(fun (yz : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y ([inr k1; inr k2] ++ z)) @
amal_mu_K (x ++ y) z k1 k2) @
ap amal_eta
(word_concat_w_ww x y ([inr (k1 * k2)] ++ z))^)
(fun (yw : Words) (z : G) =>
(ap amal_eta
(word_concat_w_ww x y ([inl (f z)] ++ w)) @
amal_tau (x ++ y) w z) @
ap amal_eta
(word_concat_w_ww x y ([inr (g z)] ++ w))^)
(funyz : Words =>
(ap amal_eta
(word_concat_w_ww x y ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y) z) @
ap amal_eta (word_concat_w_ww x y z)^)
(funyz : Words =>
(ap amal_eta
(word_concat_w_ww x y ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y) z) @
ap amal_eta (word_concat_w_ww x y z)^) r) (x ++ z)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, z: Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, z, w: Words
?Goal0 = ([inl mon_unit] ++ z) ++ w
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, z, w: Words
amal_eta (x ++ ?Goal0) = amal_eta (x ++ z ++ w)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, z, w: Words
amal_eta (x ++ [inl mon_unit] ++ z ++ w) =
amal_eta (x ++ z ++ w)
apply amal_omega_H.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words
forall (y : amal_type) (y0 : Words),
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl h1; inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(word_concat_w_ww x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr k1; inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^) y)
(x ++ [inr mon_unit] ++ y0) =
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl h1; inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(word_concat_w_ww x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr k1; inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^) y)
(x ++ y0)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words
forall (y : amal_type) (y0 : Words),
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl h1; inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(word_concat_w_ww x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr k1; inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^) y)
(x ++ [inr mon_unit] ++ y0) =
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl h1; inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(word_concat_w_ww x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr k1; inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta
(word_concat_w_ww x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(word_concat_w_ww x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (word_concat_w_ww x y1 z)^) y)
(x ++ y0)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, z: Words
forallr : amal_type,
(funx : Words =>
amal_type_rec amal_type
(funy : Words => amal_eta (x ++ y))
(fun (yz : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y ([inl h1; inl h2] ++ z)) @
amal_mu_H (x ++ y) z h1 h2) @
ap amal_eta
(word_concat_w_ww x y ([inl (h1 * h2)] ++ z))^)
(fun (yz : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y ([inr k1; inr k2] ++ z)) @
amal_mu_K (x ++ y) z k1 k2) @
ap amal_eta
(word_concat_w_ww x y ([inr (k1 * k2)] ++ z))^)
(fun (yw : Words) (z : G) =>
(ap amal_eta
(word_concat_w_ww x y ([inl (f z)] ++ w)) @
amal_tau (x ++ y) w z) @
ap amal_eta
(word_concat_w_ww x y ([inr (g z)] ++ w))^)
(funyz : Words =>
(ap amal_eta
(word_concat_w_ww x y ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y) z) @
ap amal_eta (word_concat_w_ww x y z)^)
(funyz : Words =>
(ap amal_eta
(word_concat_w_ww x y ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y) z) @
ap amal_eta (word_concat_w_ww x y z)^) r)
(x ++ [inr mon_unit] ++ z) =
(funx : Words =>
amal_type_rec amal_type
(funy : Words => amal_eta (x ++ y))
(fun (yz : Words) (h1h2 : H) =>
(ap amal_eta
(word_concat_w_ww x y ([inl h1; inl h2] ++ z)) @
amal_mu_H (x ++ y) z h1 h2) @
ap amal_eta
(word_concat_w_ww x y ([inl (h1 * h2)] ++ z))^)
(fun (yz : Words) (k1k2 : K) =>
(ap amal_eta
(word_concat_w_ww x y ([inr k1; inr k2] ++ z)) @
amal_mu_K (x ++ y) z k1 k2) @
ap amal_eta
(word_concat_w_ww x y ([inr (k1 * k2)] ++ z))^)
(fun (yw : Words) (z : G) =>
(ap amal_eta
(word_concat_w_ww x y ([inl (f z)] ++ w)) @
amal_tau (x ++ y) w z) @
ap amal_eta
(word_concat_w_ww x y ([inr (g z)] ++ w))^)
(funyz : Words =>
(ap amal_eta
(word_concat_w_ww x y ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y) z) @
ap amal_eta (word_concat_w_ww x y z)^)
(funyz : Words =>
(ap amal_eta
(word_concat_w_ww x y ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y) z) @
ap amal_eta (word_concat_w_ww x y z)^) r) (x ++ z)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, z: Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
LeftInverse sg_op negate mon_unit
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
LeftInverse sg_op negate mon_unit
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words
- amal_eta x * amal_eta x = mon_unit
apply amal_eta_word_concat_Vw.Defined.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
RightInverse sg_op negate mon_unit
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
RightInverse sg_op negate mon_unit
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words
amal_eta x * - amal_eta x = mon_unit
apply amal_eta_word_concat_wV.Defined.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
Group
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
Group
snrapply (Build_Group amal_type); repeatsplit; exact _.Defined.(** Using foldr. It's important that we use foldr as foldl is near impossible to reason about. *)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
AmalgamatedFreeProduct -> X
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
AmalgamatedFreeProduct -> X
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
Words -> X
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
Words -> X
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g w: Words
X
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g w: Words
H + K -> X -> X
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g w: Words
X
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g w: Words
H + K -> X -> X
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g w: Words l: H x: X
X
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g w: Words r: K x: X
X
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g w: Words l: H x: X
X
exact (h l * x).
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g w: Words r: K x: X
X
exact (k r * x).
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g w: Words
X
exact mon_unit.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
forall (xy : Words) (h1h2 : H),
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inl h1; inl h2] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inl (h1 * h2)] ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
forall (xy : Words) (k1k2 : K),
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inr k1; inr k2] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inr (k1 * k2)] ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
forall (xy : Words) (z : G),
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inl (f z)] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inr (g z)] ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
forallxy : Words,
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inl mon_unit] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
forallxy : Words,
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inr mon_unit] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
forall (xy : Words) (h1h2 : H),
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inl h1; inl h2] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inl (h1 * h2)] ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words h1, h2: H
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit (x ++ [inl h1; inl h2] ++ y) =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit (x ++ [inl (h1 * h2)] ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words h1, h2: H
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y) [inl h1; inl h2]) x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y) [inl (h1 * h2)]) x
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words h1, h2: H
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y) [inl h1; inl h2] =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y) [inl (h1 * h2)]
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words h1, h2: H
h h1 *
(h h2 *
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y) =
h (h1 * h2) *
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words h1, h2: H
h h1 * h h2 *
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y =
h (h1 * h2) *
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words h1, h2: H
h h1 * h h2 = h (h1 * h2)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words h1, h2: H
h (h1 * h2) = h h1 * h h2
exact (grp_homo_op h h1 h2).
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
forall (xy : Words) (k1k2 : K),
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inr k1; inr k2] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inr (k1 * k2)] ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
forall (xy : Words) (z : G),
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inl (f z)] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inr (g z)] ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
forallxy : Words,
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inl mon_unit] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
forallxy : Words,
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inr mon_unit] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
forall (xy : Words) (k1k2 : K),
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inr k1; inr k2] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inr (k1 * k2)] ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words k1, k2: K
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit (x ++ [inr k1; inr k2] ++ y) =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit (x ++ [inr (k1 * k2)] ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words k1, k2: K
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y) [inr k1; inr k2]) x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y) [inr (k1 * k2)]) x
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words k1, k2: K
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y) [inr k1; inr k2] =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y) [inr (k1 * k2)]
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words k1, k2: K
k k1 *
(k k2 *
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y) =
k (k1 * k2) *
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words k1, k2: K
k k1 * k k2 *
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y =
k (k1 * k2) *
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words k1, k2: K
k k1 * k k2 = k (k1 * k2)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words k1, k2: K
k (k1 * k2) = k k1 * k k2
exact (grp_homo_op k k1 k2).
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
forall (xy : Words) (z : G),
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inl (f z)] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inr (g z)] ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
forallxy : Words,
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inl mon_unit] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
forallxy : Words,
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inr mon_unit] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
forall (xy : Words) (z : G),
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inl (f z)] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inr (g z)] ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words z: G
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit (x ++ [inl (f z)] ++ y) =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit (x ++ [inr (g z)] ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words z: G
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y) [inl (f z)]) x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y) [inr (g z)]) x
f_ap; simpl; f_ap.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
forallxy : Words,
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inl mon_unit] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
forallxy : Words,
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inr mon_unit] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
forallxy : Words,
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inl mon_unit] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit (x ++ [inl mon_unit] ++ y) =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y) [inl mon_unit]) x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y) x
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y) [inl mon_unit] =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words
h mon_unit *
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words
mon_unit *
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y
rapply left_identity.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
forallxy : Words,
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inr mon_unit] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
forallxy : Words,
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ [inr mon_unit] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g => (fun (l : H) (x0 : X) => h l * x0) g
| inr g => (fun (r : K) (x0 : X) => k r * x0) g
end) mon_unit w) (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit (x ++ [inr mon_unit] ++ y) =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit (x ++ y)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y) [inr mon_unit]) x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y) x
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y) [inr mon_unit] =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words
k mon_unit *
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g x, y: Words
mon_unit *
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y
rapply left_identity.}Defined.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
IsSemiGroupPreserving
(AmalgamatedFreeProduct_rec' X h k p)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
IsSemiGroupPreserving
(AmalgamatedFreeProduct_rec' X h k p)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g y, x: Words
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit (x ++ y) =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit x *
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g y, x: Words
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y) x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit x *
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit y
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g y, x: Words s:= fold_right
(funX0 : H + K =>
match X0 with
| inl l => funx0 : X => h l * x0
| inr r => funx0 : X => k r * x0
end) mon_unit y: X
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) s x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit x * s
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g y: Words s:= fold_right
(funX0 : H + K =>
match X0 with
| inl l => funx0 : X => h l * x0
| inr r => funx0 : X => k r * x0
end) mon_unit y: X
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) s nil =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit nil * s
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g y: Words a: (H + K)%type x: list (H + K) s:= fold_right
(funX0 : H + K =>
match X0 with
| inl l => funx0 : X => h l * x0
| inr r => funx0 : X => k r * x0
end) mon_unit y: X IHx: fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) s x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit x * s
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) s (a :: x) =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit (a :: x) * s
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g y: Words a: (H + K)%type x: list (H + K) s:= fold_right
(funX0 : H + K =>
match X0 with
| inl l => funx0 : X => h l * x0
| inr r => funx0 : X => k r * x0
end) mon_unit y: X IHx: fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) s x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit x * s
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) s (a :: x) =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit (a :: x) * s
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g y: Words a: (H + K)%type x: list (H + K) s:= fold_right
(funX0 : H + K =>
match X0 with
| inl l => funx0 : X => h l * x0
| inr r => funx0 : X => k r * x0
end) mon_unit y: X IHx: fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) s x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit x * s
match a with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) s x) =
match a with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit x) * s
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g y: Words a: (H + K)%type x: list (H + K) s:= fold_right
(funX0 : H + K =>
match X0 with
| inl l => funx0 : X => h l * x0
| inr r => funx0 : X => k r * x0
end) mon_unit y: X IHx: fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) s x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit x * s
match a with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit x * s) =
match a with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) mon_unit x) * s
destruct a; apply simple_associativity.Qed.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
GroupHomomorphism AmalgamatedFreeProduct X
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
GroupHomomorphism AmalgamatedFreeProduct X
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
AmalgamatedFreeProduct -> X
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
IsSemiGroupPreserving ?f
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: h o f == k o g
IsSemiGroupPreserving
(AmalgamatedFreeProduct_rec' X h k p)
exact _.Defined.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
GroupHomomorphism H AmalgamatedFreeProduct
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
GroupHomomorphism H AmalgamatedFreeProduct
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
H -> AmalgamatedFreeProduct
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
IsSemiGroupPreserving ?f
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
H -> AmalgamatedFreeProduct
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: H
AmalgamatedFreeProduct
exact (amal_eta [inl x]).
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
IsSemiGroupPreserving (funx : H => amal_eta [inl x])
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x, y: H
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group
{h : GroupHomomorphism H X &
{k : GroupHomomorphism K X & h o f == k o g}} <~>
GroupHomomorphism AmalgamatedFreeProduct X
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group
{h : GroupHomomorphism H X &
{k : GroupHomomorphism K X & h o f == k o g}} <~>
GroupHomomorphism AmalgamatedFreeProduct X
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group
{h : GroupHomomorphism H X &
{k : GroupHomomorphism K X & h o f == k o g}} ->
GroupHomomorphism AmalgamatedFreeProduct X
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group
GroupHomomorphism AmalgamatedFreeProduct X ->
{h : GroupHomomorphism H X &
{k : GroupHomomorphism K X & h o f == k o g}}
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group
?f o ?g == idmap
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group
?g o ?f == idmap
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group
GroupHomomorphism AmalgamatedFreeProduct X ->
{h : GroupHomomorphism H X &
{k : GroupHomomorphism K X & h o f == k o g}}
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group
(funX0 : {h : GroupHomomorphism H X &
{k : GroupHomomorphism K X & h o f == k o g}}
=>
(fun (h : GroupHomomorphism H X)
(proj2 : {k : GroupHomomorphism K X &
(funx : G => h (f x)) ==
(funx : G => k (g x))}) =>
(fun (k : GroupHomomorphism K X)
(p : (funx : G => h (f x)) ==
(funx : G => k (g x))) =>
AmalgamatedFreeProduct_rec X h k p) proj2.1 proj2.2)
X0.1 X0.2) o ?g == idmap
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group
?g
o (funX0 : {h : GroupHomomorphism H X &
{k : GroupHomomorphism K X & h o f == k o g}}
=>
(fun (h : GroupHomomorphism H X)
(proj2 : {k : GroupHomomorphism K X &
(funx : G => h (f x)) ==
(funx : G => k (g x))}) =>
(fun (k : GroupHomomorphism K X)
(p : (funx : G => h (f x)) ==
(funx : G => k (g x))) =>
AmalgamatedFreeProduct_rec X h k p) proj2.1
proj2.2) X0.1 X0.2) == idmap
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group
GroupHomomorphism AmalgamatedFreeProduct X ->
{h : GroupHomomorphism H X &
{k : GroupHomomorphism K X & h o f == k o g}}
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: GroupHomomorphism AmalgamatedFreeProduct X
{h : GroupHomomorphism H X &
{k : GroupHomomorphism K X & h o f == k o g}}
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: GroupHomomorphism AmalgamatedFreeProduct X
{k : GroupHomomorphism K X &
(funx : G => grp_homo_compose r amal_inl (f x)) ==
(funx : G => k (g x))}
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: GroupHomomorphism AmalgamatedFreeProduct X
(funx : G => grp_homo_compose r amal_inl (f x)) ==
(funx : G => grp_homo_compose r amal_inr (g x))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: GroupHomomorphism AmalgamatedFreeProduct X x: G
grp_homo_compose r amal_inl (f x) =
grp_homo_compose r amal_inr (g x)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: GroupHomomorphism AmalgamatedFreeProduct X x: G
amal_inl (f x) = amal_inr (g x)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: GroupHomomorphism AmalgamatedFreeProduct X x: G
amal_eta [inl (f x)] = amal_eta [inr (g x)]
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: GroupHomomorphism AmalgamatedFreeProduct X x: G
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group
(funX0 : {h : GroupHomomorphism H X &
{k : GroupHomomorphism K X & h o f == k o g}}
=>
(fun (h : GroupHomomorphism H X)
(proj2 : {k : GroupHomomorphism K X &
(funx : G => h (f x)) ==
(funx : G => k (g x))}) =>
(fun (k : GroupHomomorphism K X)
(p : (funx : G => h (f x)) ==
(funx : G => k (g x))) =>
AmalgamatedFreeProduct_rec X h k p) proj2.1 proj2.2)
X0.1 X0.2)
o (funr : GroupHomomorphism AmalgamatedFreeProduct X
=>
(grp_homo_compose r amal_inl;
grp_homo_compose r amal_inr;
(funx : G =>
ap r
(internal_paths_rew
(funl : list (H + K) =>
amal_eta l = amal_eta [inr (g x)])
(internal_paths_rew
(funl : list (H + K) =>
amal_eta ([inl (f x)] ++ nil) =
amal_eta l) (amal_tau nil nil x)
(word_concat_w_nil [inr (g x)]))
(word_concat_w_nil [inl (f x)])
:
amal_inl (f x) = amal_inr (g x)))
:
(funx : G => grp_homo_compose r amal_inl (f x)) ==
(funx : G => grp_homo_compose r amal_inr (g x)))) ==
idmap
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group
(funr : GroupHomomorphism AmalgamatedFreeProduct X =>
(grp_homo_compose r amal_inl;
grp_homo_compose r amal_inr;
(funx : G =>
ap r
(internal_paths_rew
(funl : list (H + K) =>
amal_eta l = amal_eta [inr (g x)])
(internal_paths_rew
(funl : list (H + K) =>
amal_eta ([inl (f x)] ++ nil) = amal_eta l)
(amal_tau nil nil x)
(word_concat_w_nil [inr (g x)]))
(word_concat_w_nil [inl (f x)])
:
amal_inl (f x) = amal_inr (g x)))
:
(funx : G => grp_homo_compose r amal_inl (f x)) ==
(funx : G => grp_homo_compose r amal_inr (g x))))
o (funX0 : {h : GroupHomomorphism H X &
{k : GroupHomomorphism K X & h o f == k o g}}
=>
(fun (h : GroupHomomorphism H X)
(proj2 : {k : GroupHomomorphism K X &
(funx : G => h (f x)) ==
(funx : G => k (g x))}) =>
(fun (k : GroupHomomorphism K X)
(p : (funx : G => h (f x)) ==
(funx : G => k (g x))) =>
AmalgamatedFreeProduct_rec X h k p) proj2.1
proj2.2) X0.1 X0.2) == idmap
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group
(funX0 : {h : GroupHomomorphism H X &
{k : GroupHomomorphism K X & h o f == k o g}}
=>
(fun (h : GroupHomomorphism H X)
(proj2 : {k : GroupHomomorphism K X &
(funx : G => h (f x)) ==
(funx : G => k (g x))}) =>
(fun (k : GroupHomomorphism K X)
(p : (funx : G => h (f x)) ==
(funx : G => k (g x))) =>
AmalgamatedFreeProduct_rec X h k p) proj2.1 proj2.2)
X0.1 X0.2)
o (funr : GroupHomomorphism AmalgamatedFreeProduct X
=>
(grp_homo_compose r amal_inl;
grp_homo_compose r amal_inr;
(funx : G =>
ap r
(internal_paths_rew
(funl : list (H + K) =>
amal_eta l = amal_eta [inr (g x)])
(internal_paths_rew
(funl : list (H + K) =>
amal_eta ([inl (f x)] ++ nil) =
amal_eta l) (amal_tau nil nil x)
(word_concat_w_nil [inr (g x)]))
(word_concat_w_nil [inl (f x)])
:
amal_inl (f x) = amal_inr (g x)))
:
(funx : G => grp_homo_compose r amal_inl (f x)) ==
(funx : G => grp_homo_compose r amal_inr (g x)))) ==
idmap
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: GroupHomomorphism AmalgamatedFreeProduct X
AmalgamatedFreeProduct_rec X
(grp_homo_compose r amal_inl)
(grp_homo_compose r amal_inr)
(funx : G =>
ap r
(internal_paths_rew
(funl : list (H + K) =>
amal_eta l = amal_eta [inr (g x)])
(internal_paths_rew
(funl : list (H + K) =>
amal_eta ([inl (f x)] ++ nil) = amal_eta l)
(amal_tau nil nil x)
(word_concat_w_nil [inr (g x)]))
(word_concat_w_nil [inl (f x)]))) = r
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: GroupHomomorphism AmalgamatedFreeProduct X
AmalgamatedFreeProduct_rec X
(grp_homo_compose r amal_inl)
(grp_homo_compose r amal_inr)
(funx : G =>
ap r
(internal_paths_rew
(funl : list (H + K) =>
amal_eta l = amal_eta [inr (g x)])
(internal_paths_rew
(funl : list (H + K) =>
amal_eta ([inl (f x)] ++ nil) = amal_eta l)
(amal_tau nil nil x)
(word_concat_w_nil [inr (g x)]))
(word_concat_w_nil [inl (f x)]))) == r
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: GroupHomomorphism AmalgamatedFreeProduct X
forallw : Words,
(funx : amal_type =>
AmalgamatedFreeProduct_rec X
(grp_homo_compose r amal_inl)
(grp_homo_compose r amal_inr)
(funx0 : G =>
ap r
(internal_paths_rew
(funl : list (H + K) =>
amal_eta l = amal_eta [inr (g x0)])
(internal_paths_rew
(funl : list (H + K) =>
amal_eta ([inl (f x0)] ++ nil) =
amal_eta l) (amal_tau nil nil x0)
(word_concat_w_nil [inr (g x0)]))
(word_concat_w_nil [inl (f x0)]))) x = r x)
(amal_eta w)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: GroupHomomorphism AmalgamatedFreeProduct X x: Words
(funx : amal_type =>
AmalgamatedFreeProduct_rec X
(grp_homo_compose r amal_inl)
(grp_homo_compose r amal_inr)
(funx0 : G =>
ap r
(internal_paths_rew
(funl : list (H + K) =>
amal_eta l = amal_eta [inr (g x0)])
(internal_paths_rew
(funl : list (H + K) =>
amal_eta ([inl (f x0)] ++ nil) =
amal_eta l) (amal_tau nil nil x0)
(word_concat_w_nil [inr (g x0)]))
(word_concat_w_nil [inl (f x0)]))) x = r x)
(amal_eta x)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: GroupHomomorphism AmalgamatedFreeProduct X
AmalgamatedFreeProduct_rec X
(grp_homo_compose r amal_inl)
(grp_homo_compose r amal_inr)
(funx : G =>
ap r
(internal_paths_rew
(funl : list (H + K) =>
amal_eta l = amal_eta [inr (g x)])
(internal_paths_rew
(funl : list (H + K) =>
amal_eta ([inl (f x)] ++ nil) = amal_eta l)
(amal_tau nil nil x)
(word_concat_w_nil [inr (g x)]))
(word_concat_w_nil [inl (f x)])))
(amal_eta nil) = r (amal_eta nil)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: GroupHomomorphism AmalgamatedFreeProduct X a: (H + K)%type x: list (H + K) IHx: AmalgamatedFreeProduct_rec X (grp_homo_compose r amal_inl)
(grp_homo_compose r amal_inr)
(funx : G =>
ap r
(internal_paths_rew
(funl : list (H + K) => amal_eta l = amal_eta [inr (g x)])
(internal_paths_rew
(funl : list (H + K) =>
amal_eta ([inl (f x)] ++ nil) = amal_eta l) (amal_tau nil nil x)
(word_concat_w_nil [inr (g x)])) (word_concat_w_nil [inl (f x)])))
(amal_eta x) = r (amal_eta x)
AmalgamatedFreeProduct_rec X
(grp_homo_compose r amal_inl)
(grp_homo_compose r amal_inr)
(funx : G =>
ap r
(internal_paths_rew
(funl : list (H + K) =>
amal_eta l = amal_eta [inr (g x)])
(internal_paths_rew
(funl : list (H + K) =>
amal_eta ([inl (f x)] ++ nil) = amal_eta l)
(amal_tau nil nil x)
(word_concat_w_nil [inr (g x)]))
(word_concat_w_nil [inl (f x)])))
(amal_eta (a :: x)) = r (amal_eta (a :: x))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: GroupHomomorphism AmalgamatedFreeProduct X a: (H + K)%type x: list (H + K) IHx: AmalgamatedFreeProduct_rec X (grp_homo_compose r amal_inl)
(grp_homo_compose r amal_inr)
(funx : G =>
ap r
(internal_paths_rew
(funl : list (H + K) => amal_eta l = amal_eta [inr (g x)])
(internal_paths_rew
(funl : list (H + K) =>
amal_eta ([inl (f x)] ++ nil) = amal_eta l) (amal_tau nil nil x)
(word_concat_w_nil [inr (g x)])) (word_concat_w_nil [inl (f x)])))
(amal_eta x) = r (amal_eta x)
AmalgamatedFreeProduct_rec X
(grp_homo_compose r amal_inl)
(grp_homo_compose r amal_inr)
(funx : G =>
ap r
(internal_paths_rew
(funl : list (H + K) =>
amal_eta l = amal_eta [inr (g x)])
(internal_paths_rew
(funl : list (H + K) =>
amal_eta ([inl (f x)] ++ nil) = amal_eta l)
(amal_tau nil nil x)
(word_concat_w_nil [inr (g x)]))
(word_concat_w_nil [inl (f x)])))
(amal_eta (a :: x)) = r (amal_eta (a :: x))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: GroupHomomorphism AmalgamatedFreeProduct X a: (H + K)%type x: list (H + K) IHx: fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => r (amal_eta [inl g]) * x
| inr g => funx : X => r (amal_eta [inr g]) * x
end) mon_unit x = r (amal_eta x)
match a with
| inl g => funx : X => r (amal_eta [inl g]) * x
| inr g => funx : X => r (amal_eta [inr g]) * x
end
(fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => r (amal_eta [inl g]) * x
| inr g => funx : X => r (amal_eta [inr g]) * x
end) mon_unit x) = r (amal_eta (a :: x))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: GroupHomomorphism AmalgamatedFreeProduct X a: (H + K)%type x: list (H + K) IHx: fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => r (amal_eta [inl g]) * x
| inr g => funx : X => r (amal_eta [inr g]) * x
end) mon_unit x = r (amal_eta x)
match a with
| inl g => funx : X => r (amal_eta [inl g]) * x
| inr g => funx : X => r (amal_eta [inr g]) * x
end (r (amal_eta x)) = r (amal_eta (a :: x))
destruct a; symmetry;
rapply (grp_homo_op r (amal_eta [_]) (amal_eta x)).
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group
(funr : GroupHomomorphism AmalgamatedFreeProduct X =>
(grp_homo_compose r amal_inl;
grp_homo_compose r amal_inr;
(funx : G =>
ap r
(internal_paths_rew
(funl : list (H + K) =>
amal_eta l = amal_eta [inr (g x)])
(internal_paths_rew
(funl : list (H + K) =>
amal_eta ([inl (f x)] ++ nil) = amal_eta l)
(amal_tau nil nil x)
(word_concat_w_nil [inr (g x)]))
(word_concat_w_nil [inl (f x)])
:
amal_inl (f x) = amal_inr (g x)))
:
(funx : G => grp_homo_compose r amal_inl (f x)) ==
(funx : G => grp_homo_compose r amal_inr (g x))))
o (funX0 : {h : GroupHomomorphism H X &
{k : GroupHomomorphism K X & h o f == k o g}}
=>
(fun (h : GroupHomomorphism H X)
(proj2 : {k : GroupHomomorphism K X &
(funx : G => h (f x)) ==
(funx : G => k (g x))}) =>
(fun (k : GroupHomomorphism K X)
(p : (funx : G => h (f x)) ==
(funx : G => k (g x))) =>
AmalgamatedFreeProduct_rec X h k p) proj2.1
proj2.2) X0.1 X0.2) == idmap
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group hkp: {h : GroupHomomorphism H X &
{k : GroupHomomorphism K X &
(funx : G => h (f x)) == (funx : G => k (g x))}}
(grp_homo_compose
(AmalgamatedFreeProduct_rec X hkp.1 (hkp.2).1
(hkp.2).2) amal_inl;
grp_homo_compose
(AmalgamatedFreeProduct_rec X hkp.1 (hkp.2).1
(hkp.2).2) amal_inr;
funx : G =>
ap
(AmalgamatedFreeProduct_rec X hkp.1 (hkp.2).1
(hkp.2).2)
(internal_paths_rew
(funl : list (H + K) =>
amal_eta l = amal_eta [inr (g x)])
(internal_paths_rew
(funl : list (H + K) =>
amal_eta ([inl (f x)] ++ nil) = amal_eta l)
(amal_tau nil nil x)
(word_concat_w_nil [inr (g x)]))
(word_concat_w_nil [inl (f x)]))) = hkp
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group hkp: {h : GroupHomomorphism H X &
{k : GroupHomomorphism K X &
(funx : G => h (f x)) == (funx : G => k (g x))}}
(grp_homo_compose
(AmalgamatedFreeProduct_rec X hkp.1 (hkp.2).1
(hkp.2).2) amal_inl;
grp_homo_compose
(AmalgamatedFreeProduct_rec X hkp.1 (hkp.2).1
(hkp.2).2) amal_inr;
funx : G =>
ap
(AmalgamatedFreeProduct_rec' X hkp.1 (hkp.2).1
(hkp.2).2) (amal_tau nil nil x)) = hkp
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group hkp: {h : GroupHomomorphism H X &
{k : GroupHomomorphism K X &
(funx : G => h (f x)) == (funx : G => k (g x))}}
equiv_sigma_prod
(funhk : GroupHomomorphism H X *
GroupHomomorphism K X =>
(funx : G => fst hk (f x)) ==
(funx : G => snd hk (g x)))
(grp_homo_compose
(AmalgamatedFreeProduct_rec X hkp.1 (hkp.2).1
(hkp.2).2) amal_inl;
grp_homo_compose
(AmalgamatedFreeProduct_rec X hkp.1 (hkp.2).1
(hkp.2).2) amal_inr;
funx : G =>
ap
(AmalgamatedFreeProduct_rec' X hkp.1 (hkp.2).1
(hkp.2).2) (amal_tau nil nil x)) =
equiv_sigma_prod
(funhk : GroupHomomorphism H X *
GroupHomomorphism K X =>
(funx : G => fst hk (f x)) ==
(funx : G => snd hk (g x))) hkp
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group hkp: {h : GroupHomomorphism H X &
{k : GroupHomomorphism K X &
(funx : G => h (f x)) == (funx : G => k (g x))}}
(equiv_sigma_prod
(funhk : GroupHomomorphism H X *
GroupHomomorphism K X =>
(funx : G => fst hk (f x)) ==
(funx : G => snd hk (g x)))
(grp_homo_compose
(AmalgamatedFreeProduct_rec X hkp.1 (hkp.2).1
(hkp.2).2) amal_inl;
grp_homo_compose
(AmalgamatedFreeProduct_rec X hkp.1 (hkp.2).1
(hkp.2).2) amal_inr;
funx : G =>
ap
(AmalgamatedFreeProduct_rec' X hkp.1 (hkp.2).1
(hkp.2).2) (amal_tau nil nil x))).1 =
(equiv_sigma_prod
(funhk : GroupHomomorphism H X *
GroupHomomorphism K X =>
(funx : G => fst hk (f x)) ==
(funx : G => snd hk (g x))) hkp).1
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group h: GroupHomomorphism H X k: GroupHomomorphism K X p: (funx : G => h (f x)) == (funx : G => k (g x))
(equiv_sigma_prod
(funhk : GroupHomomorphism H X *
GroupHomomorphism K X =>
(funx : G => fst hk (f x)) ==
(funx : G => snd hk (g x)))
(grp_homo_compose
(AmalgamatedFreeProduct_rec X h k p) amal_inl;
grp_homo_compose
(AmalgamatedFreeProduct_rec X h k p) amal_inr;
funx : G =>
ap (AmalgamatedFreeProduct_rec' X h k p)
(amal_tau nil nil x))).1 =
(equiv_sigma_prod
(funhk : GroupHomomorphism H X *
GroupHomomorphism K X =>
(funx : G => fst hk (f x)) ==
(funx : G => snd hk (g x))) (h; k; p)).1
apply path_prod; cbn;
apply equiv_path_grouphomomorphism;
intro; simpl; rapply right_identity.Defined.EndFreeProduct.Arguments amal_eta {G H K f g} x.DefinitionFreeProduct (GH : Group) : Group
:= AmalgamatedFreeProduct grp_trivial G H (grp_trivial_rec _) (grp_trivial_rec _).Definitionfreeproduct_inl {GH : Group} : GroupHomomorphism G (FreeProduct G H)
:= amal_inl _ _ _ _ _.Definitionfreeproduct_inr {GH : Group} : GroupHomomorphism H (FreeProduct G H)
:= amal_inr _ _ _ _ _.
G, H, K: Group f: GroupHomomorphism G K g: GroupHomomorphism H K
GroupHomomorphism (FreeProduct G H) K
G, H, K: Group f: GroupHomomorphism G K g: GroupHomomorphism H K
GroupHomomorphism (FreeProduct G H) K
G, H, K: Group f: GroupHomomorphism G K g: GroupHomomorphism H K
f o grp_trivial_rec G == g o grp_trivial_rec H
G, H, K: Group f: GroupHomomorphism G K g: GroupHomomorphism H K
f (grp_trivial_rec G tt) = g (grp_trivial_rec H tt)
GroupHomomorphism G K * GroupHomomorphism H K <~>
GroupHomomorphism (FreeProduct G H) K
funext: Funext G, H, K: Group
GroupHomomorphism G K * GroupHomomorphism H K <~>
GroupHomomorphism (FreeProduct G H) K
funext: Funext G, H, K: Group
{h : GroupHomomorphism G K &
{k : GroupHomomorphism H K &
(funx : grp_trivial => h (grp_trivial_rec G x)) ==
(funx : grp_trivial => k (grp_trivial_rec H x))}} <~>
GroupHomomorphism G K * GroupHomomorphism H K
funext: Funext G, H, K: Group y: GroupHomomorphism G K
foralla : GroupHomomorphism H K,
Contr
((funx : grp_trivial => y (grp_trivial_rec G x)) ==
(funx : grp_trivial => a (grp_trivial_rec H x)))
funext: Funext G, H, K: Group y: GroupHomomorphism G K f: GroupHomomorphism H K
Contr
((funx : grp_trivial => y (grp_trivial_rec G x)) ==
(funx : grp_trivial => f (grp_trivial_rec H x)))
funext: Funext G, H, K: Group y: GroupHomomorphism G K f: GroupHomomorphism H K
foralla : grp_trivial,
Contr
(y (grp_trivial_rec G a) = f (grp_trivial_rec H a))
funext: Funext G, H, K: Group y: GroupHomomorphism G K f: GroupHomomorphism H K
merely
(y (grp_trivial_rec G tt) = f (grp_trivial_rec H tt))
funext: Funext G, H, K: Group y: GroupHomomorphism G K f: GroupHomomorphism H K
y (grp_trivial_rec G tt) = f (grp_trivial_rec H tt)
refine (grp_homo_unit _ @ (grp_homo_unit _)^).Defined.(** The freeproduct is the coproduct in the category of groups. *)
forall (z : Group) (f : G $-> z) (g : H $-> z),
?cat_coprod_rec z f g $o ?cat_inl $== f
G, H: Group
forall (z : Group) (f : G $-> z) (g : H $-> z),
?cat_coprod_rec z f g $o ?cat_inr $== g
G, H: Group
forall (z : Group) (fg : ?cat_coprod $-> z),
f $o ?cat_inl $== g $o ?cat_inl ->
f $o ?cat_inr $== g $o ?cat_inr -> f $== g
G, H: Group
Group
exact (FreeProduct G H).
G, H: Group
G $-> FreeProduct G H
exact freeproduct_inl.
G, H: Group
H $-> FreeProduct G H
exact freeproduct_inr.
G, H: Group
forallz : Group,
(G $-> z) -> (H $-> z) -> FreeProduct G H $-> z
exact (FreeProduct_rec G H).
G, H: Group
forall (z : Group) (f : G $-> z) (g : H $-> z),
FreeProduct_rec G H z f g $o freeproduct_inl $== f
G, H, Z: Group f: G $-> Z g: H $-> Z x: G
f x * mon_unit = f x
rapply right_identity.
G, H: Group
forall (z : Group) (f : G $-> z) (g : H $-> z),
FreeProduct_rec G H z f g $o freeproduct_inr $== g
G, H, Z: Group f: G $-> Z g: H $-> Z x: H
g x * mon_unit = g x
rapply right_identity.
G, H: Group
forall (z : Group) (fg : FreeProduct G H $-> z),
f $o freeproduct_inl $== g $o freeproduct_inl ->
f $o freeproduct_inr $== g $o freeproduct_inr ->
f $== g
G, H, Z: Group f, g: FreeProduct G H $-> Z p: f $o freeproduct_inl $== g $o freeproduct_inl q: f $o freeproduct_inr $== g $o freeproduct_inr
f $== g
G, H, Z: Group f, g: FreeProduct G H $-> Z p: f $o freeproduct_inl $== g $o freeproduct_inl q: f $o freeproduct_inr $== g $o freeproduct_inr
forallw : Words G H, f (amal_eta w) = g (amal_eta w)
G, H, Z: Group f, g: FreeProduct G H $-> Z p: f $o freeproduct_inl $== g $o freeproduct_inl q: f $o freeproduct_inr $== g $o freeproduct_inr w: Words G H
f (amal_eta w) = g (amal_eta w)
G, H, Z: Group f, g: FreeProduct G H $-> Z p: f $o freeproduct_inl $== g $o freeproduct_inl q: f $o freeproduct_inr $== g $o freeproduct_inr
f (amal_eta nil) = g (amal_eta nil)
G, H, Z: Group f, g: FreeProduct G H $-> Z p: f $o freeproduct_inl $== g $o freeproduct_inl q: f $o freeproduct_inr $== g $o freeproduct_inr gh: (G + H)%type w: list (G + H) IHw: f (amal_eta w) = g (amal_eta w)
f (amal_eta (gh :: w)) = g (amal_eta (gh :: w))
G, H, Z: Group f, g: FreeProduct G H $-> Z p: f $o freeproduct_inl $== g $o freeproduct_inl q: f $o freeproduct_inr $== g $o freeproduct_inr gh: (G + H)%type w: list (G + H) IHw: f (amal_eta w) = g (amal_eta w)
f (amal_eta (gh :: w)) = g (amal_eta (gh :: w))
G, H, Z: Group f, g: FreeProduct G H $-> Z p: f $o freeproduct_inl $== g $o freeproduct_inl q: f $o freeproduct_inr $== g $o freeproduct_inr gh: (G + H)%type w: list (G + H) IHw: f (amal_eta w) = g (amal_eta w)
f (amal_eta (gh :: w)) = g (amal_eta (gh :: w))
G, H, Z: Group f, g: FreeProduct G H $-> Z p: f $o freeproduct_inl $== g $o freeproduct_inl q: f $o freeproduct_inr $== g $o freeproduct_inr gh: (G + H)%type w: list (G + H) IHw: f (amal_eta w) = g (amal_eta w)
f (amal_eta [gh] * amal_eta w) =
g (amal_eta [gh] * amal_eta w)
G, H, Z: Group f, g: FreeProduct G H $-> Z p: f $o freeproduct_inl $== g $o freeproduct_inl q: f $o freeproduct_inr $== g $o freeproduct_inr gh: (G + H)%type w: list (G + H) IHw: f (amal_eta w) = g (amal_eta w)
f (amal_eta [gh]) * f (amal_eta w) =
g (amal_eta [gh]) * g (amal_eta w)
G, H, Z: Group f, g: FreeProduct G H $-> Z p: f $o freeproduct_inl $== g $o freeproduct_inl q: f $o freeproduct_inr $== g $o freeproduct_inr gh: (G + H)%type
f (amal_eta [gh]) = g (amal_eta [gh])
G, H, Z: Group f, g: FreeProduct G H $-> Z p: f $o freeproduct_inl $== g $o freeproduct_inl q: f $o freeproduct_inr $== g $o freeproduct_inr g': G
f (amal_eta [inl g']) = g (amal_eta [inl g'])
G, H, Z: Group f, g: FreeProduct G H $-> Z p: f $o freeproduct_inl $== g $o freeproduct_inl q: f $o freeproduct_inr $== g $o freeproduct_inr h: H
f (amal_eta [inr h]) = g (amal_eta [inr h])
G, H, Z: Group f, g: FreeProduct G H $-> Z p: f $o freeproduct_inl $== g $o freeproduct_inl q: f $o freeproduct_inr $== g $o freeproduct_inr g': G
f (amal_eta [inl g']) = g (amal_eta [inl g'])
exact (p g').
G, H, Z: Group f, g: FreeProduct G H $-> Z p: f $o freeproduct_inl $== g $o freeproduct_inl q: f $o freeproduct_inr $== g $o freeproduct_inr h: H