Built with Alectryon. 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.
From HoTT Require Import Basics Types.From HoTT Require Import Basics Types.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 xs: list (H + K)
Words
G, H, K: Group f: GroupHomomorphism G H g: GroupHomomorphism G K word_inverse: Words -> Words x: H + 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
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 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 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 xs: list (H + K) y: Words IHxs: word_inverse (xs ++ y) = word_inverse y ++ word_inverse xs
match x with
| inl g0 => word_inverse (xs ++ y) ++ [inl g0^]
| inr g0 => word_inverse (xs ++ y) ++ [inr g0^]
end =
word_inverse y ++
match x with
| inl g0 => word_inverse xs ++ [inl g0^]
| inr g0 => word_inverse xs ++ [inr g0^]
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
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: forallx0 : amal_type, IsHSet (P x0) e: forallw : Words, P (amal_eta w) mh: forall (x0y0 : Words) (h0h3 : H),
DPath P (amal_mu_H x0 y0 h0 h3) (e (x0 ++ [inl h0, inl h3] ++ y0))
(e (x0 ++ [inl (h0 * h3)] ++ y0)) mk: forall (x0y0 : Words) (k1k2 : K),
DPath P (amal_mu_K x0 y0 k1 k2) (e (x0 ++ [inr k1, inr k2] ++ y0))
(e (x0 ++ [inr (k1 * k2)] ++ y0)) t: forall (x0y0 : Words) (z : G),
DPath P (amal_tau x0 y0 z) (e (x0 ++ [inl (f z)] ++ y0))
(e (x0 ++ [inr (g z)] ++ y0)) oh: forallx0y0 : Words,
DPath P (amal_omega_H x0 y0) (e (x0 ++ [inl 1] ++ y0)) (e (x0 ++ y0)) ok: forallx0y0 : Words,
DPath P (amal_omega_K x0 y0) (e (x0 ++ [inr 1] ++ y0)) (e (x0 ++ y0)) 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: forallx0 : amal_type, IsHSet (P x0) e: forallw : Words, P (amal_eta w) mh: forall (x0y0 : Words) (h0h3 : H),
DPath P (amal_mu_H x0 y0 h0 h3) (e (x0 ++ [inl h0, inl h3] ++ y0))
(e (x0 ++ [inl (h0 * h3)] ++ y0)) mk: forall (x0y0 : Words) (k1k2 : K),
DPath P (amal_mu_K x0 y0 k1 k2) (e (x0 ++ [inr k1, inr k2] ++ y0))
(e (x0 ++ [inr (k1 * k2)] ++ y0)) t: forall (x0y0 : Words) (z : G),
DPath P (amal_tau x0 y0 z) (e (x0 ++ [inl (f z)] ++ y0))
(e (x0 ++ [inr (g z)] ++ y0)) oh: forallx0y0 : Words,
DPath P (amal_omega_H x0 y0) (e (x0 ++ [inl 1] ++ y0)) (e (x0 ++ y0)) ok: forallx0y0 : Words,
DPath P (amal_omega_K x0 y0) (e (x0 ++ [inr 1] ++ y0)) (e (x0 ++ y0)) 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: forallx0 : amal_type, IsHSet (P x0) e: forallw : Words, P (amal_eta w) mh: forall (x0y0 : Words) (h1h2 : H),
DPath P (amal_mu_H x0 y0 h1 h2) (e (x0 ++ [inl h1, inl h2] ++ y0))
(e (x0 ++ [inl (h1 * h2)] ++ y0)) mk: forall (x0y0 : Words) (k0k3 : K),
DPath P (amal_mu_K x0 y0 k0 k3) (e (x0 ++ [inr k0, inr k3] ++ y0))
(e (x0 ++ [inr (k0 * k3)] ++ y0)) t: forall (x0y0 : Words) (z : G),
DPath P (amal_tau x0 y0 z) (e (x0 ++ [inl (f z)] ++ y0))
(e (x0 ++ [inr (g z)] ++ y0)) oh: forallx0y0 : Words,
DPath P (amal_omega_H x0 y0) (e (x0 ++ [inl 1] ++ y0)) (e (x0 ++ y0)) ok: forallx0y0 : Words,
DPath P (amal_omega_K x0 y0) (e (x0 ++ [inr 1] ++ y0)) (e (x0 ++ y0)) 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: forallx0 : amal_type, IsHSet (P x0) e: forallw : Words, P (amal_eta w) mh: forall (x0y0 : Words) (h1h2 : H),
DPath P (amal_mu_H x0 y0 h1 h2) (e (x0 ++ [inl h1, inl h2] ++ y0))
(e (x0 ++ [inl (h1 * h2)] ++ y0)) mk: forall (x0y0 : Words) (k0k3 : K),
DPath P (amal_mu_K x0 y0 k0 k3) (e (x0 ++ [inr k0, inr k3] ++ y0))
(e (x0 ++ [inr (k0 * k3)] ++ y0)) t: forall (x0y0 : Words) (z : G),
DPath P (amal_tau x0 y0 z) (e (x0 ++ [inl (f z)] ++ y0))
(e (x0 ++ [inr (g z)] ++ y0)) oh: forallx0y0 : Words,
DPath P (amal_omega_H x0 y0) (e (x0 ++ [inl 1] ++ y0)) (e (x0 ++ y0)) ok: forallx0y0 : Words,
DPath P (amal_omega_K x0 y0) (e (x0 ++ [inr 1] ++ y0)) (e (x0 ++ y0)) 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: forallx0 : amal_type, IsHSet (P x0) e: forallw : Words, P (amal_eta w) mh: forall (x0y0 : Words) (h1h2 : H),
DPath P (amal_mu_H x0 y0 h1 h2) (e (x0 ++ [inl h1, inl h2] ++ y0))
(e (x0 ++ [inl (h1 * h2)] ++ y0)) mk: forall (x0y0 : Words) (k1k2 : K),
DPath P (amal_mu_K x0 y0 k1 k2) (e (x0 ++ [inr k1, inr k2] ++ y0))
(e (x0 ++ [inr (k1 * k2)] ++ y0)) t: forall (x0y0 : Words) (z0 : G),
DPath P (amal_tau x0 y0 z0) (e (x0 ++ [inl (f z0)] ++ y0))
(e (x0 ++ [inr (g z0)] ++ y0)) oh: forallx0y0 : Words,
DPath P (amal_omega_H x0 y0) (e (x0 ++ [inl 1] ++ y0)) (e (x0 ++ y0)) ok: forallx0y0 : Words,
DPath P (amal_omega_K x0 y0) (e (x0 ++ [inr 1] ++ y0)) (e (x0 ++ y0)) 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: forallx0 : amal_type, IsHSet (P x0) e: forallw : Words, P (amal_eta w) mh: forall (x0y0 : Words) (h1h2 : H),
DPath P (amal_mu_H x0 y0 h1 h2) (e (x0 ++ [inl h1, inl h2] ++ y0))
(e (x0 ++ [inl (h1 * h2)] ++ y0)) mk: forall (x0y0 : Words) (k1k2 : K),
DPath P (amal_mu_K x0 y0 k1 k2) (e (x0 ++ [inr k1, inr k2] ++ y0))
(e (x0 ++ [inr (k1 * k2)] ++ y0)) t: forall (x0y0 : Words) (z0 : G),
DPath P (amal_tau x0 y0 z0) (e (x0 ++ [inl (f z0)] ++ y0))
(e (x0 ++ [inr (g z0)] ++ y0)) oh: forallx0y0 : Words,
DPath P (amal_omega_H x0 y0) (e (x0 ++ [inl 1] ++ y0)) (e (x0 ++ y0)) ok: forallx0y0 : Words,
DPath P (amal_omega_K x0 y0) (e (x0 ++ [inr 1] ++ y0)) (e (x0 ++ y0)) 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: forallx0 : amal_type, IsHSet (P x0) e: forallw : Words, P (amal_eta w) mh: forall (x0y0 : Words) (h1h2 : H),
DPath P (amal_mu_H x0 y0 h1 h2) (e (x0 ++ [inl h1, inl h2] ++ y0))
(e (x0 ++ [inl (h1 * h2)] ++ y0)) mk: forall (x0y0 : Words) (k1k2 : K),
DPath P (amal_mu_K x0 y0 k1 k2) (e (x0 ++ [inr k1, inr k2] ++ y0))
(e (x0 ++ [inr (k1 * k2)] ++ y0)) t: forall (x0y0 : Words) (z : G),
DPath P (amal_tau x0 y0 z) (e (x0 ++ [inl (f z)] ++ y0))
(e (x0 ++ [inr (g z)] ++ y0)) oh: forallx0y0 : Words,
DPath P (amal_omega_H x0 y0) (e (x0 ++ [inl 1] ++ y0)) (e (x0 ++ y0)) ok: forallx0y0 : Words,
DPath P (amal_omega_K x0 y0) (e (x0 ++ [inr 1] ++ y0)) (e (x0 ++ y0)) 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: forallx0 : amal_type, IsHSet (P x0) e: forallw : Words, P (amal_eta w) mh: forall (x0y0 : Words) (h1h2 : H),
DPath P (amal_mu_H x0 y0 h1 h2) (e (x0 ++ [inl h1, inl h2] ++ y0))
(e (x0 ++ [inl (h1 * h2)] ++ y0)) mk: forall (x0y0 : Words) (k1k2 : K),
DPath P (amal_mu_K x0 y0 k1 k2) (e (x0 ++ [inr k1, inr k2] ++ y0))
(e (x0 ++ [inr (k1 * k2)] ++ y0)) t: forall (x0y0 : Words) (z : G),
DPath P (amal_tau x0 y0 z) (e (x0 ++ [inl (f z)] ++ y0))
(e (x0 ++ [inr (g z)] ++ y0)) oh: forallx0y0 : Words,
DPath P (amal_omega_H x0 y0) (e (x0 ++ [inl 1] ++ y0)) (e (x0 ++ y0)) ok: forallx0y0 : Words,
DPath P (amal_omega_K x0 y0) (e (x0 ++ [inr 1] ++ y0)) (e (x0 ++ y0)) 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: forallx0 : amal_type, IsHSet (P x0) e: forallw : Words, P (amal_eta w) mh: forall (x0y0 : Words) (h1h2 : H),
DPath P (amal_mu_H x0 y0 h1 h2) (e (x0 ++ [inl h1, inl h2] ++ y0))
(e (x0 ++ [inl (h1 * h2)] ++ y0)) mk: forall (x0y0 : Words) (k1k2 : K),
DPath P (amal_mu_K x0 y0 k1 k2) (e (x0 ++ [inr k1, inr k2] ++ y0))
(e (x0 ++ [inr (k1 * k2)] ++ y0)) t: forall (x0y0 : Words) (z : G),
DPath P (amal_tau x0 y0 z) (e (x0 ++ [inl (f z)] ++ y0))
(e (x0 ++ [inr (g z)] ++ y0)) oh: forallx0y0 : Words,
DPath P (amal_omega_H x0 y0) (e (x0 ++ [inl 1] ++ y0)) (e (x0 ++ y0)) ok: forallx0y0 : Words,
DPath P (amal_omega_K x0 y0) (e (x0 ++ [inr 1] ++ y0)) (e (x0 ++ y0)) 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: forallx0 : amal_type, IsHSet (P x0) e: forallw : Words, P (amal_eta w) mh: forall (x0y0 : Words) (h1h2 : H),
DPath P (amal_mu_H x0 y0 h1 h2) (e (x0 ++ [inl h1, inl h2] ++ y0))
(e (x0 ++ [inl (h1 * h2)] ++ y0)) mk: forall (x0y0 : Words) (k1k2 : K),
DPath P (amal_mu_K x0 y0 k1 k2) (e (x0 ++ [inr k1, inr k2] ++ y0))
(e (x0 ++ [inr (k1 * k2)] ++ y0)) t: forall (x0y0 : Words) (z : G),
DPath P (amal_tau x0 y0 z) (e (x0 ++ [inl (f z)] ++ y0))
(e (x0 ++ [inr (g z)] ++ y0)) oh: forallx0y0 : Words,
DPath P (amal_omega_H x0 y0) (e (x0 ++ [inl 1] ++ y0)) (e (x0 ++ y0)) ok: forallx0y0 : Words,
DPath P (amal_omega_K x0 y0) (e (x0 ++ [inr 1] ++ y0)) (e (x0 ++ y0)) 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 (x0y0 : Words) (h0h3 : H),
e (x0 ++ [inl h0, inl h3] ++ y0) = e (x0 ++ [inl (h0 * h3)] ++ y0) ek: forall (x0y0 : Words) (k1k2 : K),
e (x0 ++ [inr k1, inr k2] ++ y0) = e (x0 ++ [inr (k1 * k2)] ++ y0) t: forall (x0y0 : Words) (z : G),
e (x0 ++ [inl (f z)] ++ y0) = e (x0 ++ [inr (g z)] ++ y0) oh: forallx0y0 : Words, e (x0 ++ [inl 1] ++ y0) = e (x0 ++ y0) ok: forallx0y0 : Words, e (x0 ++ [inr 1] ++ y0) = e (x0 ++ y0) 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 (x0y0 : Words) (h1h2 : H),
e (x0 ++ [inl h1, inl h2] ++ y0) = e (x0 ++ [inl (h1 * h2)] ++ y0) ek: forall (x0y0 : Words) (k0k3 : K),
e (x0 ++ [inr k0, inr k3] ++ y0) = e (x0 ++ [inr (k0 * k3)] ++ y0) t: forall (x0y0 : Words) (z : G),
e (x0 ++ [inl (f z)] ++ y0) = e (x0 ++ [inr (g z)] ++ y0) oh: forallx0y0 : Words, e (x0 ++ [inl 1] ++ y0) = e (x0 ++ y0) ok: forallx0y0 : Words, e (x0 ++ [inr 1] ++ y0) = e (x0 ++ y0) 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 (x0y0 : Words) (h1h2 : H),
e (x0 ++ [inl h1, inl h2] ++ y0) = e (x0 ++ [inl (h1 * h2)] ++ y0) ek: forall (x0y0 : Words) (k1k2 : K),
e (x0 ++ [inr k1, inr k2] ++ y0) = e (x0 ++ [inr (k1 * k2)] ++ y0) t: forall (x0y0 : Words) (z0 : G),
e (x0 ++ [inl (f z0)] ++ y0) = e (x0 ++ [inr (g z0)] ++ y0) oh: forallx0y0 : Words, e (x0 ++ [inl 1] ++ y0) = e (x0 ++ y0) ok: forallx0y0 : Words, e (x0 ++ [inr 1] ++ y0) = e (x0 ++ y0) 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 (x0y0 : Words) (h1h2 : H),
e (x0 ++ [inl h1, inl h2] ++ y0) = e (x0 ++ [inl (h1 * h2)] ++ y0) ek: forall (x0y0 : Words) (k1k2 : K),
e (x0 ++ [inr k1, inr k2] ++ y0) = e (x0 ++ [inr (k1 * k2)] ++ y0) t: forall (x0y0 : Words) (z : G),
e (x0 ++ [inl (f z)] ++ y0) = e (x0 ++ [inr (g z)] ++ y0) oh: forallx0y0 : Words, e (x0 ++ [inl 1] ++ y0) = e (x0 ++ y0) ok: forallx0y0 : Words, e (x0 ++ [inr 1] ++ y0) = e (x0 ++ y0) 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 (x0y0 : Words) (h1h2 : H),
e (x0 ++ [inl h1, inl h2] ++ y0) = e (x0 ++ [inl (h1 * h2)] ++ y0) ek: forall (x0y0 : Words) (k1k2 : K),
e (x0 ++ [inr k1, inr k2] ++ y0) = e (x0 ++ [inr (k1 * k2)] ++ y0) t: forall (x0y0 : Words) (z : G),
e (x0 ++ [inl (f z)] ++ y0) = e (x0 ++ [inr (g z)] ++ y0) oh: forallx0y0 : Words, e (x0 ++ [inl 1] ++ y0) = e (x0 ++ y0) ok: forallx0y0 : Words, e (x0 ++ [inr 1] ++ y0) = e (x0 ++ y0) 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 (x0y0 : Words) (h1h2 : H),
e (x0 ++ [inl h1, inl h2] ++ y0) = e (x0 ++ [inl (h1 * h2)] ++ y0) ek: forall (x0y0 : Words) (k0k3 : K),
e (x0 ++ [inr k0, inr k3] ++ y0) = e (x0 ++ [inr (k0 * k3)] ++ y0) t: forall (x0y0 : Words) (z : G),
e (x0 ++ [inl (f z)] ++ y0) = e (x0 ++ [inr (g z)] ++ y0) oh: forallx0y0 : Words, e (x0 ++ [inl 1] ++ y0) = e (x0 ++ y0) ok: forallx0y0 : Words, e (x0 ++ [inr 1] ++ y0) = e (x0 ++ y0) 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 (x0y0 : Words) (h1h2 : H),
e (x0 ++ [inl h1, inl h2] ++ y0) = e (x0 ++ [inl (h1 * h2)] ++ y0) ek: forall (x0y0 : Words) (k1k2 : K),
e (x0 ++ [inr k1, inr k2] ++ y0) = e (x0 ++ [inr (k1 * k2)] ++ y0) t: forall (x0y0 : Words) (z0 : G),
e (x0 ++ [inl (f z0)] ++ y0) = e (x0 ++ [inr (g z0)] ++ y0) oh: forallx0y0 : Words, e (x0 ++ [inl 1] ++ y0) = e (x0 ++ y0) ok: forallx0y0 : Words, e (x0 ++ [inr 1] ++ y0) = e (x0 ++ y0) 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 (x0y0 : Words) (h1h2 : H),
e (x0 ++ [inl h1, inl h2] ++ y0) = e (x0 ++ [inl (h1 * h2)] ++ y0) ek: forall (x0y0 : Words) (k1k2 : K),
e (x0 ++ [inr k1, inr k2] ++ y0) = e (x0 ++ [inr (k1 * k2)] ++ y0) t: forall (x0y0 : Words) (z : G),
e (x0 ++ [inl (f z)] ++ y0) = e (x0 ++ [inr (g z)] ++ y0) oh: forallx0y0 : Words, e (x0 ++ [inl 1] ++ y0) = e (x0 ++ y0) ok: forallx0y0 : Words, e (x0 ++ [inr 1] ++ y0) = e (x0 ++ y0) 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 (x0y0 : Words) (h1h2 : H),
e (x0 ++ [inl h1, inl h2] ++ y0) = e (x0 ++ [inl (h1 * h2)] ++ y0) ek: forall (x0y0 : Words) (k1k2 : K),
e (x0 ++ [inr k1, inr k2] ++ y0) = e (x0 ++ [inr (k1 * k2)] ++ y0) t: forall (x0y0 : Words) (z : G),
e (x0 ++ [inl (f z)] ++ y0) = e (x0 ++ [inr (g z)] ++ y0) oh: forallx0y0 : Words, e (x0 ++ [inl 1] ++ y0) = e (x0 ++ y0) ok: forallx0y0 : Words, e (x0 ++ [inr 1] ++ y0) = e (x0 ++ y0) 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 (x0y0 : Words) (h1h2 : H),
e (x0 ++ [inl h1, inl h2] ++ y0) = e (x0 ++ [inl (h1 * h2)] ++ y0) ek: forall (x0y0 : Words) (k1k2 : K),
e (x0 ++ [inr k1, inr k2] ++ y0) = e (x0 ++ [inr (k1 * k2)] ++ y0) t: forall (x0y0 : Words) (z0 : G),
e (x0 ++ [inl (f z0)] ++ y0) = e (x0 ++ [inr (g z0)] ++ y0) oh: forallx0y0 : Words, e (x0 ++ [inl 1] ++ y0) = e (x0 ++ y0) ok: forallx0y0 : Words, e (x0 ++ [inr 1] ++ y0) = e (x0 ++ y0) 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 (x0y0 : Words) (h1h2 : H),
e (x0 ++ [inl h1, inl h2] ++ y0) = e (x0 ++ [inl (h1 * h2)] ++ y0) ek: forall (x0y0 : Words) (k1k2 : K),
e (x0 ++ [inr k1, inr k2] ++ y0) = e (x0 ++ [inr (k1 * k2)] ++ y0) t: forall (x0y0 : Words) (z : G),
e (x0 ++ [inl (f z)] ++ y0) = e (x0 ++ [inr (g z)] ++ y0) oh: forallx0y0 : Words, e (x0 ++ [inl 1] ++ y0) = e (x0 ++ y0) ok: forallx0y0 : Words, e (x0 ++ [inr 1] ++ y0) = e (x0 ++ y0) 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 (x0y0 : Words) (h1h2 : H),
e (x0 ++ [inl h1, inl h2] ++ y0) = e (x0 ++ [inl (h1 * h2)] ++ y0) ek: forall (x0y0 : Words) (k1k2 : K),
e (x0 ++ [inr k1, inr k2] ++ y0) = e (x0 ++ [inr (k1 * k2)] ++ y0) t: forall (x0y0 : Words) (z : G),
e (x0 ++ [inl (f z)] ++ y0) = e (x0 ++ [inr (g z)] ++ y0) oh: forallx0y0 : Words, e (x0 ++ [inl 1] ++ y0) = e (x0 ++ y0) ok: forallx0y0 : Words, e (x0 ++ [inr 1] ++ y0) = e (x0 ++ y0) 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 (x0y0 : Words) (h1h2 : H),
e (x0 ++ [inl h1, inl h2] ++ y0) = e (x0 ++ [inl (h1 * h2)] ++ y0) ek: forall (x0y0 : Words) (k1k2 : K),
e (x0 ++ [inr k1, inr k2] ++ y0) = e (x0 ++ [inr (k1 * k2)] ++ y0) t: forall (x0y0 : Words) (z : G),
e (x0 ++ [inl (f z)] ++ y0) = e (x0 ++ [inr (g z)] ++ y0) oh: forallx0y0 : Words, e (x0 ++ [inl 1] ++ y0) = e (x0 ++ y0) ok: forallx0y0 : Words, e (x0 ++ [inr 1] ++ y0) = e (x0 ++ y0) 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 (x0y0 : Words) (h1h2 : H),
e (x0 ++ [inl h1, inl h2] ++ y0) = e (x0 ++ [inl (h1 * h2)] ++ y0) ek: forall (x0y0 : Words) (k1k2 : K),
e (x0 ++ [inr k1, inr k2] ++ y0) = e (x0 ++ [inr (k1 * k2)] ++ y0) t: forall (x0y0 : Words) (z : G),
e (x0 ++ [inl (f z)] ++ y0) = e (x0 ++ [inr (g z)] ++ y0) oh: forallx0y0 : Words, e (x0 ++ [inl 1] ++ y0) = e (x0 ++ y0) ok: forallx0y0 : Words, e (x0 ++ [inr 1] ++ y0) = e (x0 ++ y0) 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 (x0y0 : Words) (h1h2 : H),
e (x0 ++ [inl h1, inl h2] ++ y0) = e (x0 ++ [inl (h1 * h2)] ++ y0) ek: forall (x0y0 : Words) (k1k2 : K),
e (x0 ++ [inr k1, inr k2] ++ y0) = e (x0 ++ [inr (k1 * k2)] ++ y0) t: forall (x0y0 : Words) (z : G),
e (x0 ++ [inl (f z)] ++ y0) = e (x0 ++ [inr (g z)] ++ y0) oh: forallx0y0 : Words, e (x0 ++ [inl 1] ++ y0) = e (x0 ++ y0) ok: forallx0y0 : Words, e (x0 ++ [inr 1] ++ y0) = e (x0 ++ y0) 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 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 sgop_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 g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
end)
1 w)
(x ++ [inl h1, inl h2] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
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 g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
end)
1 w)
(x ++ [inr k1, inr k2] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
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 g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
end)
1 w)
(x ++ [inl (f z)] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
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 g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
end)
1 w)
(x ++ [inl 1] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
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 g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
end)
1 w)
(x ++ [inr 1] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
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 g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
end)
1 w)
(x ++ [inl h1, inl h2] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 (x ++ [inl h1, inl h2] ++ y) =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 y)
[inl h1, inl h2])
x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 y)
[inl h1, inl h2] =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 y) =
h (h1 * h2) *
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 y =
h (h1 * h2) *
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
end)
1 w)
(x ++ [inr k1, inr k2] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
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 g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
end)
1 w)
(x ++ [inl (f z)] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
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 g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
end)
1 w)
(x ++ [inl 1] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
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 g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
end)
1 w)
(x ++ [inr 1] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
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 g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
end)
1 w)
(x ++ [inr k1, inr k2] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 (x ++ [inr k1, inr k2] ++ y) =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 y)
[inr k1, inr k2])
x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 y)
[inr k1, inr k2] =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 y) =
k (k1 * k2) *
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 y =
k (k1 * k2) *
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
end)
1 w)
(x ++ [inl (f z)] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
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 g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
end)
1 w)
(x ++ [inl 1] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
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 g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
end)
1 w)
(x ++ [inr 1] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
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 g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
end)
1 w)
(x ++ [inl (f z)] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 (x ++ [inl (f z)] ++ y) =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 y)
[inl (f z)])
x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
end)
1 w)
(x ++ [inl 1] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
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 g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
end)
1 w)
(x ++ [inr 1] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
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 g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
end)
1 w)
(x ++ [inl 1] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 (x ++ [inl 1] ++ y) =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 y)
[inl 1])
x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 y)
[inl 1] =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 y =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 y =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
end)
1 w)
(x ++ [inr 1] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
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 g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
end)
1 w)
(x ++ [inr 1] ++ y) =
(funw : Words =>
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => (fun (l : H) (x0 : X) => h l * x0) g0
| inr g0 => (fun (r : K) (x0 : X) => k r * x0) g0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 (x ++ [inr 1] ++ y) =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 y)
[inr 1])
x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 y)
[inr 1] =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 y =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 y =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 (x ++ y) =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 x *
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 y)
x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 x *
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
s x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 g0 => funx : X => h g0 * x
| inr g0 => funx : X => k g0 * x
end)
s nil =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx : X => h g0 * x
| inr g0 => funx : X => k g0 * 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 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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
s x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 x *
s
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
s (a :: x) =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
s x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 x *
s
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
s (a :: x) =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
s x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 x *
s
match a with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
s x) =
match a with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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 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 g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
s x =
fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 x *
s
match a with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end)
1 x *
s) =
match a with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
end
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => h g0 * x0
| inr g0 => funx0 : X => k g0 * x0
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
(funx0 : amal_type f g =>
AmalgamatedFreeProduct_rec X (grp_homo_compose r amal_inl)
(grp_homo_compose r amal_inr)
(funx1 : G =>
ap r
(internal_paths_rew
(funl : list (H + K) => amal_eta l = amal_eta [inr (g x1)])
(internal_paths_rew
(funl : list (H + K) =>
amal_eta ([inl (f x1)] ++ nil) = amal_eta l)
(amal_tau nil nil x1) (app_nil [inr (g x1)]))
(app_nil [inl (f x1)])))
x0 =
r x0) (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 x: list (H + K) IHx: 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)])))
(amal_eta x) =
r (amal_eta x)
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)])))
(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 x: list (H + K) IHx: 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)])))
(amal_eta x) =
r (amal_eta x)
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)])))
(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 x: list (H + K) IHx: fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => r (amal_eta [inl g0]) * x0
| inr g0 => funx0 : X => r (amal_eta [inr g0]) * x0
end)
1 x =
r (amal_eta x)
match a with
| inl g0 => funx0 : X => r (amal_eta [inl g0]) * x0
| inr g0 => funx0 : X => r (amal_eta [inr g0]) * x0
end
(fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => r (amal_eta [inl g0]) * x0
| inr g0 => funx0 : X => r (amal_eta [inr g0]) * x0
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 x: list (H + K) IHx: fold_right
(funX0 : H + K =>
match X0 with
| inl g0 => funx0 : X => r (amal_eta [inl g0]) * x0
| inr g0 => funx0 : X => r (amal_eta [inr g0]) * x0
end)
1 x =
r (amal_eta x)
match a with
| inl g0 => funx0 : X => r (amal_eta [inl g0]) * x0
| inr g0 => funx0 : X => r (amal_eta [inr g0]) * x0
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: foralla0 : H, P (amal_inl a0) 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
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: foralla0 : H, P (amal_inl a0) 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
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: foralla0 : H, P (amal_inl a0) 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: forallb0 : K, P (amal_inr b0) 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: foralla0 : H, P (amal_inl a0) 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: foralla0 : H, P (amal_inl a0) 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: forallb0 : K, P (amal_inr b0) 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: forallb0 : K, P (amal_inr b0) 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