Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.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 WildCat.Core WildCat.Coproducts.Require Import Cubical.DPath.Require Import Spaces.List.Core Spaces.List.Theory.Require Import Colimits.Pushout.Require Import Truncations.Core Truncations.SeparatedTrunc.Require Import Algebra.Groups.Group.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 successively out of coequalizers. *)(** We will call M [amal_type] and prefix all the constructors with [amal_] (for amalgamated free product). *)SectionAmalgamatedFreeProduct.Context {GHK : Group}
(f : GroupHomomorphism G H) (g : GroupHomomorphism G K).Local DefinitionWords : Type := list (H + K).
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 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; rhs napply app_assoc; 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 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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 1] ++ y)) (e (x ++ y)) ok: forallxy : Words,
DPath P (amal_omega_K x y)
(e (x ++ [inr 1] ++ 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)
forallx : amal_type, IsHSet (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 1] ++ 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 1] ++ 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)
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 1] ++ 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 1] ++ 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 1] ++ 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 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ y) = e (x ++ y)
forallxy : Words,
DPath (fun_ : amal_type => P)
(amal_omega_H x y) (e (x ++ [inl 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ y) = e (x ++ y)
forallxy : Words,
DPath (fun_ : amal_type => P)
(amal_omega_K x y) (e (x ++ [inr 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ y) = e (x ++ y) x, y: Words
e (x ++ [inl 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ y) = e (x ++ y) x, y: Words
e (x ++ [inr 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ y) = e (x ++ y) x, y: Words
e (x ++ [inl 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ y) = e (x ++ y) x, y: Words
e (x ++ [inr 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ y) = e (x ++ y) x, y: Words
e (x ++ [inl 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ y) = e (x ++ y) x, y: Words
e (x ++ [inr 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ y) = e (x ++ y) x, y: Words
e (x ++ [inl 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ y) = e (x ++ y) x, y: Words
e (x ++ [inr 1] ++ 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 1] ++ y) = e (x ++ y) ok: forallxy : Words,
e (x ++ [inr 1] ++ y) = e (x ++ y) x, y: Words
e (x ++ [inr 1] ++ y) = e (x ++ y)
apply ok.Defined.(** Now for the group structure *)(** We will frequently need to use that path types in [amal_type] are hprops, and so it speeds things up to create this instance. It is fast to use [_] here, but when the terms are large below, it becomes slower. *)Local Instanceishprop_paths_amal_type (xy : amal_type) : IsHProp (x = y) := _.(** 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
(app_assoc x y1 ([inl h1, inl h2] ++ z0)) @
amal_mu_H (x ++ y1) z0 h1 h2) @
ap amal_eta
(app_assoc x y1 ([inl (h1 * h2)] ++ z0))^)
(fun (y1z0 : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y1 ([inr k1, inr k2] ++ z0)) @
amal_mu_K (x ++ y1) z0 k1 k2) @
ap amal_eta
(app_assoc x y1 ([inr (k1 * k2)] ++ z0))^)
(fun (y1w : Words) (z0 : G) =>
(ap amal_eta (app_assoc x y1 ([inl (f z0)] ++ w)) @
amal_tau (x ++ y1) w z0) @
ap amal_eta (app_assoc x y1 ([inr (g z0)] ++ w))^)
(funy1z0 : Words =>
(ap amal_eta
(app_assoc x y1 ([inl mon_unit] ++ z0)) @
amal_omega_H (x ++ y1) z0) @
ap amal_eta (app_assoc x y1 z0)^)
(funy1z0 : Words =>
(ap amal_eta
(app_assoc x y1 ([inr mon_unit] ++ z0)) @
amal_omega_K (x ++ y1) z0) @
ap amal_eta (app_assoc 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
(app_assoc x y1 ([inl h1, inl h2] ++ z0)) @
amal_mu_H (x ++ y1) z0 h1 h2) @
ap amal_eta
(app_assoc x y1 ([inl (h1 * h2)] ++ z0))^)
(fun (y1z0 : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y1 ([inr k1, inr k2] ++ z0)) @
amal_mu_K (x ++ y1) z0 k1 k2) @
ap amal_eta
(app_assoc x y1 ([inr (k1 * k2)] ++ z0))^)
(fun (y1w : Words) (z0 : G) =>
(ap amal_eta (app_assoc x y1 ([inl (f z0)] ++ w)) @
amal_tau (x ++ y1) w z0) @
ap amal_eta (app_assoc x y1 ([inr (g z0)] ++ w))^)
(funy1z0 : Words =>
(ap amal_eta
(app_assoc x y1 ([inl mon_unit] ++ z0)) @
amal_omega_H (x ++ y1) z0) @
ap amal_eta (app_assoc x y1 z0)^)
(funy1z0 : Words =>
(ap amal_eta
(app_assoc x y1 ([inr mon_unit] ++ z0)) @
amal_omega_K (x ++ y1) z0) @
ap amal_eta (app_assoc 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
(app_assoc x y1 ([inl h1, inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(app_assoc x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y1 ([inr k1, inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(app_assoc x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta (app_assoc x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta (app_assoc x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^) y)
(x ++ [inl 1] ++ y0) =
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(app_assoc x y1 ([inl h1, inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(app_assoc x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y1 ([inr k1, inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(app_assoc x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta (app_assoc x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta (app_assoc x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (app_assoc 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
(app_assoc x y1 ([inl h1, inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(app_assoc x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y1 ([inr k1, inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(app_assoc x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta (app_assoc x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta (app_assoc x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^) y)
(x ++ [inr 1] ++ y0) =
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(app_assoc x y1 ([inl h1, inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(app_assoc x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y1 ([inr k1, inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(app_assoc x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta (app_assoc x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta (app_assoc x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (app_assoc 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
(app_assoc x y1 ([inl h1, inl h2] ++ z0)) @
amal_mu_H (x ++ y1) z0 h1 h2) @
ap amal_eta
(app_assoc x y1 ([inl (h1 * h2)] ++ z0))^)
(fun (y1z0 : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y1 ([inr k1, inr k2] ++ z0)) @
amal_mu_K (x ++ y1) z0 k1 k2) @
ap amal_eta
(app_assoc x y1 ([inr (k1 * k2)] ++ z0))^)
(fun (y1w : Words) (z0 : G) =>
(ap amal_eta (app_assoc x y1 ([inl (f z0)] ++ w)) @
amal_tau (x ++ y1) w z0) @
ap amal_eta (app_assoc x y1 ([inr (g z0)] ++ w))^)
(funy1z0 : Words =>
(ap amal_eta
(app_assoc x y1 ([inl mon_unit] ++ z0)) @
amal_omega_H (x ++ y1) z0) @
ap amal_eta (app_assoc x y1 z0)^)
(funy1z0 : Words =>
(ap amal_eta
(app_assoc x y1 ([inr mon_unit] ++ z0)) @
amal_omega_K (x ++ y1) z0) @
ap amal_eta (app_assoc 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
(app_assoc x y1 ([inl h1, inl h2] ++ z0)) @
amal_mu_H (x ++ y1) z0 h1 h2) @
ap amal_eta
(app_assoc x y1 ([inl (h1 * h2)] ++ z0))^)
(fun (y1z0 : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y1 ([inr k1, inr k2] ++ z0)) @
amal_mu_K (x ++ y1) z0 k1 k2) @
ap amal_eta
(app_assoc x y1 ([inr (k1 * k2)] ++ z0))^)
(fun (y1w : Words) (z0 : G) =>
(ap amal_eta (app_assoc x y1 ([inl (f z0)] ++ w)) @
amal_tau (x ++ y1) w z0) @
ap amal_eta (app_assoc x y1 ([inr (g z0)] ++ w))^)
(funy1z0 : Words =>
(ap amal_eta
(app_assoc x y1 ([inl mon_unit] ++ z0)) @
amal_omega_H (x ++ y1) z0) @
ap amal_eta (app_assoc x y1 z0)^)
(funy1z0 : Words =>
(ap amal_eta
(app_assoc x y1 ([inr mon_unit] ++ z0)) @
amal_omega_K (x ++ y1) z0) @
ap amal_eta (app_assoc 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
(app_assoc x y ([inl h1, inl h2] ++ z)) @
amal_mu_H (x ++ y) z h1 h2) @
ap amal_eta
(app_assoc x y ([inl (h1 * h2)] ++ z))^)
(fun (yz : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y ([inr k1, inr k2] ++ z)) @
amal_mu_K (x ++ y) z k1 k2) @
ap amal_eta
(app_assoc x y ([inr (k1 * k2)] ++ z))^)
(fun (yw : Words) (z : G) =>
(ap amal_eta (app_assoc x y ([inl (f z)] ++ w)) @
amal_tau (x ++ y) w z) @
ap amal_eta (app_assoc x y ([inr (g z)] ++ w))^)
(funyz : Words =>
(ap amal_eta (app_assoc x y ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y) z) @
ap amal_eta (app_assoc x y z)^)
(funyz : Words =>
(ap amal_eta (app_assoc x y ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y) z) @
ap amal_eta (app_assoc 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
(app_assoc x y ([inl h1, inl h2] ++ z)) @
amal_mu_H (x ++ y) z h1 h2) @
ap amal_eta
(app_assoc x y ([inl (h1 * h2)] ++ z))^)
(fun (yz : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y ([inr k1, inr k2] ++ z)) @
amal_mu_K (x ++ y) z k1 k2) @
ap amal_eta
(app_assoc x y ([inr (k1 * k2)] ++ z))^)
(fun (yw : Words) (z : G) =>
(ap amal_eta (app_assoc x y ([inl (f z)] ++ w)) @
amal_tau (x ++ y) w z) @
ap amal_eta (app_assoc x y ([inr (g z)] ++ w))^)
(funyz : Words =>
(ap amal_eta (app_assoc x y ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y) z) @
ap amal_eta (app_assoc x y z)^)
(funyz : Words =>
(ap amal_eta (app_assoc x y ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y) z) @
ap amal_eta (app_assoc 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
(app_assoc x y1 ([inl h1, inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(app_assoc x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y1 ([inr k1, inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(app_assoc x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta (app_assoc x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta (app_assoc x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^) y)
(x ++ [inl 1] ++ y0) =
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(app_assoc x y1 ([inl h1, inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(app_assoc x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y1 ([inr k1, inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(app_assoc x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta (app_assoc x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta (app_assoc x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (app_assoc 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
(app_assoc x y1 ([inl h1, inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(app_assoc x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y1 ([inr k1, inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(app_assoc x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta (app_assoc x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta (app_assoc x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^) y)
(x ++ [inr 1] ++ y0) =
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(app_assoc x y1 ([inl h1, inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(app_assoc x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y1 ([inr k1, inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(app_assoc x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta (app_assoc x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta (app_assoc x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (app_assoc 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
(app_assoc x y1 ([inl h1, inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(app_assoc x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y1 ([inr k1, inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(app_assoc x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta (app_assoc x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta (app_assoc x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^) y)
(x ++ [inl 1] ++ y0) =
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(app_assoc x y1 ([inl h1, inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(app_assoc x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y1 ([inr k1, inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(app_assoc x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta (app_assoc x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta (app_assoc x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (app_assoc 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
(app_assoc x y ([inl h1, inl h2] ++ z)) @
amal_mu_H (x ++ y) z h1 h2) @
ap amal_eta
(app_assoc x y ([inl (h1 * h2)] ++ z))^)
(fun (yz : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y ([inr k1, inr k2] ++ z)) @
amal_mu_K (x ++ y) z k1 k2) @
ap amal_eta
(app_assoc x y ([inr (k1 * k2)] ++ z))^)
(fun (yw : Words) (z : G) =>
(ap amal_eta (app_assoc x y ([inl (f z)] ++ w)) @
amal_tau (x ++ y) w z) @
ap amal_eta (app_assoc x y ([inr (g z)] ++ w))^)
(funyz : Words =>
(ap amal_eta (app_assoc x y ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y) z) @
ap amal_eta (app_assoc x y z)^)
(funyz : Words =>
(ap amal_eta (app_assoc x y ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y) z) @
ap amal_eta (app_assoc x y z)^) r)
(x ++ [inl 1] ++ z) =
(funx : Words =>
amal_type_rec amal_type
(funy : Words => amal_eta (x ++ y))
(fun (yz : Words) (h1h2 : H) =>
(ap amal_eta
(app_assoc x y ([inl h1, inl h2] ++ z)) @
amal_mu_H (x ++ y) z h1 h2) @
ap amal_eta
(app_assoc x y ([inl (h1 * h2)] ++ z))^)
(fun (yz : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y ([inr k1, inr k2] ++ z)) @
amal_mu_K (x ++ y) z k1 k2) @
ap amal_eta
(app_assoc x y ([inr (k1 * k2)] ++ z))^)
(fun (yw : Words) (z : G) =>
(ap amal_eta (app_assoc x y ([inl (f z)] ++ w)) @
amal_tau (x ++ y) w z) @
ap amal_eta (app_assoc x y ([inr (g z)] ++ w))^)
(funyz : Words =>
(ap amal_eta (app_assoc x y ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y) z) @
ap amal_eta (app_assoc x y z)^)
(funyz : Words =>
(ap amal_eta (app_assoc x y ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y) z) @
ap amal_eta (app_assoc 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 1] ++ 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 1] ++ 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
(app_assoc x y1 ([inl h1, inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(app_assoc x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y1 ([inr k1, inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(app_assoc x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta (app_assoc x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta (app_assoc x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^) y)
(x ++ [inr 1] ++ y0) =
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(app_assoc x y1 ([inl h1, inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(app_assoc x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y1 ([inr k1, inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(app_assoc x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta (app_assoc x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta (app_assoc x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (app_assoc 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
(app_assoc x y1 ([inl h1, inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(app_assoc x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y1 ([inr k1, inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(app_assoc x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta (app_assoc x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta (app_assoc x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^) y)
(x ++ [inr 1] ++ y0) =
(funx : Words =>
amal_type_rec amal_type
(funy1 : Words => amal_eta (x ++ y1))
(fun (y1z : Words) (h1h2 : H) =>
(ap amal_eta
(app_assoc x y1 ([inl h1, inl h2] ++ z)) @
amal_mu_H (x ++ y1) z h1 h2) @
ap amal_eta
(app_assoc x y1 ([inl (h1 * h2)] ++ z))^)
(fun (y1z : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y1 ([inr k1, inr k2] ++ z)) @
amal_mu_K (x ++ y1) z k1 k2) @
ap amal_eta
(app_assoc x y1 ([inr (k1 * k2)] ++ z))^)
(fun (y1w : Words) (z : G) =>
(ap amal_eta (app_assoc x y1 ([inl (f z)] ++ w)) @
amal_tau (x ++ y1) w z) @
ap amal_eta (app_assoc x y1 ([inr (g z)] ++ w))^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y1) z) @
ap amal_eta (app_assoc x y1 z)^)
(funy1z : Words =>
(ap amal_eta
(app_assoc x y1 ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y1) z) @
ap amal_eta (app_assoc 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
(app_assoc x y ([inl h1, inl h2] ++ z)) @
amal_mu_H (x ++ y) z h1 h2) @
ap amal_eta
(app_assoc x y ([inl (h1 * h2)] ++ z))^)
(fun (yz : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y ([inr k1, inr k2] ++ z)) @
amal_mu_K (x ++ y) z k1 k2) @
ap amal_eta
(app_assoc x y ([inr (k1 * k2)] ++ z))^)
(fun (yw : Words) (z : G) =>
(ap amal_eta (app_assoc x y ([inl (f z)] ++ w)) @
amal_tau (x ++ y) w z) @
ap amal_eta (app_assoc x y ([inr (g z)] ++ w))^)
(funyz : Words =>
(ap amal_eta (app_assoc x y ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y) z) @
ap amal_eta (app_assoc x y z)^)
(funyz : Words =>
(ap amal_eta (app_assoc x y ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y) z) @
ap amal_eta (app_assoc x y z)^) r)
(x ++ [inr 1] ++ z) =
(funx : Words =>
amal_type_rec amal_type
(funy : Words => amal_eta (x ++ y))
(fun (yz : Words) (h1h2 : H) =>
(ap amal_eta
(app_assoc x y ([inl h1, inl h2] ++ z)) @
amal_mu_H (x ++ y) z h1 h2) @
ap amal_eta
(app_assoc x y ([inl (h1 * h2)] ++ z))^)
(fun (yz : Words) (k1k2 : K) =>
(ap amal_eta
(app_assoc x y ([inr k1, inr k2] ++ z)) @
amal_mu_K (x ++ y) z k1 k2) @
ap amal_eta
(app_assoc x y ([inr (k1 * k2)] ++ z))^)
(fun (yw : Words) (z : G) =>
(ap amal_eta (app_assoc x y ([inl (f z)] ++ w)) @
amal_tau (x ++ y) w z) @
ap amal_eta (app_assoc x y ([inr (g z)] ++ w))^)
(funyz : Words =>
(ap amal_eta (app_assoc x y ([inl mon_unit] ++ z)) @
amal_omega_H (x ++ y) z) @
ap amal_eta (app_assoc x y z)^)
(funyz : Words =>
(ap amal_eta (app_assoc x y ([inr mon_unit] ++ z)) @
amal_omega_K (x ++ y) z) @
ap amal_eta (app_assoc 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 k: K xs: list (H + K) IHxs: amal_eta (xs ++ word_inverse xs) = 1
amal_eta [inr k] * 1 * amal_eta [inr k^] = 1
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K k: K xs: list (H + K) IHxs: amal_eta (xs ++ word_inverse xs) = 1
amal_eta [inr k] * amal_eta [inr k^] = 1
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K k: K xs: list (H + K) IHxs: amal_eta (xs ++ word_inverse xs) = 1
amal_eta ([inr k] ++ nil) * amal_eta [inr k^] = 1
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K k: K xs: list (H + K) IHxs: amal_eta (xs ++ word_inverse xs) = 1
amal_eta (([inr k] ++ [inr k^]) ++ nil) = 1
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K k: K xs: list (H + K) IHxs: amal_eta (xs ++ word_inverse xs) = 1
amal_eta ([inr k] ++ [inr k^] ++ nil) = 1
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K k: K xs: list (H + K) IHxs: amal_eta (xs ++ word_inverse xs) = 1
amal_eta (nil ++ [inr k] ++ [inr k^] ++ nil) = 1
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K k: K xs: list (H + K) IHxs: amal_eta (xs ++ word_inverse xs) = 1
amal_eta (nil ++ [inr (k * k^)] ++ nil) = 1
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K k: K xs: list (H + K) IHxs: amal_eta (xs ++ word_inverse xs) = 1
amal_eta (nil ++ [inr (k * k^)] ++ nil) = ?Goal
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K k: K xs: list (H + K) IHxs: amal_eta (xs ++ word_inverse xs) = 1
?Goal = 1
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K k: K xs: list (H + K) IHxs: amal_eta (xs ++ word_inverse xs) = 1
amal_eta (nil ++ [inr (k * k^)] ++ nil) = ?Goal
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K k: K xs: list (H + K) IHxs: amal_eta (xs ++ word_inverse xs) = 1
[inr (k * k^)] ++ nil = ?y
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K k: K xs: list (H + K) IHxs: amal_eta (xs ++ word_inverse xs) = 1
[inr (k * k^)] = ?Goal0
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K k: K xs: list (H + K) IHxs: amal_eta (xs ++ word_inverse xs) = 1
inr (k * k^) = ?Goal0
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K k: K xs: list (H + K) IHxs: amal_eta (xs ++ word_inverse xs) = 1
k * k^ = ?y
apply right_inverse.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K k: K xs: list (H + K) IHxs: amal_eta (xs ++ word_inverse xs) = 1
amal_eta (nil ++ [inr 1] ++ nil) = 1
apply amal_omega_K.Defined.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
LeftInverse sg_op inv 1
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
LeftInverse sg_op inv 1
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words
(amal_eta x)^ * amal_eta x = 1
apply amal_eta_word_concat_Vw.Defined.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
RightInverse sg_op inv 1
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
RightInverse sg_op inv 1
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: Words
amal_eta x * (amal_eta x)^ = 1
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
snapply (Build_Group amal_type); repeatsplit; exact _.Defined.EndAmalgamatedFreeProduct.Arguments amal_eta {G H K f g} x.Arguments amal_mu_H {G H K f g} x y.Arguments amal_mu_K {G H K f g} x y.Arguments amal_tau {G H K f g} x y z.Arguments amal_omega_H {G H K f g} x y.Arguments amal_omega_K {G H K f g} x y.SectionRecInd.Context {GHK : Group}
{f : GroupHomomorphism G H} {g : GroupHomomorphism G K}.(** 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 f g -> 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 f g -> 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) 1 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) 1 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) 1 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) 1 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) 1 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) 1 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) 1 w) (x ++ [inl 1] ++ 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) 1 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) 1 w) (x ++ [inr 1] ++ 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) 1 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) 1 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) 1 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) 1 (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) 1 (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) 1 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) 1 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) 1 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) 1 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) 1 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) 1 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) 1 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) 1 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) 1 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) 1 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) 1 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) 1 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) 1 w) (x ++ [inl 1] ++ 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) 1 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) 1 w) (x ++ [inr 1] ++ 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) 1 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) 1 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) 1 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) 1 (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) 1 (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) 1 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) 1 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) 1 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) 1 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) 1 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) 1 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) 1 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) 1 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) 1 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) 1 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) 1 w) (x ++ [inl 1] ++ 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) 1 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) 1 w) (x ++ [inr 1] ++ 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) 1 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) 1 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) 1 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) 1 (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) 1 (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) 1 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) 1 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) 1 w) (x ++ [inl 1] ++ 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) 1 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) 1 w) (x ++ [inr 1] ++ 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) 1 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) 1 w) (x ++ [inl 1] ++ 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) 1 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) 1 (x ++ [inl 1] ++ y) =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) 1 (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) 1 y) [inl 1]) 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) 1 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) 1 y) [inl 1] =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) 1 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 1 *
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) 1 y =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) 1 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
1 *
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) 1 y =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) 1 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) 1 w) (x ++ [inr 1] ++ 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) 1 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) 1 w) (x ++ [inr 1] ++ 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) 1 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) 1 (x ++ [inr 1] ++ y) =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) 1 (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) 1 y) [inr 1]) 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) 1 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) 1 y) [inr 1] =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) 1 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 1 *
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) 1 y =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) 1 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
1 *
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) 1 y =
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) 1 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) 1 (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) 1 x *
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) 1 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) 1 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) 1 x *
fold_right
(funX0 : H + K =>
match X0 with
| inl g => funx : X => h g * x
| inr g => funx : X => k g * x
end) 1 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) 1 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) 1 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) 1 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) 1 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) 1 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) 1 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) 1 (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) 1 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) 1 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) 1 (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) 1 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) 1 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) 1 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) 1 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) 1 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) 1 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) 1 x) * s
destruct a; apply simple_associativity.Qed.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: H $-> X k: K $-> X p: h $o f $== k $o g
AmalgamatedFreeProduct f g $-> X
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: H $-> X k: K $-> X p: h $o f $== k $o g
AmalgamatedFreeProduct f g $-> X
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: H $-> X k: K $-> X p: h $o f $== k $o g
AmalgamatedFreeProduct f g -> X
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: H $-> X k: K $-> X p: h $o f $== k $o g
IsSemiGroupPreserving ?grp_homo_map
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K X: Group h: H $-> X k: 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
H $-> AmalgamatedFreeProduct f g
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
H $-> AmalgamatedFreeProduct f g
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
H -> AmalgamatedFreeProduct f g
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
IsSemiGroupPreserving ?grp_homo_map
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
H -> AmalgamatedFreeProduct f g
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K x: H
AmalgamatedFreeProduct f g
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
amal_inl $o f $== amal_inr $o g
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K
amal_inl $o f $== amal_inr $o g
hnf; apply (amal_tau nil nil).Defined.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group
{h : H $-> X & {k : K $-> X & h $o f $== k $o g}} <~>
(AmalgamatedFreeProduct f g $-> X)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group
{h : H $-> X & {k : K $-> X & h $o f $== k $o g}} <~>
(AmalgamatedFreeProduct f g $-> X)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group
{h : H $-> X & {k : K $-> X & h $o f $== k $o g}} ->
AmalgamatedFreeProduct f g $-> X
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group
(AmalgamatedFreeProduct f g $-> X) ->
{h : H $-> X & {k : 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
(AmalgamatedFreeProduct f g $-> X) ->
{h : H $-> X & {k : 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 : H $-> X &
{k : K $-> X & h $o f $== k $o g}} =>
(fun (h : H $-> X)
(proj2 : {k : K $-> X & h $o f $== k $o g}) =>
(fun (k : K $-> X) (p : h $o f $== k $o g) =>
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 : H $-> X &
{k : K $-> X & h $o f $== k $o g}} =>
(fun (h : H $-> X)
(proj2 : {k : K $-> X & h $o f $== k $o g}) =>
(fun (k : K $-> X) (p : h $o f $== k $o g) =>
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
(AmalgamatedFreeProduct f g $-> X) ->
{h : H $-> X & {k : 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: AmalgamatedFreeProduct f g $-> X
{h : H $-> X & {k : 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: AmalgamatedFreeProduct f g $-> X
{k : K $-> X &
grp_homo_compose r amal_inl $o f $== k $o g}
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: AmalgamatedFreeProduct f g $-> X
grp_homo_compose r amal_inl $o f $==
grp_homo_compose r amal_inr $o g
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: AmalgamatedFreeProduct f g $-> X x: G
(grp_homo_compose r amal_inl $o f) x =
(grp_homo_compose r amal_inr $o g) x
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: AmalgamatedFreeProduct f g $-> 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: AmalgamatedFreeProduct f g $-> 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: AmalgamatedFreeProduct f g $-> X x: G
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group
(funX0 : {h : H $-> X &
{k : K $-> X & h $o f $== k $o g}} =>
(fun (h : H $-> X)
(proj2 : {k : K $-> X & h $o f $== k $o g}) =>
(fun (k : K $-> X) (p : h $o f $== k $o g) =>
AmalgamatedFreeProduct_rec X h k p) proj2.1 proj2.2)
X0.1 X0.2)
o (funr : AmalgamatedFreeProduct f g $-> 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)
(app_nil [inr (g x)]))
(app_nil [inl (f x)])
:
amal_inl (f x) = amal_inr (g x)))
:
grp_homo_compose r amal_inl $o f $==
grp_homo_compose r amal_inr $o g)) == idmap
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group
(funr : AmalgamatedFreeProduct f g $-> 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) (app_nil [inr (g x)]))
(app_nil [inl (f x)])
:
amal_inl (f x) = amal_inr (g x)))
:
grp_homo_compose r amal_inl $o f $==
grp_homo_compose r amal_inr $o g))
o (funX0 : {h : H $-> X &
{k : K $-> X & h $o f $== k $o g}} =>
(fun (h : H $-> X)
(proj2 : {k : K $-> X & h $o f $== k $o g}) =>
(fun (k : K $-> X) (p : h $o f $== k $o g) =>
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 : H $-> X &
{k : K $-> X & h $o f $== k $o g}} =>
(fun (h : H $-> X)
(proj2 : {k : K $-> X & h $o f $== k $o g}) =>
(fun (k : K $-> X) (p : h $o f $== k $o g) =>
AmalgamatedFreeProduct_rec X h k p) proj2.1 proj2.2)
X0.1 X0.2)
o (funr : AmalgamatedFreeProduct f g $-> 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)
(app_nil [inr (g x)]))
(app_nil [inl (f x)])
:
amal_inl (f x) = amal_inr (g x)))
:
grp_homo_compose r amal_inl $o f $==
grp_homo_compose r amal_inr $o g)) == idmap
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: AmalgamatedFreeProduct f g $-> 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) (app_nil [inr (g x)]))
(app_nil [inl (f x)]))) = r
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: AmalgamatedFreeProduct f g $-> 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) (app_nil [inr (g x)]))
(app_nil [inl (f x)]))) == r
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group r: AmalgamatedFreeProduct f g $-> X
forallw : Words,
(funx : amal_type f g =>
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)
(app_nil [inr (g x0)]))
(app_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: AmalgamatedFreeProduct f g $-> X x: Words
(funx : amal_type f g =>
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)
(app_nil [inr (g x0)]))
(app_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: AmalgamatedFreeProduct f g $-> 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) (app_nil [inr (g x)]))
(app_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: AmalgamatedFreeProduct f g $-> 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)
(app_nil [inr (g x)])) (app_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) (app_nil [inr (g x)]))
(app_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: AmalgamatedFreeProduct f g $-> 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)
(app_nil [inr (g x)])) (app_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) (app_nil [inr (g x)]))
(app_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 f g) X a: (H + K)%type x: list (H + K) IHx: fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx : X => r (amal_eta [inl g0]) * x
| inr g0 => funx : X => r (amal_eta [inr g0]) * x
end) 1 x = r (amal_eta x)
match a with
| inl g0 => funx : X => r (amal_eta [inl g0]) * x
| inr g0 => funx : X => r (amal_eta [inr g0]) * x
end
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 =>
funx : X => r (amal_eta [inl g0]) * x
| inr g0 =>
funx : X => r (amal_eta [inr g0]) * x
end) 1 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 f g) X a: (H + K)%type x: list (H + K) IHx: fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx : X => r (amal_eta [inl g0]) * x
| inr g0 => funx : X => r (amal_eta [inr g0]) * x
end) 1 x = r (amal_eta x)
match a with
| inl g0 => funx : X => r (amal_eta [inl g0]) * x
| inr g0 => funx : X => r (amal_eta [inr g0]) * 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 : AmalgamatedFreeProduct f g $-> 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) (app_nil [inr (g x)]))
(app_nil [inl (f x)])
:
amal_inl (f x) = amal_inr (g x)))
:
grp_homo_compose r amal_inl $o f $==
grp_homo_compose r amal_inr $o g))
o (funX0 : {h : H $-> X &
{k : K $-> X & h $o f $== k $o g}} =>
(fun (h : H $-> X)
(proj2 : {k : K $-> X & h $o f $== k $o g}) =>
(fun (k : K $-> X) (p : h $o f $== k $o g) =>
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 : H $-> X & {k : K $-> X & h $o f $== k $o g}}
(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) (app_nil [inr (g x)]))
(app_nil [inl (f x)]))) = hkp
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext X: Group hkp: {h : H $-> X & {k : K $-> X & h $o f $== k $o g}}
(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 : H $-> X & {k : K $-> X & h $o f $== k $o g}}
equiv_sigma_prod
(funhk : (H $-> X) * (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 : (H $-> X) * (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 : H $-> X & {k : K $-> X & h $o f $== k $o g}}
(equiv_sigma_prod
(funhk : (H $-> X) * (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 : (H $-> X) * (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: H $-> X k: K $-> X p: h $o f $== k $o g
(equiv_sigma_prod
(funhk : (H $-> X) * (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 : (H $-> X) * (K $-> X) =>
(funx : G => fst hk (f x)) ==
(funx : G => snd hk (g x))) (h; k; p)).1
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: AmalgamatedFreeProduct f g -> Type H0: forallx : AmalgamatedFreeProduct f g,
IsHProp (P x) l: foralla : H, P (amal_inl a) r: forallb : K, P (amal_inr b) Hop: forallxy : AmalgamatedFreeProduct f g, P x -> P y -> P (x * y)
forallx : AmalgamatedFreeProduct f g, P x
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: AmalgamatedFreeProduct f g -> Type H0: forallx : AmalgamatedFreeProduct f g,
IsHProp (P x) l: foralla : H, P (amal_inl a) r: forallb : K, P (amal_inr b) Hop: forallxy : AmalgamatedFreeProduct f g, P x -> P y -> P (x * y)
forallx : AmalgamatedFreeProduct f g, P x
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: AmalgamatedFreeProduct f g -> Type H0: forallx : AmalgamatedFreeProduct f g,
IsHProp (P x) l: foralla : H, P (amal_inl a) r: forallb : K, P (amal_inr b) Hop: forallxy : AmalgamatedFreeProduct f g, P x -> P y -> P (x * y)
forallw : Words, P (amal_eta w)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: AmalgamatedFreeProduct f g -> Type H0: forallx : AmalgamatedFreeProduct f g,
IsHProp (P x) l: foralla : H, P (amal_inl a) r: forallb : K, P (amal_inr b) Hop: forallxy : AmalgamatedFreeProduct f g, P x -> P y -> P (x * y) w: Words
P (amal_eta w)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: AmalgamatedFreeProduct f g -> Type H0: forallx : AmalgamatedFreeProduct f g,
IsHProp (P x) l: foralla : H, P (amal_inl a) r: forallb : K, P (amal_inr b) Hop: forallxy : AmalgamatedFreeProduct f g, P x -> P y -> P (x * y)
P (amal_eta nil)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: AmalgamatedFreeProduct f g -> Type H0: forallx : AmalgamatedFreeProduct f g,
IsHProp (P x) l: foralla : H, P (amal_inl a) r: forallb : K, P (amal_inr b) Hop: forallxy : AmalgamatedFreeProduct f g, P x -> P y -> P (x * y) w: list (H + K) IH: P (amal_eta w) a: (H + K)%type
P (amal_eta (a :: w))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: AmalgamatedFreeProduct f g -> Type H0: forallx : AmalgamatedFreeProduct f g,
IsHProp (P x) l: foralla : H, P (amal_inl a) r: forallb : K, P (amal_inr b) Hop: forallxy : AmalgamatedFreeProduct f g, P x -> P y -> P (x * y)
P (amal_eta nil)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: AmalgamatedFreeProduct f g -> Type H0: forallx : AmalgamatedFreeProduct f g,
IsHProp (P x) l: foralla : H, P (amal_inl a) r: forallb : K, P (amal_inr b) Hop: forallxy : AmalgamatedFreeProduct f g, P x -> P y -> P (x * y)
P (amal_eta (nil ++ [inl 1] ++ nil))
apply l.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: AmalgamatedFreeProduct f g -> Type H0: forallx : AmalgamatedFreeProduct f g,
IsHProp (P x) l: foralla : H, P (amal_inl a) r: forallb : K, P (amal_inr b) Hop: forallxy : AmalgamatedFreeProduct f g, P x -> P y -> P (x * y) w: list (H + K) IH: P (amal_eta w) a: (H + K)%type
P (amal_eta (a :: w))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: AmalgamatedFreeProduct f g -> Type H0: forallx : AmalgamatedFreeProduct f g,
IsHProp (P x) l: foralla : H, P (amal_inl a) r: forallb : K, P (amal_inr b) Hop: forallxy : AmalgamatedFreeProduct f g, P x -> P y -> P (x * y) w: list (H + K) IH: P (amal_eta w) a: H
P (amal_eta (inl a :: w))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: AmalgamatedFreeProduct f g -> Type H0: forallx : AmalgamatedFreeProduct f g,
IsHProp (P x) l: foralla : H, P (amal_inl a) r: forallb : K, P (amal_inr b) Hop: forallxy : AmalgamatedFreeProduct f g, P x -> P y -> P (x * y) w: list (H + K) IH: P (amal_eta w) b: K
P (amal_eta (inr b :: w))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: AmalgamatedFreeProduct f g -> Type H0: forallx : AmalgamatedFreeProduct f g,
IsHProp (P x) l: foralla : H, P (amal_inl a) r: forallb : K, P (amal_inr b) Hop: forallxy : AmalgamatedFreeProduct f g, P x -> P y -> P (x * y) w: list (H + K) IH: P (amal_eta w) a: H
P (amal_eta (inl a :: w))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: AmalgamatedFreeProduct f g -> Type H0: forallx : AmalgamatedFreeProduct f g,
IsHProp (P x) l: foralla : H, P (amal_inl a) r: forallb : K, P (amal_inr b) Hop: forallxy : AmalgamatedFreeProduct f g, P x -> P y -> P (x * y) w: list (H + K) IH: P (amal_eta w) a: H
P (amal_inl a * amal_eta w)
byapply Hop.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: AmalgamatedFreeProduct f g -> Type H0: forallx : AmalgamatedFreeProduct f g,
IsHProp (P x) l: foralla : H, P (amal_inl a) r: forallb : K, P (amal_inr b) Hop: forallxy : AmalgamatedFreeProduct f g, P x -> P y -> P (x * y) w: list (H + K) IH: P (amal_eta w) b: K
P (amal_eta (inr b :: w))
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: AmalgamatedFreeProduct f g -> Type H0: forallx : AmalgamatedFreeProduct f g,
IsHProp (P x) l: foralla : H, P (amal_inl a) r: forallb : K, P (amal_inr b) Hop: forallxy : AmalgamatedFreeProduct f g, P x -> P y -> P (x * y) w: list (H + K) IH: P (amal_eta w) b: K
P (amal_inr b * amal_eta w)
byapply Hop.Defined.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Group k, k': AmalgamatedFreeProduct f g $-> P l: k $o amal_inl $== k' $o amal_inl r: k $o amal_inr $== k' $o amal_inr
k $== k'
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Group k, k': AmalgamatedFreeProduct f g $-> P l: k $o amal_inl $== k' $o amal_inl r: k $o amal_inr $== k' $o amal_inr
k $== k'
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K P: Group k, k': AmalgamatedFreeProduct f g $-> P l: k $o amal_inl $== k' $o amal_inl r: k $o amal_inr $== k' $o amal_inr
forallxy : AmalgamatedFreeProduct f g,
k x = k' x -> k y = k' y -> k (x * y) = k' (x * y)
intros x y; napply grp_homo_op_agree.Defined.
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext P: Group k, k': AmalgamatedFreeProduct f g $-> P
(k $o amal_inl $== k' $o amal_inl) *
(k $o amal_inr $== k' $o amal_inr) <~> k $== k'
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext P: Group k, k': AmalgamatedFreeProduct f g $-> P
(k $o amal_inl $== k' $o amal_inl) *
(k $o amal_inr $== k' $o amal_inr) <~> k $== k'
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext P: Group k, k': AmalgamatedFreeProduct f g $-> P
(k $o amal_inl $== k' $o amal_inl) *
(k $o amal_inr $== k' $o amal_inr) -> k $== k'
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext P: Group k, k': AmalgamatedFreeProduct f g $-> P
k $== k' ->
(k $o amal_inl $== k' $o amal_inl) *
(k $o amal_inr $== k' $o amal_inr)
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext P: Group k, k': AmalgamatedFreeProduct f g $-> P
(k $o amal_inl $== k' $o amal_inl) *
(k $o amal_inr $== k' $o amal_inr) -> k $== k'
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K H0: Funext P: Group k, k': AmalgamatedFreeProduct f g $-> P
k $== k' ->
(k $o amal_inl $== k' $o amal_inl) *
(k $o amal_inr $== k' $o amal_inr)
intros p; split; exact (p $@R _).Defined.EndRecInd.DefinitionFreeProduct (GH : Group) : Group
:= AmalgamatedFreeProduct (grp_trivial_rec G) (grp_trivial_rec H).Definitionfreeproduct_inl {GH : Group} : GroupHomomorphism G (FreeProduct G H)
:= amal_inl.Definitionfreeproduct_inr {GH : Group} : GroupHomomorphism H (FreeProduct G H)
:= amal_inr.Definitionfreeproduct_ind_hprop {GH} (P : FreeProduct G H -> Type)
`{forallx, IsHProp (P x)}
(l : forallg, P (freeproduct_inl g))
(r : forallh, P (freeproduct_inr h))
(Hop : forallxy, P x -> P y -> P (x * y))
: forallx, P x
:= amalgamatedfreeproduct_ind_hprop P l r Hop.(* The above is slow, ~0.15s. *)Definitionfreeproduct_ind_homotopy {GHK : Group}
{ff' : FreeProduct G H $-> K}
(l : f $o freeproduct_inl $== f' $o freeproduct_inl)
(r : f $o freeproduct_inr $== f' $o freeproduct_inr)
: f $== f'
:= amalgamatedfreeproduct_ind_homotopy l r.Definitionequiv_freeproduct_ind_homotopy {Funext : Funext} {GHK : Group}
(ff' : FreeProduct G H $-> K)
: (f $o freeproduct_inl $== f' $o freeproduct_inl)
* (f $o freeproduct_inr $== f' $o freeproduct_inr)
<~> f $== f'
:= equiv_amalgamatedfreeproduct_ind_homotopy _ _.
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
intros Z; exact FreeProduct_rec.
G, H: Group
forall (z : Group) (f : G $-> z) (g : H $-> z),
(funZ : Group => FreeProduct_rec) z f g $o
freeproduct_inl $== f
intros; apply freeproduct_rec_beta_inl.
G, H: Group
forall (z : Group) (f : G $-> z) (g : H $-> z),
(funZ : Group => FreeProduct_rec) z f g $o
freeproduct_inr $== g
intros; apply freeproduct_rec_beta_inr.
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