Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Forall Types.Sigma Types.Prod. Require Import WildCat.Core WildCat.Equiv WildCat.Monoidal WildCat.Bifunctor. Require Import WildCat.NatTrans WildCat.MonoidalTwistConstruction. Require Import Algebra.Groups.Group Algebra.Groups.QuotientGroup. Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Biproduct. Require Import Algebra.AbGroups.AbHom Algebra.AbGroups.FreeAbelianGroup. Require Import Algebra.AbGroups.Abelianization Algebra Algebra.Groups.FreeGroup. Require Import Colimits.Quotient. Require Import Spaces.List.Core Spaces.Int. Require Import AbGroups.Z. Require Import Truncations. Local Open Scope mc_add_scope. (** * The Tensor Product of Abelian Groups *) (** Various maps [A * B → C] from the cartesian product of two abelian groups to another abelian group are "biadditive" (also called "bilinear"), meaning that they are group homomorphisms when we fix the left or right argument. The tensor product of abelian groups is a construction that produces an abelian group [A ⊗ B] along with a biadditive map [A * B -> A ⊗ B] which is initial among biadditive maps from [A * B]. This means that any biadditive map [A * B → C] factors uniquely through the tensor product via a group homomorphism [A ⊗ B -> C]. Biadditive functions appear in all sorts of contexts ranging from linear algebra to analysis. Therefore having a way to systematically study them is very useful. *) (** ** Construction *) (** We define the tensor product of abelian groups as a quotient of the free abelian group on pairs of elements of the two groups by the subgroup generated by the biadditive pairs. *) (** Here we define the subgroup of biadditive pairs in two steps. *)
A, B: AbGroup

FreeAbGroup (A * B) -> Type
A, B: AbGroup

FreeAbGroup (A * B) -> Type
A, B: AbGroup
x: FreeAbGroup (A * B)

Type
A, B: AbGroup
x: FreeAbGroup (A * B)
a1, a2: A
b: B

Type
A, B: AbGroup
x: FreeAbGroup (A * B)
a: A
b1, b2: B
Type
A, B: AbGroup
x: FreeAbGroup (A * B)
a1, a2: A
b: B

Type
A, B: AbGroup
x: FreeAbGroup (A * B)
a1, a2: A
b: B

FreeAbGroup (A * B)
A, B: AbGroup
x: FreeAbGroup (A * B)
a1, a2: A
b: B
FreeAbGroup (A * B)
A, B: AbGroup
x: FreeAbGroup (A * B)
a1, a2: A
b: B
FreeAbGroup (A * B)
A, B: AbGroup
x: FreeAbGroup (A * B)
a1, a2: A
b: B

A * B
A, B: AbGroup
x: FreeAbGroup (A * B)
a1, a2: A
b: B
A * B
A, B: AbGroup
x: FreeAbGroup (A * B)
a1, a2: A
b: B
A * B
A, B: AbGroup
x: FreeAbGroup (A * B)
a1, a2: A
b: B

A * B
exact (a1 + a2, b).
A, B: AbGroup
x: FreeAbGroup (A * B)
a1, a2: A
b: B

A * B
exact (a1, b).
A, B: AbGroup
x: FreeAbGroup (A * B)
a1, a2: A
b: B

A * B
exact (a2, b).
A, B: AbGroup
x: FreeAbGroup (A * B)
a: A
b1, b2: B

Type
A, B: AbGroup
x: FreeAbGroup (A * B)
a: A
b1, b2: B

FreeAbGroup (A * B)
A, B: AbGroup
x: FreeAbGroup (A * B)
a: A
b1, b2: B
FreeAbGroup (A * B)
A, B: AbGroup
x: FreeAbGroup (A * B)
a: A
b1, b2: B
FreeAbGroup (A * B)
A, B: AbGroup
x: FreeAbGroup (A * B)
a: A
b1, b2: B

A * B
A, B: AbGroup
x: FreeAbGroup (A * B)
a: A
b1, b2: B
A * B
A, B: AbGroup
x: FreeAbGroup (A * B)
a: A
b1, b2: B
A * B
A, B: AbGroup
x: FreeAbGroup (A * B)
a: A
b1, b2: B

A * B
exact (a, b1 + b2).
A, B: AbGroup
x: FreeAbGroup (A * B)
a: A
b1, b2: B

A * B
exact (a, b1).
A, B: AbGroup
x: FreeAbGroup (A * B)
a: A
b1, b2: B

A * B
exact (a, b2). Defined. Definition subgroup_biadditive_pairs {A B : AbGroup} : Subgroup (FreeAbGroup (A * B)) := subgroup_generated family_biadditive_pairs. (** The tensor product [ab_tensor_prod A B] of two abelian groups [A] and [B] is defined to be a quotient of the free abelian group on pairs of elements [A * B] by the subgroup of biadditive pairs. *) Definition ab_tensor_prod (A B : AbGroup) : AbGroup := QuotientAbGroup (FreeAbGroup (A * B)) subgroup_biadditive_pairs. Arguments ab_tensor_prod A B : simpl never. (** The tensor product of [A] and [B] contains formal sums and differences of pairs of elements from [A] and [B]. We denote these pairs as "simple tensors" and name them [tensor]. *) Definition tensor {A B : AbGroup} : A -> B -> ab_tensor_prod A B := fun a b => grp_quotient_map (freeabgroup_in (a, b)). (** ** Properties of tensors *) (** The characterizing property of simple tensors are that they are biadditive in their arguments. *) (** A [tensor] of a sum distributes over the sum on the left. *)
A, B: AbGroup
a: A
b, b': B

tensor a (b + b') = tensor a b + tensor a b'
A, B: AbGroup
a: A
b, b': B

tensor a (b + b') = tensor a b + tensor a b'
A, B: AbGroup
a: A
b, b': B

subgroup_generated_type family_biadditive_pairs (- freeabgroup_in (a, b + b') + (freeabgroup_in (a, b) + freeabgroup_in (a, b')))
A, B: AbGroup
a: A
b, b': B

family_biadditive_pairs (- freeabgroup_in (a, b + b') + (freeabgroup_in (a, b) + freeabgroup_in (a, b')))
A, B: AbGroup
a: A
b, b': B

{a0 : A & {b1 : B & {b2 : B & - freeabgroup_in (a0, b1 + b2) + (freeabgroup_in (a0, b1) + freeabgroup_in (a0, b2)) = - freeabgroup_in (a, b + b') + (freeabgroup_in (a, b) + freeabgroup_in (a, b'))}}}
by exists a, b, b'. Defined. (** A [tensor] of a sum distributes over the sum on the right. *)
A, B: AbGroup
a, a': A
b: B

tensor (a + a') b = tensor a b + tensor a' b
A, B: AbGroup
a, a': A
b: B

tensor (a + a') b = tensor a b + tensor a' b
A, B: AbGroup
a, a': A
b: B

subgroup_generated_type family_biadditive_pairs (- freeabgroup_in (a + a', b) + (freeabgroup_in (a, b) + freeabgroup_in (a', b)))
A, B: AbGroup
a, a': A
b: B

family_biadditive_pairs (- freeabgroup_in (a + a', b) + (freeabgroup_in (a, b) + freeabgroup_in (a', b)))
A, B: AbGroup
a, a': A
b: B

{a1 : A & {a2 : A & {b0 : B & - freeabgroup_in (a1 + a2, b0) + (freeabgroup_in (a1, b0) + freeabgroup_in (a2, b0)) = - freeabgroup_in (a + a', b) + (freeabgroup_in (a, b) + freeabgroup_in (a', b))}}}
by exists a, a', b. Defined. (** Tensoring on the left is a group homomorphism. *)
A, B: AbGroup
a: A

B $-> ab_tensor_prod A B
A, B: AbGroup
a: A

B $-> ab_tensor_prod A B
A, B: AbGroup
a: A

B -> ab_tensor_prod A B
A, B: AbGroup
a: A
IsSemiGroupPreserving ?grp_homo_map
A, B: AbGroup
a: A

B -> ab_tensor_prod A B
exact (fun b => tensor a b).
A, B: AbGroup
a: A

IsSemiGroupPreserving (fun b : B => tensor a b)
A, B: AbGroup
a: A
b, b': B

tensor a (b + b') = tensor a b + tensor a b'
napply tensor_dist_l. Defined. (** Tensoring on the right is a group homomorphism. *)
A, B: AbGroup
b: B

A $-> ab_tensor_prod A B
A, B: AbGroup
b: B

A $-> ab_tensor_prod A B
A, B: AbGroup
b: B

A -> ab_tensor_prod A B
A, B: AbGroup
b: B
IsSemiGroupPreserving ?grp_homo_map
A, B: AbGroup
b: B

A -> ab_tensor_prod A B
exact (fun a => tensor a b).
A, B: AbGroup
b: B

IsSemiGroupPreserving (fun a : A => tensor a b)
A, B: AbGroup
b: B
a, a': A

tensor (a + a') b = tensor a b + tensor a' b
napply tensor_dist_r. Defined. (** Tensors preserve negation in the left argument. *) Definition tensor_neg_l {A B : AbGroup} (a : A) (b : B) : tensor (-a) b = - tensor a b := grp_homo_inv (grp_homo_tensor_r b) a. (** Tensors preserve negation in the right argument. *) Definition tensor_neg_r {A B : AbGroup} (a : A) (b : B) : tensor a (-b) = - tensor a b := grp_homo_inv (grp_homo_tensor_l a) b. (** Tensoring by zero on the left is zero. *) Definition tensor_zero_l {A B : AbGroup} (b : B) : tensor (A:=A) 0 b = 0 := grp_homo_unit (grp_homo_tensor_r b). (** Tensoring by zero on the right is zero. *) Definition tensor_zero_r {A B : AbGroup} (a : A) : tensor (B:=B) a 0 = 0 := grp_homo_unit (grp_homo_tensor_l a). (** The [tensor] map is biadditive and therefore can be written in a curried form using the internal abelian group hom. *)
H: Funext
A, B: AbGroup

A $-> ab_hom B (ab_tensor_prod A B)
H: Funext
A, B: AbGroup

A $-> ab_hom B (ab_tensor_prod A B)
H: Funext
A, B: AbGroup

A -> ab_hom B (ab_tensor_prod A B)
H: Funext
A, B: AbGroup
IsSemiGroupPreserving ?grp_homo_map
H: Funext
A, B: AbGroup

A -> ab_hom B (ab_tensor_prod A B)
H: Funext
A, B: AbGroup
a: A

ab_hom B (ab_tensor_prod A B)
H: Funext
A, B: AbGroup
a: A

B -> ab_tensor_prod A B
H: Funext
A, B: AbGroup
a: A
IsSemiGroupPreserving ?grp_homo_map
H: Funext
A, B: AbGroup
a: A

B -> ab_tensor_prod A B
exact (tensor a).
H: Funext
A, B: AbGroup
a: A

IsSemiGroupPreserving (tensor a)
napply tensor_dist_l.
H: Funext
A, B: AbGroup

IsSemiGroupPreserving (fun a : A => {| grp_homo_map := tensor a; issemigrouppreserving_grp_homo := tensor_dist_l a |})
H: Funext
A, B: AbGroup
a, a': A

{| grp_homo_map := tensor (a + a'); issemigrouppreserving_grp_homo := tensor_dist_l (a + a') |} = {| grp_homo_map := tensor a; issemigrouppreserving_grp_homo := tensor_dist_l a |} + {| grp_homo_map := tensor a'; issemigrouppreserving_grp_homo := tensor_dist_l a' |}
H: Funext
A, B: AbGroup
a, a': A

{| grp_homo_map := tensor (a + a'); issemigrouppreserving_grp_homo := tensor_dist_l (a + a') |} == {| grp_homo_map := tensor a; issemigrouppreserving_grp_homo := tensor_dist_l a |} + {| grp_homo_map := tensor a'; issemigrouppreserving_grp_homo := tensor_dist_l a' |}
H: Funext
A, B: AbGroup
a, a': A
b: B

{| grp_homo_map := tensor (a + a'); issemigrouppreserving_grp_homo := tensor_dist_l (a + a') |} b = ({| grp_homo_map := tensor a; issemigrouppreserving_grp_homo := tensor_dist_l a |} + {| grp_homo_map := tensor a'; issemigrouppreserving_grp_homo := tensor_dist_l a' |}) b
napply tensor_dist_r. Defined. (** ** Induction principles *) (** Here we write down some induction principles to help us prove lemmas about the tensor product. Some of these are quite specialised but are patterns that appear often in practice. *) (** Our main recursion principle states that in order to build a homomorphism out of the tensor product, it is sufficient to provide a map out of the direct product which is biadditive, that is, a map that preserves addition in each argument of the product. *) (** We separate out the proof of this part, so we can make it opaque. *)
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b
x: FreeAbGroup (A * B)
insg: subgroup_biadditive_pairs x

grp_homo_abel_rec (FreeGroup_rec (uncurry f)) x = 0
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b
x: FreeAbGroup (A * B)
insg: subgroup_biadditive_pairs x

grp_homo_abel_rec (FreeGroup_rec (uncurry f)) x = 0
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b
x: FreeAbGroup (A * B)
insg: subgroup_biadditive_pairs x
abel_rec:= grp_homo_abel_rec (FreeGroup_rec (uncurry f)): abel (FreeGroup (A * B)) $-> C

abel_rec x = 0
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b
x: FreeAbGroup (A * B)
abel_rec:= grp_homo_abel_rec (FreeGroup_rec (uncurry f)): abel (FreeGroup (A * B)) $-> C
insg: subgroup_generated_type family_biadditive_pairs x

abel_rec x = 0
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b
abel_rec:= grp_homo_abel_rec (FreeGroup_rec (uncurry f)): abel (FreeGroup (A * B)) $-> C
x: FreeAbGroup (A * B)
biad: family_biadditive_pairs x

abel_rec x = 0
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b
abel_rec:= grp_homo_abel_rec (FreeGroup_rec (uncurry f)): abel (FreeGroup (A * B)) $-> C
abel_rec 0 = 0
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b
abel_rec:= grp_homo_abel_rec (FreeGroup_rec (uncurry f)): abel (FreeGroup (A * B)) $-> C
g, h: FreeAbGroup (A * B)
insg_g: subgroup_generated_type family_biadditive_pairs g
insg_h: subgroup_generated_type family_biadditive_pairs h
IHg: abel_rec g = 0
IHh: abel_rec h = 0
abel_rec (g - h) = 0
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b
abel_rec:= grp_homo_abel_rec (FreeGroup_rec (uncurry f)): abel (FreeGroup (A * B)) $-> C
x: FreeAbGroup (A * B)
biad: family_biadditive_pairs x

abel_rec x = 0
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b
abel_rec:= grp_homo_abel_rec (FreeGroup_rec (uncurry f)): abel (FreeGroup (A * B)) $-> C
x: FreeAbGroup (A * B)
a, a': A
b: B
p: - freeabgroup_in (a + a', b) + (freeabgroup_in (a, b) + freeabgroup_in (a', b)) = x

abel_rec x = 0
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b
abel_rec:= grp_homo_abel_rec (FreeGroup_rec (uncurry f)): abel (FreeGroup (A * B)) $-> C
x: FreeAbGroup (A * B)
a: A
b, b': B
p: - freeabgroup_in (a, b + b') + (freeabgroup_in (a, b) + freeabgroup_in (a, b')) = x
abel_rec x = 0
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b
abel_rec:= grp_homo_abel_rec (FreeGroup_rec (uncurry f)): abel (FreeGroup (A * B)) $-> C
a, a': A
b: B

- f (a + a') b + (f a b + f a' b) = 0
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b
abel_rec:= grp_homo_abel_rec (FreeGroup_rec (uncurry f)): abel (FreeGroup (A * B)) $-> C
a: A
b, b': B
- f a (b + b') + (f a b + f a b') = 0
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b
abel_rec:= grp_homo_abel_rec (FreeGroup_rec (uncurry f)): abel (FreeGroup (A * B)) $-> C
a, a': A
b: B

f (a + a') b = f a b + f a' b
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b
abel_rec:= grp_homo_abel_rec (FreeGroup_rec (uncurry f)): abel (FreeGroup (A * B)) $-> C
a: A
b, b': B
f a (b + b') = f a b + f a b'
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b
abel_rec:= grp_homo_abel_rec (FreeGroup_rec (uncurry f)): abel (FreeGroup (A * B)) $-> C
a: A
b, b': B

f a (b + b') = f a b + f a b'
apply l.
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b
abel_rec:= grp_homo_abel_rec (FreeGroup_rec (uncurry f)): abel (FreeGroup (A * B)) $-> C

abel_rec 0 = 0
napply grp_homo_unit.
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b
abel_rec:= grp_homo_abel_rec (FreeGroup_rec (uncurry f)): abel (FreeGroup (A * B)) $-> C
g, h: FreeAbGroup (A * B)
insg_g: subgroup_generated_type family_biadditive_pairs g
insg_h: subgroup_generated_type family_biadditive_pairs h
IHg: abel_rec g = 0
IHh: abel_rec h = 0

abel_rec (g - h) = 0
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b
abel_rec:= grp_homo_abel_rec (FreeGroup_rec (uncurry f)): abel (FreeGroup (A * B)) $-> C
g, h: FreeAbGroup (A * B)
insg_g: subgroup_generated_type family_biadditive_pairs g
insg_h: subgroup_generated_type family_biadditive_pairs h
IHg: abel_rec g = 0
IHh: abel_rec h = 0

abel_rec g - abel_rec h = 0
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b
abel_rec:= grp_homo_abel_rec (FreeGroup_rec (uncurry f)): abel (FreeGroup (A * B)) $-> C
g, h: FreeAbGroup (A * B)
insg_g: subgroup_generated_type family_biadditive_pairs g
insg_h: subgroup_generated_type family_biadditive_pairs h
IHg: abel_rec g = 0
IHh: abel_rec h = 0

abel_rec g = abel_rec h
exact (IHg @ IHh^). Defined. Opaque ab_tensor_prod_rec_helper.
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b

ab_tensor_prod A B $-> C
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b

ab_tensor_prod A B $-> C
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b

QuotientAbGroup (FreeAbGroup (A * B)) subgroup_biadditive_pairs $-> C
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b

FreeAbGroup (A * B) $-> C
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b
forall n : FreeAbGroup (A * B), {| normalsubgroup_subgroup := subgroup_biadditive_pairs; normalsubgroup_isnormal := isnormal_ab_subgroup (FreeAbGroup (A * B)) subgroup_biadditive_pairs |} n -> ?f n = 0
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b

FreeAbGroup (A * B) $-> C
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b

A * B -> C
exact (uncurry f).
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b

forall n : FreeAbGroup (A * B), {| normalsubgroup_subgroup := subgroup_biadditive_pairs; normalsubgroup_isnormal := isnormal_ab_subgroup (FreeAbGroup (A * B)) subgroup_biadditive_pairs |} n -> FreeAbGroup_rec (uncurry f) n = 0
A, B, C: AbGroup
f: A -> B -> C
l: forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
r: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b

forall n : FreeAbGroup (A * B), subgroup_biadditive_pairs n -> FreeAbGroup_rec (uncurry f) n = 0
apply ab_tensor_prod_rec_helper; assumption. Defined. (** A special case that arises. *)
A, B, C: AbGroup
f: A -> B $-> C
l: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b

ab_tensor_prod A B $-> C
A, B, C: AbGroup
f: A -> B $-> C
l: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b

ab_tensor_prod A B $-> C
A, B, C: AbGroup
f: A -> B $-> C
l: forall (a a' : A) (b : B), f (a + a') b = f a b + f a' b

forall (a : A) (b b' : B), f a (b + b') = f a b + f a b'
intro a; apply grp_homo_op. Defined. (** We give an induction principle for an hprop-valued type family [P]. It may be surprising at first that we only require [P] to hold for the simple tensors [tensor a b] and be closed under addition. It automatically follows that [P 0] holds (since [tensor 0 0 = 0]) and that [P] is closed under negation (since [tensor -a b = - tensor a b]). This induction principle says that the simple tensors generate the tensor product as a semigroup. *)
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)

forall x : ab_tensor_prod A B, P x
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)

forall x : ab_tensor_prod A B, P x
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)

forall x : QuotientAbGroup (FreeAbGroup (A * B)) subgroup_biadditive_pairs, P x
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)

forall x : FreeAbGroup (A * B), P (grp_quotient_map x)
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)

forall x : FreeGroup (A * B), P (grp_quotient_map (abel_in x))
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)
tensor_in:= grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B: FreeGroup (A * B) $-> ab_tensor_prod A B

forall x : FreeGroup (A * B), P (grp_quotient_map (abel_in x))
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)
tensor_in:= grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B: FreeGroup (A * B) $-> ab_tensor_prod A B

forall x : FreeGroup (A * B), P (tensor_in x)
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)
tensor_in:= grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B: FreeGroup (A * B) $-> ab_tensor_prod A B
w: FreeGroup.Words (A * B)

P (tensor_in (freegroup_eta w))
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)
tensor_in:= grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B: FreeGroup (A * B) $-> ab_tensor_prod A B

P (tensor_in (freegroup_eta nil))
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)
tensor_in:= grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B: FreeGroup (A * B) $-> ab_tensor_prod A B
a: (A * B + A * B)%type
w: list (A * B + A * B)
IHw: P (tensor_in (freegroup_eta w))
P (tensor_in (freegroup_eta (a :: w)%list))
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)
tensor_in:= grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B: FreeGroup (A * B) $-> ab_tensor_prod A B

P (tensor_in (freegroup_eta nil))
exact (transport P (tensor_zero_l 0) (Hin 0 0)).
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)
tensor_in:= grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B: FreeGroup (A * B) $-> ab_tensor_prod A B
a: (A * B + A * B)%type
w: list (A * B + A * B)
IHw: P (tensor_in (freegroup_eta w))

P (tensor_in (freegroup_eta (a :: w)%list))
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)
tensor_in:= grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B: FreeGroup (A * B) $-> ab_tensor_prod A B
a: (A * B + A * B)%type
w: list (A * B + A * B)
IHw: P (tensor_in (freegroup_eta w))

P (tensor_in (freegroup_eta [a]%list + freegroup_eta w))
(* This [rewrite] is [reflexivity], but the [Defined] is slow if [change] is used instead. *)
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)
tensor_in:= grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B: FreeGroup (A * B) $-> ab_tensor_prod A B
a: (A * B + A * B)%type
w: list (A * B + A * B)
IHw: P (tensor_in (freegroup_eta w))

P (tensor_in (freegroup_eta [a]%list) + tensor_in (freegroup_eta w))
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)
tensor_in:= grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B: FreeGroup (A * B) $-> ab_tensor_prod A B
a: A
b: B
w: list (A * B + A * B)
IHw: P (tensor_in (freegroup_eta w))

P (tensor_in (freegroup_eta [inl (a, b)]%list) + tensor_in (freegroup_eta w))
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)
tensor_in:= grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B: FreeGroup (A * B) $-> ab_tensor_prod A B
a: A
b: B
w: list (A * B + A * B)
IHw: P (tensor_in (freegroup_eta w))
P (tensor_in (freegroup_eta [inr (a, b)]%list) + tensor_in (freegroup_eta w))
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)
tensor_in:= grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B: FreeGroup (A * B) $-> ab_tensor_prod A B
a: A
b: B
w: list (A * B + A * B)
IHw: P (tensor_in (freegroup_eta w))

P (tensor_in (freegroup_eta [inl (a, b)]%list) + tensor_in (freegroup_eta w))
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)
tensor_in:= grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B: FreeGroup (A * B) $-> ab_tensor_prod A B
a: A
b: B
w: list (A * B + A * B)
IHw: P (tensor_in (freegroup_eta w))

P (tensor_in (freegroup_in (a, b)) + tensor_in (freegroup_eta w))
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)
tensor_in:= grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B: FreeGroup (A * B) $-> ab_tensor_prod A B
a: A
b: B
w: list (A * B + A * B)
IHw: P (tensor_in (freegroup_eta w))

P (tensor_in (freegroup_in (a, b)))
apply Hin.
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)
tensor_in:= grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B: FreeGroup (A * B) $-> ab_tensor_prod A B
a: A
b: B
w: list (A * B + A * B)
IHw: P (tensor_in (freegroup_eta w))

P (tensor_in (freegroup_eta [inr (a, b)]%list) + tensor_in (freegroup_eta w))
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)
tensor_in:= grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B: FreeGroup (A * B) $-> ab_tensor_prod A B
a: A
b: B
w: list (A * B + A * B)
IHw: P (tensor_in (freegroup_eta w))

P (tensor_in (- freegroup_in (a, b)) + tensor_in (freegroup_eta w))
(* This [rewrite] is reflexivity, but using [change] to achieve this is slow and slows down the Defined line. *)
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)
tensor_in:= grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B: FreeGroup (A * B) $-> ab_tensor_prod A B
a: A
b: B
w: list (A * B + A * B)
IHw: P (tensor_in (freegroup_eta w))

P (- tensor_in (freegroup_in (a, b)) + tensor_in (freegroup_eta w))
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)
tensor_in:= grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B: FreeGroup (A * B) $-> ab_tensor_prod A B
a: A
b: B
w: list (A * B + A * B)
IHw: P (tensor_in (freegroup_eta w))

P (- tensor_in (freegroup_in (a, b)))
A, B: AbGroup
P: ab_tensor_prod A B -> Type
H: forall x : ab_tensor_prod A B, IsHProp (P x)
Hin: forall (a : A) (b : B), P (tensor a b)
Hop: forall x y : ab_tensor_prod A B, P x -> P y -> P (x + y)
tensor_in:= grp_quotient_map $o abel_unit : FreeGroup (A * B) $-> ab_tensor_prod A B: FreeGroup (A * B) $-> ab_tensor_prod A B
a: A
b: B
w: list (A * B + A * B)
IHw: P (tensor_in (freegroup_eta w))

P (tensor (- a) b)
apply Hin. Defined. (** As a commonly occurring special case of the above induction principle, we have the case when the predicate in question is showing that two group homomorphisms out of the tensor product are homotopic. In order to do this, it suffices to show it only for simple tensors. The homotopy is closed under addition, so we don't need to hypothesise anything else. *)
A, B, G: AbGroup
f, f': ab_tensor_prod A B $-> G
H: forall (a : A) (b : B), f (tensor a b) = f' (tensor a b)

f $== f'
A, B, G: AbGroup
f, f': ab_tensor_prod A B $-> G
H: forall (a : A) (b : B), f (tensor a b) = f' (tensor a b)

f $== f'
A, B, G: AbGroup
f, f': ab_tensor_prod A B $-> G
H: forall (a : A) (b : B), f (tensor a b) = f' (tensor a b)

forall x : ab_tensor_prod A B, IsHProp (f x = f' x)
A, B, G: AbGroup
f, f': ab_tensor_prod A B $-> G
H: forall (a : A) (b : B), f (tensor a b) = f' (tensor a b)
forall (a : A) (b : B), f (tensor a b) = f' (tensor a b)
A, B, G: AbGroup
f, f': ab_tensor_prod A B $-> G
H: forall (a : A) (b : B), f (tensor a b) = f' (tensor a b)
forall x y : ab_tensor_prod A B, f x = f' x -> f y = f' y -> f (x + y) = f' (x + y)
A, B, G: AbGroup
f, f': ab_tensor_prod A B $-> G
H: forall (a : A) (b : B), f (tensor a b) = f' (tensor a b)

forall x : ab_tensor_prod A B, IsHProp (f x = f' x)
exact _.
A, B, G: AbGroup
f, f': ab_tensor_prod A B $-> G
H: forall (a : A) (b : B), f (tensor a b) = f' (tensor a b)

forall (a : A) (b : B), f (tensor a b) = f' (tensor a b)
exact H.
A, B, G: AbGroup
f, f': ab_tensor_prod A B $-> G
H: forall (a : A) (b : B), f (tensor a b) = f' (tensor a b)

forall x y : ab_tensor_prod A B, f x = f' x -> f y = f' y -> f (x + y) = f' (x + y)
intros x y; apply grp_homo_op_agree. Defined. (** As an even more specialised case, we occasionally have the second homomorphism being a sum of abelian group homomorphisms. In those cases, it is easier to use this specialised lemma. *) Definition ab_tensor_prod_ind_homotopy_plus {A B G : AbGroup} {f f' f'' : ab_tensor_prod A B $-> G} (H : forall a b, f (tensor a b) = f' (tensor a b) + f'' (tensor a b)) : forall x, f x = f' x + f'' x := ab_tensor_prod_ind_homotopy (f':=f' + f'') H. (** Here we give an induction principle for a triple tensor, a.k.a a dependent trilinear function. *)
A, B, C: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B C) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B C), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C), P (tensor a (tensor b c))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B C), P x -> P y -> P (x + y)

forall x : ab_tensor_prod A (ab_tensor_prod B C), P x
A, B, C: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B C) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B C), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C), P (tensor a (tensor b c))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B C), P x -> P y -> P (x + y)

forall x : ab_tensor_prod A (ab_tensor_prod B C), P x
A, B, C: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B C) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B C), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C), P (tensor a (tensor b c))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B C), P x -> P y -> P (x + y)

forall (a : A) (b : ab_tensor_prod B C), P (tensor a b)
A, B, C: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B C) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B C), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C), P (tensor a (tensor b c))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B C), P x -> P y -> P (x + y)
forall x y : ab_tensor_prod A (ab_tensor_prod B C), P x -> P y -> P (x + y)
A, B, C: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B C) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B C), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C), P (tensor a (tensor b c))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B C), P x -> P y -> P (x + y)

forall (a : A) (b : ab_tensor_prod B C), P (tensor a b)
A, B, C: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B C) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B C), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C), P (tensor a (tensor b c))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B C), P x -> P y -> P (x + y)
a: A

forall b : ab_tensor_prod B C, P (tensor a b)
A, B, C: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B C) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B C), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C), P (tensor a (tensor b c))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B C), P x -> P y -> P (x + y)
a: A

forall (a0 : B) (b : C), P (tensor a (tensor a0 b))
A, B, C: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B C) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B C), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C), P (tensor a (tensor b c))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B C), P x -> P y -> P (x + y)
a: A
forall x y : ab_tensor_prod B C, P (tensor a x) -> P (tensor a y) -> P (tensor a (x + y))
A, B, C: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B C) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B C), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C), P (tensor a (tensor b c))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B C), P x -> P y -> P (x + y)
a: A

forall (a0 : B) (b : C), P (tensor a (tensor a0 b))
napply Hin.
A, B, C: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B C) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B C), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C), P (tensor a (tensor b c))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B C), P x -> P y -> P (x + y)
a: A

forall x y : ab_tensor_prod B C, P (tensor a x) -> P (tensor a y) -> P (tensor a (x + y))
A, B, C: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B C) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B C), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C), P (tensor a (tensor b c))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B C), P x -> P y -> P (x + y)
a: A
x, y: ab_tensor_prod B C
Hx: P (tensor a x)
Hy: P (tensor a y)

P (tensor a (x + y))
A, B, C: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B C) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B C), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C), P (tensor a (tensor b c))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B C), P x -> P y -> P (x + y)
a: A
x, y: ab_tensor_prod B C
Hx: P (tensor a x)
Hy: P (tensor a y)

P (tensor a x + tensor a y)
by apply Hop.
A, B, C: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B C) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B C), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C), P (tensor a (tensor b c))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B C), P x -> P y -> P (x + y)

forall x y : ab_tensor_prod A (ab_tensor_prod B C), P x -> P y -> P (x + y)
exact Hop. Defined. (** Similar to before, we specialise the triple tensor induction principle for proving homotopies of trilinear/triadditive functions. *)
A, B, C, G: AbGroup
f, f': ab_tensor_prod A (ab_tensor_prod B C) $-> G
H: forall (a : A) (b : B) (c : C), f (tensor a (tensor b c)) = f' (tensor a (tensor b c))

f $== f'
A, B, C, G: AbGroup
f, f': ab_tensor_prod A (ab_tensor_prod B C) $-> G
H: forall (a : A) (b : B) (c : C), f (tensor a (tensor b c)) = f' (tensor a (tensor b c))

f $== f'
A, B, C, G: AbGroup
f, f': ab_tensor_prod A (ab_tensor_prod B C) $-> G
H: forall (a : A) (b : B) (c : C), f (tensor a (tensor b c)) = f' (tensor a (tensor b c))

forall x : ab_tensor_prod A (ab_tensor_prod B C), IsHProp (f x = f' x)
A, B, C, G: AbGroup
f, f': ab_tensor_prod A (ab_tensor_prod B C) $-> G
H: forall (a : A) (b : B) (c : C), f (tensor a (tensor b c)) = f' (tensor a (tensor b c))
forall (a : A) (b : B) (c : C), f (tensor a (tensor b c)) = f' (tensor a (tensor b c))
A, B, C, G: AbGroup
f, f': ab_tensor_prod A (ab_tensor_prod B C) $-> G
H: forall (a : A) (b : B) (c : C), f (tensor a (tensor b c)) = f' (tensor a (tensor b c))
forall x y : ab_tensor_prod A (ab_tensor_prod B C), f x = f' x -> f y = f' y -> f (x + y) = f' (x + y)
A, B, C, G: AbGroup
f, f': ab_tensor_prod A (ab_tensor_prod B C) $-> G
H: forall (a : A) (b : B) (c : C), f (tensor a (tensor b c)) = f' (tensor a (tensor b c))

forall x : ab_tensor_prod A (ab_tensor_prod B C), IsHProp (f x = f' x)
exact _.
A, B, C, G: AbGroup
f, f': ab_tensor_prod A (ab_tensor_prod B C) $-> G
H: forall (a : A) (b : B) (c : C), f (tensor a (tensor b c)) = f' (tensor a (tensor b c))

forall (a : A) (b : B) (c : C), f (tensor a (tensor b c)) = f' (tensor a (tensor b c))
exact H.
A, B, C, G: AbGroup
f, f': ab_tensor_prod A (ab_tensor_prod B C) $-> G
H: forall (a : A) (b : B) (c : C), f (tensor a (tensor b c)) = f' (tensor a (tensor b c))

forall x y : ab_tensor_prod A (ab_tensor_prod B C), f x = f' x -> f y = f' y -> f (x + y) = f' (x + y)
intros x y; apply grp_homo_op_agree. Defined. (** As explained for the biadditive and triadditive cases, we also derive an induction principle for quadruple tensors giving us dependent quadrilinear maps. *)
A, B, C, D: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C) (d : D), P (tensor a (tensor b (tensor c d)))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), P x -> P y -> P (x + y)

forall x : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), P x
A, B, C, D: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C) (d : D), P (tensor a (tensor b (tensor c d)))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), P x -> P y -> P (x + y)

forall x : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), P x
A, B, C, D: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C) (d : D), P (tensor a (tensor b (tensor c d)))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), P x -> P y -> P (x + y)

forall (a : A) (b : ab_tensor_prod B (ab_tensor_prod C D)), P (tensor a b)
A, B, C, D: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C) (d : D), P (tensor a (tensor b (tensor c d)))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), P x -> P y -> P (x + y)
forall x y : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), P x -> P y -> P (x + y)
A, B, C, D: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C) (d : D), P (tensor a (tensor b (tensor c d)))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), P x -> P y -> P (x + y)

forall (a : A) (b : ab_tensor_prod B (ab_tensor_prod C D)), P (tensor a b)
A, B, C, D: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C) (d : D), P (tensor a (tensor b (tensor c d)))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), P x -> P y -> P (x + y)
a: A

forall b : ab_tensor_prod B (ab_tensor_prod C D), P (tensor a b)
A, B, C, D: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C) (d : D), P (tensor a (tensor b (tensor c d)))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), P x -> P y -> P (x + y)
a: A

forall x : ab_tensor_prod B (ab_tensor_prod C D), IsHProp (P (tensor a x))
A, B, C, D: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C) (d : D), P (tensor a (tensor b (tensor c d)))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), P x -> P y -> P (x + y)
a: A
forall (a0 : B) (b : C) (c : D), P (tensor a (tensor a0 (tensor b c)))
A, B, C, D: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C) (d : D), P (tensor a (tensor b (tensor c d)))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), P x -> P y -> P (x + y)
a: A
forall x y : ab_tensor_prod B (ab_tensor_prod C D), P (tensor a x) -> P (tensor a y) -> P (tensor a (x + y))
A, B, C, D: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C) (d : D), P (tensor a (tensor b (tensor c d)))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), P x -> P y -> P (x + y)
a: A

forall x : ab_tensor_prod B (ab_tensor_prod C D), IsHProp (P (tensor a x))
intro x; apply H.
A, B, C, D: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C) (d : D), P (tensor a (tensor b (tensor c d)))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), P x -> P y -> P (x + y)
a: A

forall (a0 : B) (b : C) (c : D), P (tensor a (tensor a0 (tensor b c)))
napply Hin.
A, B, C, D: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C) (d : D), P (tensor a (tensor b (tensor c d)))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), P x -> P y -> P (x + y)
a: A

forall x y : ab_tensor_prod B (ab_tensor_prod C D), P (tensor a x) -> P (tensor a y) -> P (tensor a (x + y))
A, B, C, D: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C) (d : D), P (tensor a (tensor b (tensor c d)))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), P x -> P y -> P (x + y)
a: A
x, y: ab_tensor_prod B (ab_tensor_prod C D)
Hx: P (tensor a x)
Hy: P (tensor a y)

P (tensor a (x + y))
A, B, C, D: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C) (d : D), P (tensor a (tensor b (tensor c d)))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), P x -> P y -> P (x + y)
a: A
x, y: ab_tensor_prod B (ab_tensor_prod C D)
Hx: P (tensor a x)
Hy: P (tensor a y)

P (tensor a x + tensor a y)
by apply Hop.
A, B, C, D: AbGroup
P: ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) -> Type
H: forall x : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), IsHProp (P x)
Hin: forall (a : A) (b : B) (c : C) (d : D), P (tensor a (tensor b (tensor c d)))
Hop: forall x y : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), P x -> P y -> P (x + y)

forall x y : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), P x -> P y -> P (x + y)
exact Hop. Defined. (** To construct a homotopy between quadrilinear maps we need only check equality for the quadruple simple tensors. *)
A, B, C, D, G: AbGroup
f, f': ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) $-> G
H: forall (a : A) (b : B) (c : C) (d : D), f (tensor a (tensor b (tensor c d))) = f' (tensor a (tensor b (tensor c d)))

f $== f'
A, B, C, D, G: AbGroup
f, f': ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) $-> G
H: forall (a : A) (b : B) (c : C) (d : D), f (tensor a (tensor b (tensor c d))) = f' (tensor a (tensor b (tensor c d)))

f $== f'
A, B, C, D, G: AbGroup
f, f': ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) $-> G
H: forall (a : A) (b : B) (c : C) (d : D), f (tensor a (tensor b (tensor c d))) = f' (tensor a (tensor b (tensor c d)))

forall x : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), IsHProp (f x = f' x)
A, B, C, D, G: AbGroup
f, f': ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) $-> G
H: forall (a : A) (b : B) (c : C) (d : D), f (tensor a (tensor b (tensor c d))) = f' (tensor a (tensor b (tensor c d)))
forall (a : A) (b : B) (c : C) (d : D), f (tensor a (tensor b (tensor c d))) = f' (tensor a (tensor b (tensor c d)))
A, B, C, D, G: AbGroup
f, f': ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) $-> G
H: forall (a : A) (b : B) (c : C) (d : D), f (tensor a (tensor b (tensor c d))) = f' (tensor a (tensor b (tensor c d)))
forall x y : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), f x = f' x -> f y = f' y -> f (x + y) = f' (x + y)
A, B, C, D, G: AbGroup
f, f': ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) $-> G
H: forall (a : A) (b : B) (c : C) (d : D), f (tensor a (tensor b (tensor c d))) = f' (tensor a (tensor b (tensor c d)))

forall x : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), IsHProp (f x = f' x)
exact _.
A, B, C, D, G: AbGroup
f, f': ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) $-> G
H: forall (a : A) (b : B) (c : C) (d : D), f (tensor a (tensor b (tensor c d))) = f' (tensor a (tensor b (tensor c d)))

forall (a : A) (b : B) (c : C) (d : D), f (tensor a (tensor b (tensor c d))) = f' (tensor a (tensor b (tensor c d)))
exact H.
A, B, C, D, G: AbGroup
f, f': ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)) $-> G
H: forall (a : A) (b : B) (c : C) (d : D), f (tensor a (tensor b (tensor c d))) = f' (tensor a (tensor b (tensor c d)))

forall x y : ab_tensor_prod A (ab_tensor_prod B (ab_tensor_prod C D)), f x = f' x -> f y = f' y -> f (x + y) = f' (x + y)
intros x y; apply grp_homo_op_agree. Defined. (** ** Universal Property of the Tensor Product *) (** A function of two variables is biadditive if it preserves the operation in each variable. *) Class IsBiadditive {A B C : Type} `{SgOp A, SgOp B, SgOp C} (f : A -> B -> C) := { isbiadditive_l :: forall b, IsSemiGroupPreserving (flip f b); isbiadditive_r :: forall a, IsSemiGroupPreserving (f a); }. Definition issig_IsBiadditive {A B C : Type} `{SgOp A, SgOp B, SgOp C} (f : A -> B -> C) : _ <~> IsBiadditive f := ltac:(issig). (** The truncation level of the [IsBiadditive f] predicate is determined by the truncation level of the codomain. This will almost always be a hset. *)
H: Funext
A, B, C: Type
H0: SgOp A
H1: SgOp B
H2: SgOp C
f: A -> B -> C
n: trunc_index
IsTrunc0: IsTrunc n.+1 C

IsTrunc n (IsBiadditive f)
H: Funext
A, B, C: Type
H0: SgOp A
H1: SgOp B
H2: SgOp C
f: A -> B -> C
n: trunc_index
IsTrunc0: IsTrunc n.+1 C

IsTrunc n (IsBiadditive f)
H: Funext
A, B, C: Type
H0: SgOp A
H1: SgOp B
H2: SgOp C
f: A -> B -> C
n: trunc_index
IsTrunc0: IsTrunc n.+1 C

?Goal <~> IsBiadditive f
H: Funext
A, B, C: Type
H0: SgOp A
H1: SgOp B
H2: SgOp C
f: A -> B -> C
n: trunc_index
IsTrunc0: IsTrunc n.+1 C
IsTrunc n ?Goal
H: Funext
A, B, C: Type
H0: SgOp A
H1: SgOp B
H2: SgOp C
f: A -> B -> C
n: trunc_index
IsTrunc0: IsTrunc n.+1 C

IsTrunc n {_ : forall b : B, IsSemiGroupPreserving (flip f b) & forall a : A, IsSemiGroupPreserving (f a)}
H: Funext
A, B, C: Type
H0: SgOp A
H1: SgOp B
H2: SgOp C
f: A -> B -> C
n: trunc_index
IsTrunc0: IsTrunc n.+1 C

IsTrunc n {_ : forall (b : B) (x y : A), flip f b (x + y) = flip f b x + flip f b y & forall (a : A) (x y : B), f a (x + y) = f a x + f a y}
exact _. Defined. (** The simple tensor map is biadditive. *) Instance isbiadditive_tensor (A B : AbGroup) : IsBiadditive (@tensor A B) := {| isbiadditive_l := fun b a a' => tensor_dist_r a a' b; isbiadditive_r := tensor_dist_l; |}. (** The type of biadditive maps. *) Record Biadditive (A B C : Type) `{SgOp A, SgOp B, SgOp C} := { biadditive_fun :> A -> B -> C; biadditive_isbiadditive :: IsBiadditive biadditive_fun; }. Definition issig_Biadditive {A B C : Type} `{SgOp A, SgOp B, SgOp C} : _ <~> Biadditive A B C := ltac:(issig).
A, B, C: AbGroup

(ab_tensor_prod A B $-> C) -> Biadditive A B C
A, B, C: AbGroup

(ab_tensor_prod A B $-> C) -> Biadditive A B C
A, B, C: AbGroup
f: ab_tensor_prod A B $-> C

Biadditive A B C
A, B, C: AbGroup
f: ab_tensor_prod A B $-> C

IsBiadditive (fun (x : A) (y : B) => f (tensor x y))
A, B, C: AbGroup
f: ab_tensor_prod A B $-> C

forall b : B, IsSemiGroupPreserving (flip (fun (x : A) (y : B) => f (tensor x y)) b)
A, B, C: AbGroup
f: ab_tensor_prod A B $-> C
forall a : A, IsSemiGroupPreserving ((fun (x : A) (y : B) => f (tensor x y)) a)
A, B, C: AbGroup
f: ab_tensor_prod A B $-> C

forall b : B, IsSemiGroupPreserving (flip (fun (x : A) (y : B) => f (tensor x y)) b)
A, B, C: AbGroup
f: ab_tensor_prod A B $-> C
b: B
a, a': A

f (tensor (a + a') b) = f (tensor a b) + f (tensor a' b)
A, B, C: AbGroup
f: ab_tensor_prod A B $-> C
b: B
a, a': A

tensor (a + a') b = ?Goal
A, B, C: AbGroup
f: ab_tensor_prod A B $-> C
b: B
a, a': A
f ?Goal = f (tensor a b) + f (tensor a' b)
A, B, C: AbGroup
f: ab_tensor_prod A B $-> C
b: B
a, a': A

f (tensor a b + tensor a' b) = f (tensor a b) + f (tensor a' b)
napply grp_homo_op.
A, B, C: AbGroup
f: ab_tensor_prod A B $-> C

forall a : A, IsSemiGroupPreserving ((fun (x : A) (y : B) => f (tensor x y)) a)
A, B, C: AbGroup
f: ab_tensor_prod A B $-> C
a: A
a', b: B

f (tensor a (a' + b)) = f (tensor a a') + f (tensor a b)
A, B, C: AbGroup
f: ab_tensor_prod A B $-> C
a: A
a', b: B

tensor a (a' + b) = ?Goal
A, B, C: AbGroup
f: ab_tensor_prod A B $-> C
a: A
a', b: B
f ?Goal = f (tensor a a') + f (tensor a b)
A, B, C: AbGroup
f: ab_tensor_prod A B $-> C
a: A
a', b: B

f (tensor a a' + tensor a b) = f (tensor a a') + f (tensor a b)
napply grp_homo_op. Defined. (** The universal property of the tensor product is that biadditive maps between abelian groups are in one-to-one correspondence with maps out of the tensor product. In this sense, the tensor product is the most perfect object describing biadditive maps between two abelian groups. *)
H: Funext
A, B, C: AbGroup

Biadditive A B C <~> (ab_tensor_prod A B $-> C)
H: Funext
A, B, C: AbGroup

Biadditive A B C <~> (ab_tensor_prod A B $-> C)
H: Funext
A, B, C: AbGroup

Biadditive A B C -> ab_tensor_prod A B $-> C
H: Funext
A, B, C: AbGroup
(ab_tensor_prod A B $-> C) -> Biadditive A B C
H: Funext
A, B, C: AbGroup
?f o ?g == idmap
H: Funext
A, B, C: AbGroup
?g o ?f == idmap
H: Funext
A, B, C: AbGroup

Biadditive A B C -> ab_tensor_prod A B $-> C
H: Funext
A, B, C: AbGroup
f: A -> B -> C
l: forall b : B, IsSemiGroupPreserving (flip f b)
r: forall a : A, IsSemiGroupPreserving (f a)

ab_tensor_prod A B $-> C
exact (ab_tensor_prod_rec f r (fun a a' b => l b a a')).
H: Funext
A, B, C: AbGroup

(ab_tensor_prod A B $-> C) -> Biadditive A B C
snapply biadditive_ab_tensor_prod.
H: Funext
A, B, C: AbGroup

(fun X : Biadditive A B C => (fun (f : A -> B -> C) (biadditive_isbiadditive0 : IsBiadditive f) => (fun (l : forall b : B, IsSemiGroupPreserving (flip f b)) (r : forall a : A, IsSemiGroupPreserving (f a)) => ab_tensor_prod_rec f r (fun (a a' : A) (b : B) => l b a a')) isbiadditive_l isbiadditive_r) X (biadditive_isbiadditive A B C X)) o biadditive_ab_tensor_prod == idmap
H: Funext
A, B, C: AbGroup
f: ab_tensor_prod A B $-> C

ab_tensor_prod_rec (biadditive_ab_tensor_prod f) isbiadditive_r (fun (a a' : A) (b : B) => isbiadditive_l b a a') = f
H: Funext
A, B, C: AbGroup
f: ab_tensor_prod A B $-> C

ab_tensor_prod_rec (biadditive_ab_tensor_prod f) isbiadditive_r (fun (a a' : A) (b : B) => isbiadditive_l b a a') == f
H: Funext
A, B, C: AbGroup
f: ab_tensor_prod A B $-> C

forall (a : A) (b : B), ab_tensor_prod_rec (biadditive_ab_tensor_prod f) isbiadditive_r (fun (a0 a' : A) (b0 : B) => isbiadditive_l b0 a0 a') (tensor a b) = f (tensor a b)
H: Funext
A, B, C: AbGroup
f: ab_tensor_prod A B $-> C
a: A
b: B

f (tensor a b) = f (tensor a b)
reflexivity.
H: Funext
A, B, C: AbGroup

biadditive_ab_tensor_prod o (fun X : Biadditive A B C => (fun (f : A -> B -> C) (biadditive_isbiadditive0 : IsBiadditive f) => (fun (l : forall b : B, IsSemiGroupPreserving (flip f b)) (r : forall a : A, IsSemiGroupPreserving (f a)) => ab_tensor_prod_rec f r (fun (a a' : A) (b : B) => l b a a')) isbiadditive_l isbiadditive_r) X (biadditive_isbiadditive A B C X)) == idmap
H: Funext
A, B, C: AbGroup
f: A -> B -> C
l: forall b : B, IsSemiGroupPreserving (flip f b)
r: forall a : A, IsSemiGroupPreserving (f a)

biadditive_ab_tensor_prod (ab_tensor_prod_rec f r (fun (a a' : A) (b : B) => l b a a')) = {| biadditive_fun := f; biadditive_isbiadditive := {| isbiadditive_l := l; isbiadditive_r := r |} |}
H: Funext
A, B, C: AbGroup
f: A -> B -> C
l: forall b : B, IsSemiGroupPreserving (flip f b)
r: forall a : A, IsSemiGroupPreserving (f a)

issig_Biadditive^-1 (biadditive_ab_tensor_prod (ab_tensor_prod_rec f r (fun (a a' : A) (b : B) => l b a a'))) = issig_Biadditive^-1 {| biadditive_fun := f; biadditive_isbiadditive := {| isbiadditive_l := l; isbiadditive_r := r |} |}
H: Funext
A, B, C: AbGroup
f: A -> B -> C
l: forall b : B, IsSemiGroupPreserving (flip f b)
r: forall a : A, IsSemiGroupPreserving (f a)

(fun (x : A) (y : B) => f x y) = f
reflexivity. Defined. (** ** Functoriality of the Tensor Product *) (** The tensor product produces a bifunctor and we will later show that it gives a symmetric monoidal structure on the category of abelian groups. *) (** Given a pair of maps, we can produce a homomorphism between the pairwise tensor products of the domains and codomains. *)
A, B, A', B': AbGroup
f: A $-> A'
g: B $-> B'

ab_tensor_prod A B $-> ab_tensor_prod A' B'
A, B, A', B': AbGroup
f: A $-> A'
g: B $-> B'

ab_tensor_prod A B $-> ab_tensor_prod A' B'
A, B, A', B': AbGroup
f: A $-> A'
g: B $-> B'

A -> B $-> ab_tensor_prod A' B'
A, B, A', B': AbGroup
f: A $-> A'
g: B $-> B'
forall (a a' : A) (b : B), ?f (a + a') b = ?f a b + ?f a' b
A, B, A', B': AbGroup
f: A $-> A'
g: B $-> B'

A -> B $-> ab_tensor_prod A' B'
A, B, A', B': AbGroup
f: A $-> A'
g: B $-> B'
a: A

B $-> ab_tensor_prod A' B'
exact (grp_homo_tensor_l (f a) $o g).
A, B, A', B': AbGroup
f: A $-> A'
g: B $-> B'

forall (a a' : A) (b : B), (fun a0 : A => grp_homo_tensor_l (f a0) $o g) (a + a') b = (fun a0 : A => grp_homo_tensor_l (f a0) $o g) a b + (fun a0 : A => grp_homo_tensor_l (f a0) $o g) a' b
A, B, A', B': AbGroup
f: A $-> A'
g: B $-> B'
a, a': A
b: B

(grp_homo_tensor_l (f (a + a')) $o g) b = (grp_homo_tensor_l (f a) $o g) b + (grp_homo_tensor_l (f a') $o g) b
A, B, A', B': AbGroup
f: A $-> A'
g: B $-> B'
a, a': A
b: B

(grp_homo_tensor_l (f a + f a') $o g) b = (grp_homo_tensor_l (f a) $o g) b + (grp_homo_tensor_l (f a') $o g) b
napply tensor_dist_r. Defined. (** 2-functoriality of the tensor product. *)
A, B, A', B': AbGroup
f, f': A $-> A'
p: f $== f'
g, g': B $-> B'
q: g $== g'

functor_ab_tensor_prod f g $== functor_ab_tensor_prod f' g'
A, B, A', B': AbGroup
f, f': A $-> A'
p: f $== f'
g, g': B $-> B'
q: g $== g'

functor_ab_tensor_prod f g $== functor_ab_tensor_prod f' g'
A, B, A', B': AbGroup
f, f': A $-> A'
p: f $== f'
g, g': B $-> B'
q: g $== g'

forall (a : A) (b : B), functor_ab_tensor_prod f g (tensor a b) = functor_ab_tensor_prod f' g' (tensor a b)
A, B, A', B': AbGroup
f, f': A $-> A'
p: f $== f'
g, g': B $-> B'
q: g $== g'
a: A
b: B

tensor (f a) (g b) = tensor (f' a) (g' b)
exact (ap011 tensor (p _) (q _)). Defined. (** The tensor product functor preserves identity morphisms. *)
A, B: AbGroup

functor_ab_tensor_prod (Id A) (Id B) $== Id (ab_tensor_prod A B)
A, B: AbGroup

functor_ab_tensor_prod (Id A) (Id B) $== Id (ab_tensor_prod A B)
A, B: AbGroup

forall (a : A) (b : B), functor_ab_tensor_prod (Id A) (Id B) (tensor a b) = Id (ab_tensor_prod A B) (tensor a b)
A, B: AbGroup
a: A
b: B

tensor a b = tensor a b
reflexivity. Defined. (** The tensor product functor preserves composition. *)
A, B, C, A', B', C': AbGroup
f: A $-> B
g: B $-> C
f': A' $-> B'
g': B' $-> C'

functor_ab_tensor_prod (g $o f) (g' $o f') $== functor_ab_tensor_prod g g' $o functor_ab_tensor_prod f f'
A, B, C, A', B', C': AbGroup
f: A $-> B
g: B $-> C
f': A' $-> B'
g': B' $-> C'

functor_ab_tensor_prod (g $o f) (g' $o f') $== functor_ab_tensor_prod g g' $o functor_ab_tensor_prod f f'
A, B, C, A', B', C': AbGroup
f: A $-> B
g: B $-> C
f': A' $-> B'
g': B' $-> C'

forall (a : A) (b : A'), functor_ab_tensor_prod (g $o f) (g' $o f') (tensor a b) = (functor_ab_tensor_prod g g' $o functor_ab_tensor_prod f f') (tensor a b)
A, B, C, A', B', C': AbGroup
f: A $-> B
g: B $-> C
f': A' $-> B'
g': B' $-> C'
a: A
b: A'

tensor (g (f a)) (g' (f' b)) = tensor (g (f a)) (g' (f' b))
reflexivity. Defined. (** The tensor product functor is a 0-bifunctor. *)

Is0Bifunctor ab_tensor_prod

Is0Bifunctor ab_tensor_prod

Is0Functor (uncurry ab_tensor_prod)

forall a b : AbGroup * AbGroup, (a $-> b) -> uncurry ab_tensor_prod a $-> uncurry ab_tensor_prod b
A, B, A', B': AbGroup
f: fst (A, B) $-> fst (A', B')
g: snd (A, B) $-> snd (A', B')

uncurry ab_tensor_prod (A, B) $-> uncurry ab_tensor_prod (A', B')
exact (functor_ab_tensor_prod f g). Defined. (** The tensor product functor is a bifunctor. *)

Is1Bifunctor ab_tensor_prod

Is1Bifunctor ab_tensor_prod

Is1Functor (uncurry ab_tensor_prod)

forall (a b : AbGroup * AbGroup) (f g : a $-> b), f $== g -> fmap (uncurry ab_tensor_prod) f $== fmap (uncurry ab_tensor_prod) g

forall a : AbGroup * AbGroup, fmap (uncurry ab_tensor_prod) (Id a) $== Id (uncurry ab_tensor_prod a)

forall (a b c : AbGroup * AbGroup) (f : a $-> b) (g : b $-> c), fmap (uncurry ab_tensor_prod) (g $o f) $== fmap (uncurry ab_tensor_prod) g $o fmap (uncurry ab_tensor_prod) f

forall (a b : AbGroup * AbGroup) (f g : a $-> b), f $== g -> fmap (uncurry ab_tensor_prod) f $== fmap (uncurry ab_tensor_prod) g
AB, A'B': AbGroup * AbGroup
fg, f'g': AB $-> A'B'
p: fst fg $-> fst f'g'
q: snd fg $-> snd f'g'

fmap (uncurry ab_tensor_prod) fg $== fmap (uncurry ab_tensor_prod) f'g'
exact (functor2_ab_tensor_prod p q).

forall a : AbGroup * AbGroup, fmap (uncurry ab_tensor_prod) (Id a) $== Id (uncurry ab_tensor_prod a)
A, B: AbGroup

fmap (uncurry ab_tensor_prod) (Id (A, B)) $== Id (uncurry ab_tensor_prod (A, B))
exact (functor_ab_tensor_prod_id A B).

forall (a b c : AbGroup * AbGroup) (f : a $-> b) (g : b $-> c), fmap (uncurry ab_tensor_prod) (g $o f) $== fmap (uncurry ab_tensor_prod) g $o fmap (uncurry ab_tensor_prod) f
AA', BB', CC': AbGroup * AbGroup
f: fst AA' $-> fst BB'
g: snd AA' $-> snd BB'
f': fst BB' $-> fst CC'
g': snd BB' $-> snd CC'

fmap (uncurry ab_tensor_prod) ((f', g') $o (f, g)) $== fmap (uncurry ab_tensor_prod) (f', g') $o fmap (uncurry ab_tensor_prod) (f, g)
exact (functor_ab_tensor_prod_compose f f' g g'). Defined. (** ** Symmetry of the Tensor Product *) (** The tensor product is symmetric in that the order in which we take the tensor shouldn't matter up to isomorphism. *) (** We can define a swap map which swaps the order of simple tensors. *)
A, B: AbGroup

ab_tensor_prod A B $-> ab_tensor_prod B A
A, B: AbGroup

ab_tensor_prod A B $-> ab_tensor_prod B A
A, B: AbGroup

A -> B -> ab_tensor_prod B A
A, B: AbGroup
forall (a : A) (b b' : B), ?f a (b + b') = ?f a b + ?f a b'
A, B: AbGroup
forall (a a' : A) (b : B), ?f (a + a') b = ?f a b + ?f a' b
A, B: AbGroup

A -> B -> ab_tensor_prod B A
exact (flip tensor).
A, B: AbGroup

forall (a : A) (b b' : B), flip tensor a (b + b') = flip tensor a b + flip tensor a b'
A, B: AbGroup
a: A
b, b': B

flip tensor a (b + b') = flip tensor a b + flip tensor a b'
apply tensor_dist_r.
A, B: AbGroup

forall (a a' : A) (b : B), flip tensor (a + a') b = flip tensor a b + flip tensor a' b
A, B: AbGroup
a, a': A
b: B

flip tensor (a + a') b = flip tensor a b + flip tensor a' b
apply tensor_dist_l. Defined. (** [ab_tensor_swap] is involutive. *)
A, B: AbGroup

ab_tensor_swap $o ab_tensor_swap $== Id (ab_tensor_prod A B)
A, B: AbGroup

ab_tensor_swap $o ab_tensor_swap $== Id (ab_tensor_prod A B)
A, B: AbGroup

forall (a : A) (b : B), (ab_tensor_swap $o ab_tensor_swap) (tensor a b) = Id (ab_tensor_prod A B) (tensor a b)
reflexivity. Defined. (** [ab_tensor_swap] is natural in both arguments. This means that it also acts on tensor functors. *)
A, B, A', B': AbGroup
f: A $-> A'
g: B $-> B'

ab_tensor_swap $o functor_ab_tensor_prod f g $== functor_ab_tensor_prod g f $o ab_tensor_swap
A, B, A', B': AbGroup
f: A $-> A'
g: B $-> B'

ab_tensor_swap $o functor_ab_tensor_prod f g $== functor_ab_tensor_prod g f $o ab_tensor_swap
A, B, A', B': AbGroup
f: A $-> A'
g: B $-> B'

forall (a : A) (b : B), (ab_tensor_swap $o functor_ab_tensor_prod f g) (tensor a b) = (functor_ab_tensor_prod g f $o ab_tensor_swap) (tensor a b)
A, B, A', B': AbGroup
f: A $-> A'
g: B $-> B'

forall (a : A) (b : B), tensor (g b) (f a) = tensor (g b) (f a)
reflexivity. Defined. (** The swap map gives us a symmetric braiding on the category of abelian groups. We will later show it is a full symmetric monoidal category. *)

SymmetricBraiding ab_tensor_prod

SymmetricBraiding ab_tensor_prod

Braiding ab_tensor_prod

forall a b : AbGroup, ?braiding_symmetricbraiding a b $o ?braiding_symmetricbraiding b a $== Id (ab_tensor_prod b a)

Braiding ab_tensor_prod

uncurry ab_tensor_prod $=> uncurry (flip ab_tensor_prod)

Is1Natural (uncurry ab_tensor_prod) (uncurry (flip ab_tensor_prod)) ?alpha

uncurry ab_tensor_prod $=> uncurry (flip ab_tensor_prod)
intro; exact ab_tensor_swap.

Is1Natural (uncurry ab_tensor_prod) (uncurry (flip ab_tensor_prod)) ((fun a : AbGroup * AbGroup => ab_tensor_swap) : uncurry ab_tensor_prod $=> uncurry (flip ab_tensor_prod))

forall (a a' : AbGroup * AbGroup) (f : a $-> a'), (fun a0 : AbGroup * AbGroup => ab_tensor_swap) a' $o fmap (uncurry ab_tensor_prod) f $== fmap (uncurry (flip ab_tensor_prod)) f $o (fun a0 : AbGroup * AbGroup => ab_tensor_swap) a
intros; napply ab_tensor_swap_natural.

forall a b : AbGroup, {| trans_nattrans := (fun a0 : AbGroup * AbGroup => ab_tensor_swap) : uncurry ab_tensor_prod $=> uncurry (flip ab_tensor_prod); is1natural_nattrans := Build_Is1Natural (fun a0 : AbGroup * AbGroup => ab_tensor_swap) (fun (a0 a' : AbGroup * AbGroup) (f : a0 $-> a') => ab_tensor_swap_natural (fst f) (snd f)) |} a b $o {| trans_nattrans := (fun a0 : AbGroup * AbGroup => ab_tensor_swap) : uncurry ab_tensor_prod $=> uncurry (flip ab_tensor_prod); is1natural_nattrans := Build_Is1Natural (fun a0 : AbGroup * AbGroup => ab_tensor_swap) (fun (a0 a' : AbGroup * AbGroup) (f : a0 $-> a') => ab_tensor_swap_natural (fst f) (snd f)) |} b a $== Id (ab_tensor_prod b a)
intros; napply ab_tensor_swap_swap. Defined. (** ** Twisting Triple Tensors *) (** In order to construct the symmetric monoidal category, we will use what is termed the "Twist construction" in Monoidal.v. This simplifies the data of a symmetric monoidal category by constructing it from simpler parts. For instance, instead of having to prove full associativity [(A ⊗ B) ⊗ C $-> A ⊗ (B ⊗ C)], we can provide a twist map [A ⊗ (B ⊗ C) $-> B ⊗ (A ⊗ C)] and use the symmetric braiding we have so far to prove associativity. *) (** In order to be more efficient whilst unfolding definitions, we break up the definition of a twist map into its components. *)
A, B, C: AbGroup

A -> ab_tensor_prod B C $-> ab_tensor_prod B (ab_tensor_prod A C)
A, B, C: AbGroup

A -> ab_tensor_prod B C $-> ab_tensor_prod B (ab_tensor_prod A C)
A, B, C: AbGroup
a: A

ab_tensor_prod B C $-> ab_tensor_prod B (ab_tensor_prod A C)
A, B, C: AbGroup
a: A

B -> C $-> ab_tensor_prod B (ab_tensor_prod A C)
A, B, C: AbGroup
a: A
forall (a0 a' : B) (b : C), ?f (a0 + a') b = ?f a0 b + ?f a' b
A, B, C: AbGroup
a: A

B -> C $-> ab_tensor_prod B (ab_tensor_prod A C)
A, B, C: AbGroup
a: A
b: B

C $-> ab_tensor_prod B (ab_tensor_prod A C)
exact (grp_homo_tensor_l b $o grp_homo_tensor_l a).
A, B, C: AbGroup
a: A

forall (a0 a' : B) (b : C), (fun b0 : B => grp_homo_tensor_l b0 $o grp_homo_tensor_l a) (a0 + a') b = (fun b0 : B => grp_homo_tensor_l b0 $o grp_homo_tensor_l a) a0 b + (fun b0 : B => grp_homo_tensor_l b0 $o grp_homo_tensor_l a) a' b
A, B, C: AbGroup
a: A
b, b': B
c: C

(grp_homo_tensor_l (b + b') $o grp_homo_tensor_l a) c = (grp_homo_tensor_l b $o grp_homo_tensor_l a) c + (grp_homo_tensor_l b' $o grp_homo_tensor_l a) c
napply tensor_dist_r. Defined.
A, B, C: AbGroup
a, a': A
b: ab_tensor_prod B C

ab_tensor_prod_twist_map (a + a') b = ab_tensor_prod_twist_map a b + ab_tensor_prod_twist_map a' b
A, B, C: AbGroup
a, a': A
b: ab_tensor_prod B C

ab_tensor_prod_twist_map (a + a') b = ab_tensor_prod_twist_map a b + ab_tensor_prod_twist_map a' b
A, B, C: AbGroup
a, a': A

forall b : ab_tensor_prod B C, ab_tensor_prod_twist_map (a + a') b = ab_tensor_prod_twist_map a b + ab_tensor_prod_twist_map a' b
A, B, C: AbGroup
a, a': A

forall (a0 : B) (b : C), ab_tensor_prod_twist_map (a + a') (tensor a0 b) = ab_tensor_prod_twist_map a (tensor a0 b) + ab_tensor_prod_twist_map a' (tensor a0 b)
A, B, C: AbGroup
a, a': A
b: B
c: C

ab_tensor_prod_twist_map (a + a') (tensor b c) = ab_tensor_prod_twist_map a (tensor b c) + ab_tensor_prod_twist_map a' (tensor b c)
A, B, C: AbGroup
a, a': A
b: B
c: C

tensor b (tensor (a + a') c) = tensor b (tensor a c) + tensor b (tensor a' c)
A, B, C: AbGroup
a, a': A
b: B
c: C

tensor b (tensor (a + a') c) = tensor b (tensor a c + tensor a' c)
A, B, C: AbGroup
a, a': A
b: B
c: C

tensor (a + a') c = tensor a c + tensor a' c
napply tensor_dist_r. Defined. (** Given a triple tensor product, we have a twist map which permutes the first two components. *)
A, B, C: AbGroup

ab_tensor_prod A (ab_tensor_prod B C) $-> ab_tensor_prod B (ab_tensor_prod A C)
A, B, C: AbGroup

ab_tensor_prod A (ab_tensor_prod B C) $-> ab_tensor_prod B (ab_tensor_prod A C)
A, B, C: AbGroup

A -> ab_tensor_prod B C $-> ab_tensor_prod B (ab_tensor_prod A C)
A, B, C: AbGroup
forall (a a' : A) (b : ab_tensor_prod B C), ?f (a + a') b = ?f a b + ?f a' b
A, B, C: AbGroup

A -> ab_tensor_prod B C $-> ab_tensor_prod B (ab_tensor_prod A C)
exact ab_tensor_prod_twist_map.
A, B, C: AbGroup

forall (a a' : A) (b : ab_tensor_prod B C), ab_tensor_prod_twist_map (a + a') b = ab_tensor_prod_twist_map a b + ab_tensor_prod_twist_map a' b
exact ab_tensor_prod_twist_map_additive_l. Defined. (** The twist map is involutive. *)
A, B, C: AbGroup

ab_tensor_prod_twist $o ab_tensor_prod_twist $== Id (ab_tensor_prod A (ab_tensor_prod B C))
A, B, C: AbGroup

ab_tensor_prod_twist $o ab_tensor_prod_twist $== Id (ab_tensor_prod A (ab_tensor_prod B C))
A, B, C: AbGroup

forall (a : A) (b : B) (c : C), (ab_tensor_prod_twist $o ab_tensor_prod_twist) (tensor a (tensor b c)) = Id (ab_tensor_prod A (ab_tensor_prod B C)) (tensor a (tensor b c))
reflexivity. Defined. (** The twist map is natural in all 3 arguments. This means that the twist map acts on the triple tensor functor in the same way. *)
A, B, C, A', B', C': AbGroup
f: A $-> A'
g: B $-> B'
h: C $-> C'

ab_tensor_prod_twist $o fmap11 ab_tensor_prod f (fmap11 ab_tensor_prod g h) $== fmap11 ab_tensor_prod g (fmap11 ab_tensor_prod f h) $o ab_tensor_prod_twist
A, B, C, A', B', C': AbGroup
f: A $-> A'
g: B $-> B'
h: C $-> C'

ab_tensor_prod_twist $o fmap11 ab_tensor_prod f (fmap11 ab_tensor_prod g h) $== fmap11 ab_tensor_prod g (fmap11 ab_tensor_prod f h) $o ab_tensor_prod_twist
A, B, C, A', B', C': AbGroup
f: A $-> A'
g: B $-> B'
h: C $-> C'

forall (a : A) (b : B) (c : C), (ab_tensor_prod_twist $o fmap11 ab_tensor_prod f (fmap11 ab_tensor_prod g h)) (tensor a (tensor b c)) = (fmap11 ab_tensor_prod g (fmap11 ab_tensor_prod f h) $o ab_tensor_prod_twist) (tensor a (tensor b c))
A, B, C, A', B', C': AbGroup
f: A $-> A'
g: B $-> B'
h: C $-> C'
a: A
b: B
c: C

(ab_tensor_prod_twist $o fmap11 ab_tensor_prod f (fmap11 ab_tensor_prod g h)) (tensor a (tensor b c)) = (fmap11 ab_tensor_prod g (fmap11 ab_tensor_prod f h) $o ab_tensor_prod_twist) (tensor a (tensor b c))
(* This [change] speeds up the [reflexivity]. [simpl] produces a goal that looks the same, but is still slow. *)
A, B, C, A', B', C': AbGroup
f: A $-> A'
g: B $-> B'
h: C $-> C'
a: A
b: B
c: C

tensor (g b) (tensor (f a) (h c)) = tensor (g b) (tensor (f a) (h c))
reflexivity. Defined. (** ** Unitality of [abgroup_Z] *) (** In the symmetric monoidal structure on abelian groups, [abgroup_Z] is the unit. We show that tensoring with [abgroup_Z] on the right is isomorphic to the original group. *) (** First we characterise the action of integers via [grp_pow] and their interaction on tensors. This is just a generalisation of the distributivity laws for tensors. *) (** Multiplication in the first factor can be factored out. *) Definition tensor_ab_mul_l {A B : AbGroup} (z : Int) (a : A) (b : B) : tensor (ab_mul z a) b = ab_mul z (tensor a b) := ab_mul_natural (grp_homo_tensor_r b) z a. (** Multiplication in the second factor can be factored out. *) Definition tensor_ab_mul_r {A B : AbGroup} (z : Int) (a : A) (b : B) : tensor a (ab_mul z b) = ab_mul z (tensor a b) := ab_mul_natural (grp_homo_tensor_l a) z b. (** Multiplication can be transferred from one factor to the other. The tensor product of [R]-modules will include this as an extra axiom, but here we have [Z]-modules and we can prove it. *)
A, B: AbGroup
z: Int
a: A
b: B

tensor (ab_mul z a) b = tensor a (ab_mul z b)
A, B: AbGroup
z: Int
a: A
b: B

tensor (ab_mul z a) b = tensor a (ab_mul z b)
A, B: AbGroup
z: Int
a: A
b: B

tensor (ab_mul z a) b = ab_mul z (tensor a b)
napply tensor_ab_mul_l. Defined. (** [abgroup_Z] is a right identity for the tensor product. *)
A: AbGroup

ab_tensor_prod A abgroup_Z $<~> A
A: AbGroup

ab_tensor_prod A abgroup_Z $<~> A
(** Checking that the inverse map is a homomorphism is easier. *)
A: AbGroup

A $<~> ab_tensor_prod A abgroup_Z
A: AbGroup

GroupHomomorphism A (ab_tensor_prod A abgroup_Z)
A: AbGroup
IsEquiv ?grp_iso_homo
A: AbGroup

GroupHomomorphism A (ab_tensor_prod A abgroup_Z)
A: AbGroup

abgroup_Z
exact 1%int.
A: AbGroup

IsEquiv (grp_homo_tensor_r 1%int)
A: AbGroup

ab_tensor_prod A abgroup_Z -> A
A: AbGroup
grp_homo_tensor_r 1%int o ?g == idmap
A: AbGroup
?g o grp_homo_tensor_r 1%int == idmap
A: AbGroup

ab_tensor_prod A abgroup_Z -> A
A: AbGroup

A -> abgroup_Z $-> A
A: AbGroup
forall (a a' : A) (b : abgroup_Z), ?f (a + a') b = ?f a b + ?f a' b
A: AbGroup

A -> abgroup_Z $-> A
exact grp_pow_homo.
A: AbGroup

forall (a a' : A) (b : abgroup_Z), grp_pow_homo (a + a') b = grp_pow_homo a b + grp_pow_homo a' b
A: AbGroup
a, a': A
z: abgroup_Z

grp_pow_homo (a + a') z = grp_pow_homo a z + grp_pow_homo a' z
napply (grp_homo_op (ab_mul z)).
A: AbGroup

grp_homo_tensor_r 1%int o ab_tensor_prod_rec' grp_pow_homo (fun (a a' : A) (z : abgroup_Z) => grp_homo_op (ab_mul z) a a' : grp_pow_homo (a + a') z = grp_pow_homo a z + grp_pow_homo a' z) == idmap
A: AbGroup

forall x : ab_tensor_prod A abgroup_Z, grp_homo_tensor_r 1%int (ab_tensor_prod_rec' grp_pow_homo (fun (a a' : A) (z : abgroup_Z) => grp_homo_op (ab_mul z) a a') x) = x
A: AbGroup

grp_homo_tensor_r 1%int $o ab_tensor_prod_rec' grp_pow_homo (fun (a a' : A) (z : abgroup_Z) => grp_homo_op (ab_mul z) a a') $== Id (ab_tensor_prod A abgroup_Z)
A: AbGroup

forall (a : A) (b : abgroup_Z), (grp_homo_tensor_r 1%int $o ab_tensor_prod_rec' grp_pow_homo (fun (a0 a' : A) (z : abgroup_Z) => grp_homo_op (ab_mul z) a0 a')) (tensor a b) = Id (ab_tensor_prod A abgroup_Z) (tensor a b)
A: AbGroup
a: A
z: abgroup_Z

(grp_homo_tensor_r 1%int $o ab_tensor_prod_rec' grp_pow_homo (fun (a a' : A) (z : abgroup_Z) => grp_homo_op (ab_mul z) a a')) (tensor a z) = Id (ab_tensor_prod A abgroup_Z) (tensor a z)
A: AbGroup
a: A
z: abgroup_Z

tensor (grp_pow a z) 1%int = tensor a z
A: AbGroup
a: A
z: abgroup_Z

tensor a (ab_mul z 1%int) = tensor a z
A: AbGroup
a: A
z: abgroup_Z

ab_mul z 1%int = z
A: AbGroup
a: A
z: abgroup_Z

(z * 1)%int = z
apply int_mul_1_r.
A: AbGroup

ab_tensor_prod_rec' grp_pow_homo (fun (a a' : A) (z : abgroup_Z) => grp_homo_op (ab_mul z) a a' : grp_pow_homo (a + a') z = grp_pow_homo a z + grp_pow_homo a' z) o grp_homo_tensor_r 1%int == idmap
exact grp_unit_r. Defined. (** We have a right unitor for the tensor product given by unit [abgroup_Z]. Naturality of [ab_tensor_prod_Z_r] is straightforward to prove. *)

RightUnitor ab_tensor_prod abgroup_Z

RightUnitor ab_tensor_prod abgroup_Z

forall a : AbGroup, flip ab_tensor_prod abgroup_Z a $<~> idmap a

Is1Natural (flip ab_tensor_prod abgroup_Z) idmap (fun a : AbGroup => ?e a)

forall a : AbGroup, flip ab_tensor_prod abgroup_Z a $<~> idmap a
A: AbGroup

flip ab_tensor_prod abgroup_Z A $<~> idmap A
apply ab_tensor_prod_Z_r.

Is1Natural (flip ab_tensor_prod abgroup_Z) idmap (fun a : AbGroup => (fun A : AbGroup => ab_tensor_prod_Z_r) a)

forall (a a' : AbGroup) (f : a $-> a'), (fun a0 : AbGroup => cate_fun ((fun A : AbGroup => ab_tensor_prod_Z_r) a0)) a' $o fmap (flip ab_tensor_prod abgroup_Z) f $== fmap idmap f $o (fun a0 : AbGroup => cate_fun ((fun A : AbGroup => ab_tensor_prod_Z_r) a0)) a
A, A': AbGroup
f: A $-> A'

(fun a : AbGroup => cate_fun ((fun A : AbGroup => ab_tensor_prod_Z_r) a)) A' $o fmap (flip ab_tensor_prod abgroup_Z) f $== fmap idmap f $o (fun a : AbGroup => cate_fun ((fun A : AbGroup => ab_tensor_prod_Z_r) a)) A
A, A': AbGroup
f: A $-> A'

forall (a : A) (b : abgroup_Z), ((fun a0 : AbGroup => cate_fun ((fun A : AbGroup => ab_tensor_prod_Z_r) a0)) A' $o fmap (flip ab_tensor_prod abgroup_Z) f) (tensor a b) = (fmap idmap f $o (fun a0 : AbGroup => cate_fun ((fun A : AbGroup => ab_tensor_prod_Z_r) a0)) A) (tensor a b)
A, A': AbGroup
f: A $-> A'
a: A
z: abgroup_Z

(fmap idmap f $o (fun a : AbGroup => cate_fun ((fun A : AbGroup => ab_tensor_prod_Z_r) a)) A) (tensor a z) = ((fun a : AbGroup => cate_fun ((fun A : AbGroup => ab_tensor_prod_Z_r) a)) A' $o fmap (flip ab_tensor_prod abgroup_Z) f) (tensor a z)
exact (grp_pow_natural _ _ _). Defined. (** Since we have symmetry of the tensor product, we get left unitality for free. *)

LeftUnitor ab_tensor_prod abgroup_Z

LeftUnitor ab_tensor_prod abgroup_Z
rapply left_unitor_twist. Defined. (** ** Symmetric Monoidal Structure of Tensor Product *) (** Using the twist construction we can derive an associator for the tensor product. In other words, we have associativity of the tensor product of abelian groups natural in each factor. *)

Associator ab_tensor_prod

Associator ab_tensor_prod

forall a b c : AbGroup, ab_tensor_prod a (ab_tensor_prod b c) $-> ab_tensor_prod b (ab_tensor_prod a c)

forall a b c : AbGroup, ?twist a b c $o ?twist b a c $== Id (ab_tensor_prod b (ab_tensor_prod a c))

forall (a a' b b' c c' : AbGroup) (f : a $-> a') (g : b $-> b') (h : c $-> c'), ?twist a' b' c' $o fmap11 ab_tensor_prod f (fmap11 ab_tensor_prod g h) $== fmap11 ab_tensor_prod g (fmap11 ab_tensor_prod f h) $o ?twist a b c

forall a b c : AbGroup, ab_tensor_prod a (ab_tensor_prod b c) $-> ab_tensor_prod b (ab_tensor_prod a c)
exact @ab_tensor_prod_twist.

forall a b c : AbGroup, ab_tensor_prod_twist $o ab_tensor_prod_twist $== Id (ab_tensor_prod b (ab_tensor_prod a c))
intros; napply ab_tensor_prod_twist_twist.

forall (a a' b b' c c' : AbGroup) (f : a $-> a') (g : b $-> b') (h : c $-> c'), ab_tensor_prod_twist $o fmap11 ab_tensor_prod f (fmap11 ab_tensor_prod g h) $== fmap11 ab_tensor_prod g (fmap11 ab_tensor_prod f h) $o ab_tensor_prod_twist
intros; napply ab_tensor_prod_twist_natural. Defined. (** The triangle identity is straightforward to prove using the custom induction principles we proved earlier. *)

TriangleIdentity ab_tensor_prod abgroup_Z

TriangleIdentity ab_tensor_prod abgroup_Z

forall a b : AbGroup, fmap01 ab_tensor_prod a (rightunitor_ab_tensor_prod b) $== symmetricbraiding_ab_tensor_prod b a $o fmap01 ab_tensor_prod b (rightunitor_ab_tensor_prod a) $o ab_tensor_prod_twist
A, B: AbGroup

fmap01 ab_tensor_prod A (rightunitor_ab_tensor_prod B) $== symmetricbraiding_ab_tensor_prod B A $o fmap01 ab_tensor_prod B (rightunitor_ab_tensor_prod A) $o ab_tensor_prod_twist
A, B: AbGroup

forall (a : A) (b : B) (c : abgroup_Z), fmap01 ab_tensor_prod A (rightunitor_ab_tensor_prod B) (tensor a (tensor b c)) = (symmetricbraiding_ab_tensor_prod B A $o fmap01 ab_tensor_prod B (rightunitor_ab_tensor_prod A) $o ab_tensor_prod_twist) (tensor a (tensor b c))
A, B: AbGroup
a: A
b: B
z: abgroup_Z

(symmetricbraiding_ab_tensor_prod B A $o fmap01 ab_tensor_prod B (rightunitor_ab_tensor_prod A) $o ab_tensor_prod_twist) (tensor a (tensor b z)) = fmap01 ab_tensor_prod A (rightunitor_ab_tensor_prod B) (tensor a (tensor b z))
exact (tensor_ab_mul z a b). Defined. (** The hexagon identity is also straightforward to prove. We simply have to reduce all the involved functions on the simple tensors using our custom triple tensor induction principle. *)

HexagonIdentity ab_tensor_prod

HexagonIdentity ab_tensor_prod

forall a b c : AbGroup, fmap01 ab_tensor_prod c (symmetricbraiding_ab_tensor_prod b a) $o ab_tensor_prod_twist $o fmap01 ab_tensor_prod b (symmetricbraiding_ab_tensor_prod a c) $== ab_tensor_prod_twist $o fmap01 ab_tensor_prod a (symmetricbraiding_ab_tensor_prod b c) $o ab_tensor_prod_twist
A, B, C: AbGroup

fmap01 ab_tensor_prod C (symmetricbraiding_ab_tensor_prod B A) $o ab_tensor_prod_twist $o fmap01 ab_tensor_prod B (symmetricbraiding_ab_tensor_prod A C) $== ab_tensor_prod_twist $o fmap01 ab_tensor_prod A (symmetricbraiding_ab_tensor_prod B C) $o ab_tensor_prod_twist
A, B, C: AbGroup

forall (a : B) (b : A) (c : C), (fmap01 ab_tensor_prod C (symmetricbraiding_ab_tensor_prod B A) $o ab_tensor_prod_twist $o fmap01 ab_tensor_prod B (symmetricbraiding_ab_tensor_prod A C)) (tensor a (tensor b c)) = (ab_tensor_prod_twist $o fmap01 ab_tensor_prod A (symmetricbraiding_ab_tensor_prod B C) $o ab_tensor_prod_twist) (tensor a (tensor b c))
A, B, C: AbGroup
b: B
a: A
c: C

(fmap01 ab_tensor_prod C (symmetricbraiding_ab_tensor_prod B A) $o ab_tensor_prod_twist $o fmap01 ab_tensor_prod B (symmetricbraiding_ab_tensor_prod A C)) (tensor b (tensor a c)) = (ab_tensor_prod_twist $o fmap01 ab_tensor_prod A (symmetricbraiding_ab_tensor_prod B C) $o ab_tensor_prod_twist) (tensor b (tensor a c))
A, B, C: AbGroup
b: B
a: A
c: C

tensor c (tensor a b) = tensor c (tensor a b)
reflexivity. Defined. (** Finally, we can prove the pentagon identity using the quadruple tensor induction principle. As we did before, the work only involves reducing the involved functions on the simple tensor redexes. *)

PentagonIdentity ab_tensor_prod

PentagonIdentity ab_tensor_prod

forall a b c d : AbGroup, fmap01 ab_tensor_prod c (symmetricbraiding_ab_tensor_prod (ab_tensor_prod a b) d) $o ab_tensor_prod_twist $o symmetricbraiding_ab_tensor_prod (ab_tensor_prod c d) (ab_tensor_prod a b) $o ab_tensor_prod_twist $o fmap01 ab_tensor_prod a (symmetricbraiding_ab_tensor_prod b (ab_tensor_prod c d)) $== fmap01 ab_tensor_prod c ab_tensor_prod_twist $o fmap01 ab_tensor_prod c (fmap01 ab_tensor_prod a (symmetricbraiding_ab_tensor_prod b d)) $o ab_tensor_prod_twist $o fmap01 ab_tensor_prod a ab_tensor_prod_twist
A, B, C, D: AbGroup

fmap01 ab_tensor_prod C (symmetricbraiding_ab_tensor_prod (ab_tensor_prod A B) D) $o ab_tensor_prod_twist $o symmetricbraiding_ab_tensor_prod (ab_tensor_prod C D) (ab_tensor_prod A B) $o ab_tensor_prod_twist $o fmap01 ab_tensor_prod A (symmetricbraiding_ab_tensor_prod B (ab_tensor_prod C D)) $== fmap01 ab_tensor_prod C ab_tensor_prod_twist $o fmap01 ab_tensor_prod C (fmap01 ab_tensor_prod A (symmetricbraiding_ab_tensor_prod B D)) $o ab_tensor_prod_twist $o fmap01 ab_tensor_prod A ab_tensor_prod_twist
A, B, C, D: AbGroup

forall (a : A) (b : B) (c : C) (d : D), (fmap01 ab_tensor_prod C (symmetricbraiding_ab_tensor_prod (ab_tensor_prod A B) D) $o ab_tensor_prod_twist $o symmetricbraiding_ab_tensor_prod (ab_tensor_prod C D) (ab_tensor_prod A B) $o ab_tensor_prod_twist $o fmap01 ab_tensor_prod A (symmetricbraiding_ab_tensor_prod B (ab_tensor_prod C D))) (tensor a (tensor b (tensor c d))) = (fmap01 ab_tensor_prod C ab_tensor_prod_twist $o fmap01 ab_tensor_prod C (fmap01 ab_tensor_prod A (symmetricbraiding_ab_tensor_prod B D)) $o ab_tensor_prod_twist $o fmap01 ab_tensor_prod A ab_tensor_prod_twist) (tensor a (tensor b (tensor c d)))
A, B, C, D: AbGroup
a: A
b: B
c: C
d: D

(fmap01 ab_tensor_prod C (symmetricbraiding_ab_tensor_prod (ab_tensor_prod A B) D) $o ab_tensor_prod_twist $o symmetricbraiding_ab_tensor_prod (ab_tensor_prod C D) (ab_tensor_prod A B) $o ab_tensor_prod_twist $o fmap01 ab_tensor_prod A (symmetricbraiding_ab_tensor_prod B (ab_tensor_prod C D))) (tensor a (tensor b (tensor c d))) = (fmap01 ab_tensor_prod C ab_tensor_prod_twist $o fmap01 ab_tensor_prod C (fmap01 ab_tensor_prod A (symmetricbraiding_ab_tensor_prod B D)) $o ab_tensor_prod_twist $o fmap01 ab_tensor_prod A ab_tensor_prod_twist) (tensor a (tensor b (tensor c d)))
A, B, C, D: AbGroup
a: A
b: B
c: C
d: D

tensor c (tensor d (tensor a b)) = tensor c (tensor d (tensor a b))
reflexivity. Defined. (** We therefore have all the data of a monoidal category. *) Instance ismonoidal_ab_tensor_prod : IsMonoidal AbGroup ab_tensor_prod abgroup_Z := {}. (** And furthermore, all the data of a symmetric monoidal category. *) Instance issymmmetricmonoidal_ab_tensor_prod : IsSymmetricMonoidal AbGroup ab_tensor_prod abgroup_Z := {}. (** ** Preservation of Coequalizers *) (** The tensor product of abelian groups preserves coequalizers, meaning that the coequalizer of two tensored groups is the tensor of the coequalizer. We show this is the case on the left and the right. *) (** Tensor products preserve coequalizers on the right. *)
A, B, C: AbGroup
f, g: B $-> C

ab_coeq (fmap01 ab_tensor_prod A f) (fmap01 ab_tensor_prod A g) $<~> ab_tensor_prod A (ab_coeq f g)
A, B, C: AbGroup
f, g: B $-> C

ab_coeq (fmap01 ab_tensor_prod A f) (fmap01 ab_tensor_prod A g) $<~> ab_tensor_prod A (ab_coeq f g)
A, B, C: AbGroup
f, g: B $-> C

ab_coeq (fmap01 ab_tensor_prod A f) (fmap01 ab_tensor_prod A g) $-> ab_tensor_prod A (ab_coeq f g)
A, B, C: AbGroup
f, g: B $-> C
ab_tensor_prod A (ab_coeq f g) $-> ab_coeq (fmap01 ab_tensor_prod A f) (fmap01 ab_tensor_prod A g)
A, B, C: AbGroup
f, g: B $-> C
?f $o ?g $== Id (ab_tensor_prod A (ab_coeq f g))
A, B, C: AbGroup
f, g: B $-> C
?g $o ?f $== Id (ab_coeq (fmap01 ab_tensor_prod A f) (fmap01 ab_tensor_prod A g))
A, B, C: AbGroup
f, g: B $-> C

ab_coeq (fmap01 ab_tensor_prod A f) (fmap01 ab_tensor_prod A g) $-> ab_tensor_prod A (ab_coeq f g)
A, B, C: AbGroup
f, g: B $-> C

ab_tensor_prod A C $-> ab_tensor_prod A (ab_coeq f g)
A, B, C: AbGroup
f, g: B $-> C
?i $o fmap01 ab_tensor_prod A f $== ?i $o fmap01 ab_tensor_prod A g
A, B, C: AbGroup
f, g: B $-> C

ab_tensor_prod A C $-> ab_tensor_prod A (ab_coeq f g)
A, B, C: AbGroup
f, g: B $-> C

C $-> ab_coeq f g
napply ab_coeq_in.
A, B, C: AbGroup
f, g: B $-> C

fmap01 ab_tensor_prod A ab_coeq_in $o fmap01 ab_tensor_prod A f $== fmap01 ab_tensor_prod A ab_coeq_in $o fmap01 ab_tensor_prod A g
A, B, C: AbGroup
f, g: B $-> C

fmap01 ab_tensor_prod A ?Goal0 $-> fmap01 ab_tensor_prod A ab_coeq_in $o fmap01 ab_tensor_prod A f
A, B, C: AbGroup
f, g: B $-> C
?Goal0 $== ?Goal1
A, B, C: AbGroup
f, g: B $-> C
fmap01 ab_tensor_prod A ?Goal1 $== fmap01 ab_tensor_prod A ab_coeq_in $o fmap01 ab_tensor_prod A g
A, B, C: AbGroup
f, g: B $-> C

ab_coeq_in $o f $== ab_coeq_in $o g
napply ab_coeq_glue.
A, B, C: AbGroup
f, g: B $-> C

ab_tensor_prod A (ab_coeq f g) $-> ab_coeq (fmap01 ab_tensor_prod A f) (fmap01 ab_tensor_prod A g)
A, B, C: AbGroup
f, g: B $-> C

A -> ab_coeq f g $-> ab_coeq (fmap01 ab_tensor_prod A f) (fmap01 ab_tensor_prod A g)
A, B, C: AbGroup
f, g: B $-> C
forall (a a' : A) (b : ab_coeq f g), ?f (a + a') b = ?f a b + ?f a' b
A, B, C: AbGroup
f, g: B $-> C

A -> ab_coeq f g $-> ab_coeq (fmap01 ab_tensor_prod A f) (fmap01 ab_tensor_prod A g)
A, B, C: AbGroup
f, g: B $-> C
a: A

ab_coeq f g $-> ab_coeq (fmap01 ab_tensor_prod A f) (fmap01 ab_tensor_prod A g)
A, B, C: AbGroup
f, g: B $-> C
a: A

B $-> ab_tensor_prod A B
A, B, C: AbGroup
f, g: B $-> C
a: A
C $-> ab_tensor_prod A C
A, B, C: AbGroup
f, g: B $-> C
a: A
fmap01 ab_tensor_prod A f $o ?a $== ?b $o f
A, B, C: AbGroup
f, g: B $-> C
a: A
fmap01 ab_tensor_prod A g $o ?a $== ?b $o g
A, B, C: AbGroup
f, g: B $-> C
a: A

fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a $== grp_homo_tensor_l a $o f
A, B, C: AbGroup
f, g: B $-> C
a: A
fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a $== grp_homo_tensor_l a $o g
1,2: hnf; reflexivity.
A, B, C: AbGroup
f, g: B $-> C

forall (a a' : A) (b : ab_coeq f g), (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) (a + a') b = (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) a b + (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) a' b
A, B, C: AbGroup
f, g: B $-> C
a, a': A

forall b : ab_coeq f g, functor_ab_coeq (grp_homo_tensor_l (a + a')) (grp_homo_tensor_l (a + a')) (fun x : B => 1) (fun x : B => 1) b = functor_ab_coeq (grp_homo_tensor_l a) (grp_homo_tensor_l a) (fun x : B => 1) (fun x : B => 1) b + functor_ab_coeq (grp_homo_tensor_l a') (grp_homo_tensor_l a') (fun x : B => 1) (fun x : B => 1) b
A, B, C: AbGroup
f, g: B $-> C
a, a': A

forall b : C, (fun x : ab_coeq f g => functor_ab_coeq (grp_homo_tensor_l (a + a')) (grp_homo_tensor_l (a + a')) (fun x0 : B => 1) (fun x0 : B => 1) x = functor_ab_coeq (grp_homo_tensor_l a) (grp_homo_tensor_l a) (fun x0 : B => 1) (fun x0 : B => 1) x + functor_ab_coeq (grp_homo_tensor_l a') (grp_homo_tensor_l a') (fun x0 : B => 1) (fun x0 : B => 1) x) (ab_coeq_in b)
A, B, C: AbGroup
f, g: B $-> C
a, a': A
x: C

(fun x : ab_coeq f g => functor_ab_coeq (grp_homo_tensor_l (a + a')) (grp_homo_tensor_l (a + a')) (fun x0 : B => 1) (fun x0 : B => 1) x = functor_ab_coeq (grp_homo_tensor_l a) (grp_homo_tensor_l a) (fun x0 : B => 1) (fun x0 : B => 1) x + functor_ab_coeq (grp_homo_tensor_l a') (grp_homo_tensor_l a') (fun x0 : B => 1) (fun x0 : B => 1) x) (ab_coeq_in x)
exact (ap (ab_coeq_in (f:=fmap01 ab_tensor_prod A f) (g:=fmap01 ab_tensor_prod A g)) (tensor_dist_r a a' x)).
A, B, C: AbGroup
f, g: B $-> C

ab_coeq_rec (fmap01 ab_tensor_prod A ab_coeq_in) (((fmap01_comp ab_tensor_prod A ab_coeq_in f)^$ $@ fmap02 ab_tensor_prod A ab_coeq_glue) $@ fmap01_comp ab_tensor_prod A ab_coeq_in g) $o ab_tensor_prod_rec' (fun a : A => functor_ab_coeq (grp_homo_tensor_l a) (grp_homo_tensor_l a) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a $== grp_homo_tensor_l a $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a $== grp_homo_tensor_l a $o g)) (fun a a' : A => ab_coeq_ind_hprop (fun x : ab_coeq f g => functor_ab_coeq (grp_homo_tensor_l (a + a')) (grp_homo_tensor_l (a + a')) (fun x0 : B => 1) (fun x0 : B => 1) x = functor_ab_coeq (grp_homo_tensor_l a) (grp_homo_tensor_l a) (fun x0 : B => 1) (fun x0 : B => 1) x + functor_ab_coeq (grp_homo_tensor_l a') (grp_homo_tensor_l a') (fun x0 : B => 1) (fun x0 : B => 1) x) (fun x : C => ap ab_coeq_in (tensor_dist_r a a' x)) : forall b : ab_coeq f g, (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) (a + a') b = (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) a b + (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) a' b) $== Id (ab_tensor_prod A (ab_coeq f g))
A, B, C: AbGroup
f, g: B $-> C

forall (a : A) (b : ab_coeq f g), (ab_coeq_rec (fmap01 ab_tensor_prod A ab_coeq_in) (((fmap01_comp ab_tensor_prod A ab_coeq_in f)^$ $@ fmap02 ab_tensor_prod A ab_coeq_glue) $@ fmap01_comp ab_tensor_prod A ab_coeq_in g) $o ab_tensor_prod_rec' (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) (fun a0 a' : A => ab_coeq_ind_hprop (fun x : ab_coeq f g => functor_ab_coeq (grp_homo_tensor_l (a0 + a')) (grp_homo_tensor_l (a0 + a')) (fun x0 : B => 1) (fun x0 : B => 1) x = functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) (fun x0 : B => 1) (fun x0 : B => 1) x + functor_ab_coeq (grp_homo_tensor_l a') (grp_homo_tensor_l a') (fun x0 : B => 1) (fun x0 : B => 1) x) (fun x : C => ap ab_coeq_in (tensor_dist_r a0 a' x)) : forall b0 : ab_coeq f g, (fun a1 : A => functor_ab_coeq (grp_homo_tensor_l a1) (grp_homo_tensor_l a1) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a1 $== grp_homo_tensor_l a1 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a1 $== grp_homo_tensor_l a1 $o g)) (a0 + a') b0 = (fun a1 : A => functor_ab_coeq (grp_homo_tensor_l a1) (grp_homo_tensor_l a1) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a1 $== grp_homo_tensor_l a1 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a1 $== grp_homo_tensor_l a1 $o g)) a0 b0 + (fun a1 : A => functor_ab_coeq (grp_homo_tensor_l a1) (grp_homo_tensor_l a1) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a1 $== grp_homo_tensor_l a1 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a1 $== grp_homo_tensor_l a1 $o g)) a' b0)) (tensor a b) = Id (ab_tensor_prod A (ab_coeq f g)) (tensor a b)
A, B, C: AbGroup
f, g: B $-> C
a: A

forall b : ab_coeq f g, (ab_coeq_rec (fmap01 ab_tensor_prod A ab_coeq_in) (((fmap01_comp ab_tensor_prod A ab_coeq_in f)^$ $@ fmap02 ab_tensor_prod A ab_coeq_glue) $@ fmap01_comp ab_tensor_prod A ab_coeq_in g) $o ab_tensor_prod_rec' (fun a : A => functor_ab_coeq (grp_homo_tensor_l a) (grp_homo_tensor_l a) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a $== grp_homo_tensor_l a $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a $== grp_homo_tensor_l a $o g)) (fun a a' : A => ab_coeq_ind_hprop (fun x : ab_coeq f g => functor_ab_coeq (grp_homo_tensor_l (a + a')) (grp_homo_tensor_l (a + a')) (fun x0 : B => 1) (fun x0 : B => 1) x = functor_ab_coeq (grp_homo_tensor_l a) (grp_homo_tensor_l a) (fun x0 : B => 1) (fun x0 : B => 1) x + functor_ab_coeq (grp_homo_tensor_l a') (grp_homo_tensor_l a') (fun x0 : B => 1) (fun x0 : B => 1) x) (fun x : C => ap ab_coeq_in (tensor_dist_r a a' x)) : forall b0 : ab_coeq f g, (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) (a + a') b0 = (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) a b0 + (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) a' b0)) (tensor a b) = Id (ab_tensor_prod A (ab_coeq f g)) (tensor a b)
A, B, C: AbGroup
f, g: B $-> C
a: A

forall b : C, (fun x : ab_coeq f g => (ab_coeq_rec (fmap01 ab_tensor_prod A ab_coeq_in) (((fmap01_comp ab_tensor_prod A ab_coeq_in f)^$ $@ fmap02 ab_tensor_prod A ab_coeq_glue) $@ fmap01_comp ab_tensor_prod A ab_coeq_in g) $o ab_tensor_prod_rec' (fun a : A => functor_ab_coeq (grp_homo_tensor_l a) (grp_homo_tensor_l a) ((fun x0 : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a $== grp_homo_tensor_l a $o f) ((fun x0 : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a $== grp_homo_tensor_l a $o g)) (fun a a' : A => ab_coeq_ind_hprop (fun x0 : ab_coeq f g => functor_ab_coeq (grp_homo_tensor_l (a + a')) (grp_homo_tensor_l (a + a')) (fun x1 : B => 1) (fun x1 : B => 1) x0 = functor_ab_coeq (grp_homo_tensor_l a) (grp_homo_tensor_l a) (fun x1 : B => 1) (fun x1 : B => 1) x0 + functor_ab_coeq (grp_homo_tensor_l a') (grp_homo_tensor_l a') (fun x1 : B => 1) (fun x1 : B => 1) x0) (fun x0 : C => ap ab_coeq_in (tensor_dist_r a a' x0)) : forall b0 : ab_coeq f g, (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x0 : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x0 : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) (a + a') b0 = (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x0 : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x0 : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) a b0 + (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x0 : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x0 : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) a' b0)) (tensor a x) = Id (ab_tensor_prod A (ab_coeq f g)) (tensor a x)) (ab_coeq_in b)
A, B, C: AbGroup
f, g: B $-> C
a: A
c: C

(fun x : ab_coeq f g => (ab_coeq_rec (fmap01 ab_tensor_prod A ab_coeq_in) (((fmap01_comp ab_tensor_prod A ab_coeq_in f)^$ $@ fmap02 ab_tensor_prod A ab_coeq_glue) $@ fmap01_comp ab_tensor_prod A ab_coeq_in g) $o ab_tensor_prod_rec' (fun a : A => functor_ab_coeq (grp_homo_tensor_l a) (grp_homo_tensor_l a) ((fun x0 : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a $== grp_homo_tensor_l a $o f) ((fun x0 : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a $== grp_homo_tensor_l a $o g)) (fun a a' : A => ab_coeq_ind_hprop (fun x0 : ab_coeq f g => functor_ab_coeq (grp_homo_tensor_l (a + a')) (grp_homo_tensor_l (a + a')) (fun x1 : B => 1) (fun x1 : B => 1) x0 = functor_ab_coeq (grp_homo_tensor_l a) (grp_homo_tensor_l a) (fun x1 : B => 1) (fun x1 : B => 1) x0 + functor_ab_coeq (grp_homo_tensor_l a') (grp_homo_tensor_l a') (fun x1 : B => 1) (fun x1 : B => 1) x0) (fun x0 : C => ap ab_coeq_in (tensor_dist_r a a' x0)) : forall b : ab_coeq f g, (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x0 : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x0 : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) (a + a') b = (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x0 : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x0 : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) a b + (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x0 : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x0 : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) a' b)) (tensor a x) = Id (ab_tensor_prod A (ab_coeq f g)) (tensor a x)) (ab_coeq_in c)
reflexivity.
A, B, C: AbGroup
f, g: B $-> C

ab_tensor_prod_rec' (fun a : A => functor_ab_coeq (grp_homo_tensor_l a) (grp_homo_tensor_l a) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a $== grp_homo_tensor_l a $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a $== grp_homo_tensor_l a $o g)) (fun a a' : A => ab_coeq_ind_hprop (fun x : ab_coeq f g => functor_ab_coeq (grp_homo_tensor_l (a + a')) (grp_homo_tensor_l (a + a')) (fun x0 : B => 1) (fun x0 : B => 1) x = functor_ab_coeq (grp_homo_tensor_l a) (grp_homo_tensor_l a) (fun x0 : B => 1) (fun x0 : B => 1) x + functor_ab_coeq (grp_homo_tensor_l a') (grp_homo_tensor_l a') (fun x0 : B => 1) (fun x0 : B => 1) x) (fun x : C => ap ab_coeq_in (tensor_dist_r a a' x)) : forall b : ab_coeq f g, (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) (a + a') b = (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) a b + (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) a' b) $o ab_coeq_rec (fmap01 ab_tensor_prod A ab_coeq_in) (((fmap01_comp ab_tensor_prod A ab_coeq_in f)^$ $@ fmap02 ab_tensor_prod A ab_coeq_glue) $@ fmap01_comp ab_tensor_prod A ab_coeq_in g) $== Id (ab_coeq (fmap01 ab_tensor_prod A f) (fmap01 ab_tensor_prod A g))
A, B, C: AbGroup
f, g: B $-> C

ab_tensor_prod_rec' (fun a : A => functor_ab_coeq (grp_homo_tensor_l a) (grp_homo_tensor_l a) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a $== grp_homo_tensor_l a $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a $== grp_homo_tensor_l a $o g)) (fun a a' : A => ab_coeq_ind_hprop (fun x : ab_coeq f g => functor_ab_coeq (grp_homo_tensor_l (a + a')) (grp_homo_tensor_l (a + a')) (fun x0 : B => 1) (fun x0 : B => 1) x = functor_ab_coeq (grp_homo_tensor_l a) (grp_homo_tensor_l a) (fun x0 : B => 1) (fun x0 : B => 1) x + functor_ab_coeq (grp_homo_tensor_l a') (grp_homo_tensor_l a') (fun x0 : B => 1) (fun x0 : B => 1) x) (fun x : C => ap ab_coeq_in (tensor_dist_r a a' x)) : forall b : ab_coeq f g, (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) (a + a') b = (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) a b + (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) a' b) $o ab_coeq_rec (fmap01 ab_tensor_prod A ab_coeq_in) (((fmap01_comp ab_tensor_prod A ab_coeq_in f)^$ $@ fmap02 ab_tensor_prod A ab_coeq_glue) $@ fmap01_comp ab_tensor_prod A ab_coeq_in g) $o ab_coeq_in $== Id (ab_coeq (fmap01 ab_tensor_prod A f) (fmap01 ab_tensor_prod A g)) $o ab_coeq_in
A, B, C: AbGroup
f, g: B $-> C

forall (a : A) (b : C), (ab_tensor_prod_rec' (fun a0 : A => functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a0 $== grp_homo_tensor_l a0 $o g)) (fun a0 a' : A => ab_coeq_ind_hprop (fun x : ab_coeq f g => functor_ab_coeq (grp_homo_tensor_l (a0 + a')) (grp_homo_tensor_l (a0 + a')) (fun x0 : B => 1) (fun x0 : B => 1) x = functor_ab_coeq (grp_homo_tensor_l a0) (grp_homo_tensor_l a0) (fun x0 : B => 1) (fun x0 : B => 1) x + functor_ab_coeq (grp_homo_tensor_l a') (grp_homo_tensor_l a') (fun x0 : B => 1) (fun x0 : B => 1) x) (fun x : C => ap ab_coeq_in (tensor_dist_r a0 a' x)) : forall b0 : ab_coeq f g, (fun a1 : A => functor_ab_coeq (grp_homo_tensor_l a1) (grp_homo_tensor_l a1) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a1 $== grp_homo_tensor_l a1 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a1 $== grp_homo_tensor_l a1 $o g)) (a0 + a') b0 = (fun a1 : A => functor_ab_coeq (grp_homo_tensor_l a1) (grp_homo_tensor_l a1) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a1 $== grp_homo_tensor_l a1 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a1 $== grp_homo_tensor_l a1 $o g)) a0 b0 + (fun a1 : A => functor_ab_coeq (grp_homo_tensor_l a1) (grp_homo_tensor_l a1) ((fun x : B => 1) : fmap01 ab_tensor_prod A f $o grp_homo_tensor_l a1 $== grp_homo_tensor_l a1 $o f) ((fun x : B => 1) : fmap01 ab_tensor_prod A g $o grp_homo_tensor_l a1 $== grp_homo_tensor_l a1 $o g)) a' b0) $o ab_coeq_rec (fmap01 ab_tensor_prod A ab_coeq_in) (((fmap01_comp ab_tensor_prod A ab_coeq_in f)^$ $@ fmap02 ab_tensor_prod A ab_coeq_glue) $@ fmap01_comp ab_tensor_prod A ab_coeq_in g) $o ab_coeq_in) (tensor a b) = (Id (ab_coeq (fmap01 ab_tensor_prod A f) (fmap01 ab_tensor_prod A g)) $o ab_coeq_in) (tensor a b)
reflexivity. Defined. (** The equivalence respects the natural maps from [ab_tensor_prod A C]. *)
A, B, C: AbGroup
f, g: B $-> C

grp_iso_ab_tensor_prod_coeq_l A f g $o ab_coeq_in $== fmap01 ab_tensor_prod A ab_coeq_in
A, B, C: AbGroup
f, g: B $-> C

grp_iso_ab_tensor_prod_coeq_l A f g $o ab_coeq_in $== fmap01 ab_tensor_prod A ab_coeq_in
A, B, C: AbGroup
f, g: B $-> C

forall (a : A) (b : C), (grp_iso_ab_tensor_prod_coeq_l A f g $o ab_coeq_in) (tensor a b) = fmap01 ab_tensor_prod A ab_coeq_in (tensor a b)
reflexivity. Defined. (** Tensor products preserve coequalizers on the left. *)
A, B: AbGroup
f, g: A $-> B
C: AbGroup

ab_coeq (fmap10 ab_tensor_prod f C) (fmap10 ab_tensor_prod g C) $<~> ab_tensor_prod (ab_coeq f g) C
A, B: AbGroup
f, g: A $-> B
C: AbGroup

ab_coeq (fmap10 ab_tensor_prod f C) (fmap10 ab_tensor_prod g C) $<~> ab_tensor_prod (ab_coeq f g) C
A, B: AbGroup
f, g: A $-> B
C: AbGroup

ab_coeq (fmap10 ab_tensor_prod f C) (fmap10 ab_tensor_prod g C) $<~> ab_tensor_prod C (ab_coeq f g)
A, B: AbGroup
f, g: A $-> B
C: AbGroup

ab_coeq (fmap10 ab_tensor_prod f C) (fmap10 ab_tensor_prod g C) $<~> ab_coeq (fmap01 ab_tensor_prod C f) (fmap01 ab_tensor_prod C g)
A, B: AbGroup
f, g: A $-> B
C: AbGroup

ab_tensor_prod A C $<~> ab_tensor_prod C A
A, B: AbGroup
f, g: A $-> B
C: AbGroup
ab_tensor_prod B C $<~> ab_tensor_prod C B
A, B: AbGroup
f, g: A $-> B
C: AbGroup
fmap01 ab_tensor_prod C f $o ?a $== ?b $o fmap10 ab_tensor_prod f C
A, B: AbGroup
f, g: A $-> B
C: AbGroup
fmap01 ab_tensor_prod C g $o ?a $== ?b $o fmap10 ab_tensor_prod g C
A, B: AbGroup
f, g: A $-> B
C: AbGroup

fmap01 ab_tensor_prod C f $o braide A C $== braide B C $o fmap10 ab_tensor_prod f C
A, B: AbGroup
f, g: A $-> B
C: AbGroup
fmap01 ab_tensor_prod C g $o braide A C $== braide B C $o fmap10 ab_tensor_prod g C
1,2: symmetry; napply ab_tensor_swap_natural. Defined. (** The equivalence respects the natural maps from [ab_tensor_prod B C]. *)
A, B: AbGroup
f, g: A $-> B
C: AbGroup

grp_iso_ab_tensor_prod_coeq_r f g C $o ab_coeq_in $== fmap10 ab_tensor_prod ab_coeq_in C
A, B: AbGroup
f, g: A $-> B
C: AbGroup

grp_iso_ab_tensor_prod_coeq_r f g C $o ab_coeq_in $== fmap10 ab_tensor_prod ab_coeq_in C
A, B: AbGroup
f, g: A $-> B
C: AbGroup

forall (a : B) (b : C), (grp_iso_ab_tensor_prod_coeq_r f g C $o ab_coeq_in) (tensor a b) = fmap10 ab_tensor_prod ab_coeq_in C (tensor a b)
reflexivity. Defined. (** ** Tensor Product of Free Abelian Groups *)
X, Y: Type

FreeAbGroup (X * Y) $<~> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
X, Y: Type

FreeAbGroup (X * Y) $<~> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
X, Y: Type

FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
X, Y: Type
f:= ?Goal: FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)
X, Y: Type
f:= ?Goal: FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ?Goal0: ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)
f $o g $== Id (ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y))
X, Y: Type
f:= ?Goal: FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ?Goal0: ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)
g $o f $== Id (FreeAbGroup (X * Y))
X, Y: Type

FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
X, Y: Type

X * Y -> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
X, Y: Type
x: X
y: Y

ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
exact (tensor (freeabgroup_in x) (freeabgroup_in y)).
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)

ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)

FreeAbGroup X -> FreeAbGroup Y -> FreeAbGroup (X * Y)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
forall (a : FreeAbGroup X) (b b' : FreeAbGroup Y), ?f a (b + b') = ?f a b + ?f a b'
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
forall (a a' : FreeAbGroup X) (b : FreeAbGroup Y), ?f (a + a') b = ?f a b + ?f a' b
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)

FreeAbGroup X -> FreeAbGroup Y -> FreeAbGroup (X * Y)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
x: FreeAbGroup X

FreeAbGroup Y -> FreeAbGroup (X * Y)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
x: FreeAbGroup X

Y -> FreeAbGroup (X * Y)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
y: Y

FreeAbGroup X -> FreeAbGroup (X * Y)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
y: Y

abel (FreeGroup X) -> abel (FreeGroup (X * Y))
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
y: Y

X -> abel (FreeGroup (X * Y))
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
y: Y
x: X

abel (FreeGroup (X * Y))
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
y: Y
x: X

FreeGroup (X * Y)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
y: Y
x: X

X * Y
exact (x, y).
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)

forall (a : FreeAbGroup X) (b b' : FreeAbGroup Y), (fun x : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x))) a (b + b') = (fun x : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x))) a b + (fun x : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x))) a b'
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
x: FreeAbGroup X
y, y': FreeAbGroup Y

(fun x : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x))) x (y + y') = (fun x : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x))) x y + (fun x : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x))) x y'
snapply grp_homo_op.
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)

forall (a a' : FreeAbGroup X) (b : FreeAbGroup Y), (fun x : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x))) (a + a') b = (fun x : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x))) a b + (fun x : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x))) a' b
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
x, x': FreeAbGroup X

forall b : FreeAbGroup Y, (fun x : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x))) (x + x') b = (fun x : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x))) x b + (fun x : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x))) x' b
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
x, x': FreeAbGroup X

forall x0 : FreeGroup Y, FreeAbGroup_rec (fun y : Y => FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) (x + x')) (abel_in x0) = FreeAbGroup_rec (fun y : Y => FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) x) (abel_in x0) + FreeAbGroup_rec (fun y : Y => FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) x') (abel_in x0)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
x, x': FreeAbGroup X

forall x0 : Y, FreeGroup_rec (fun y : Y => FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) (x + x')) (freegroup_in x0) = sgop_hom (FreeGroup_rec (fun y : Y => FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) x)) (FreeGroup_rec (fun y : Y => FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) x')) (freegroup_in x0)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
x, x': FreeAbGroup X
y: Y

FreeGroup_rec (fun y : Y => FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) (x + x')) (freegroup_in y) = sgop_hom (FreeGroup_rec (fun y : Y => FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) x)) (FreeGroup_rec (fun y : Y => FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) x')) (freegroup_in y)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
x, x': FreeAbGroup X
y: Y

FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) (x + x') = sgop_hom (FreeGroup_rec (fun y : Y => FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) x)) (FreeGroup_rec (fun y : Y => FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) x')) (freegroup_in y)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
x, x': FreeAbGroup X
y: Y

FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) x + FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) x' = sgop_hom (FreeGroup_rec (fun y : Y => FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) x)) (FreeGroup_rec (fun y : Y => FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) x')) (freegroup_in y)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
x, x': FreeAbGroup X
y: Y

grp_homo_id (fst (grp_prod_corec (FreeGroup_rec (fun y : Y => FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) x)) (FreeGroup_rec (fun y : Y => FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) x')) (freegroup_in y))) = FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) x
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
x, x': FreeAbGroup X
y: Y
grp_homo_id (snd (grp_prod_corec (FreeGroup_rec (fun y : Y => FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) x)) (FreeGroup_rec (fun y : Y => FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) x')) (freegroup_in y))) = FreeAbGroup_rec (fun x : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x, y))) x'
1,2: napply FreeGroup_rec_beta.
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)

f $o g $== Id (ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y))
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)

forall (a : FreeAbGroup X) (b : FreeAbGroup Y), (f $o g) (tensor a b) = Id (ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)) (tensor a b)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)
x: FreeAbGroup X

forall b : FreeAbGroup Y, (f $o g) (tensor x b) = Id (ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)) (tensor x b)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)
x: FreeAbGroup X

f $o g $o grp_homo_tensor_l x $== grp_homo_tensor_l x
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)
x: FreeAbGroup X

forall x0 : FreeGroup Y, (f $o g $o grp_homo_tensor_l x) (abel_in x0) = grp_homo_tensor_l x (abel_in x0)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)
x: FreeAbGroup X

forall x0 : FreeGroup Y, (f $o g $o grp_homo_tensor_l x) (abel_unit x0) = grp_homo_tensor_l x (abel_unit x0)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)
x: FreeAbGroup X

forall x0 : FreeGroup Y, (f $o g $o grp_homo_tensor_l x) (abel_unit x0) = grp_homo_tensor_l x (abel_unit x0)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)
x: FreeAbGroup X

f $o g $o grp_homo_tensor_l x $o abel_unit $== grp_homo_tensor_l x $o abel_unit
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)
x: FreeAbGroup X

forall x0 : Y, (f $o g $o grp_homo_tensor_l x $o abel_unit) (freegroup_in x0) = (grp_homo_tensor_l x $o abel_unit) (freegroup_in x0)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)
y: Y

forall x : FreeAbGroup X, (f $o g $o grp_homo_tensor_l x $o abel_unit) (freegroup_in y) = (grp_homo_tensor_l x $o abel_unit) (freegroup_in y)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)
y: Y

f $o g $o grp_homo_tensor_r (freeabgroup_in y) $== grp_homo_tensor_r (freeabgroup_in y)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)
y: Y

forall x : FreeGroup X, (f $o g $o grp_homo_tensor_r (freeabgroup_in y)) (abel_in x) = grp_homo_tensor_r (freeabgroup_in y) (abel_in x)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)
y: Y

forall x : FreeGroup X, (f $o g $o grp_homo_tensor_r (freeabgroup_in y)) (abel_unit x) = grp_homo_tensor_r (freeabgroup_in y) (abel_unit x)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)
y: Y

forall x : FreeGroup X, (f $o g $o grp_homo_tensor_r (freeabgroup_in y)) (abel_unit x) = grp_homo_tensor_r (freeabgroup_in y) (abel_unit x)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)
y: Y

f $o g $o grp_homo_tensor_r (freeabgroup_in y) $o abel_unit $== grp_homo_tensor_r (freeabgroup_in y) $o abel_unit
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)
y: Y

forall x : X, (f $o g $o grp_homo_tensor_r (freeabgroup_in y) $o abel_unit) (freegroup_in x) = (grp_homo_tensor_r (freeabgroup_in y) $o abel_unit) (freegroup_in x)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)
y: Y
x: X

(f $o g $o grp_homo_tensor_r (freeabgroup_in y) $o abel_unit) (freegroup_in x) = (grp_homo_tensor_r (freeabgroup_in y) $o abel_unit) (freegroup_in x)
reflexivity.
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)

g $o f $== Id (FreeAbGroup (X * Y))
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)

forall x : FreeGroup (X * Y), (g $o f) (abel_in x) = Id (FreeAbGroup (X * Y)) (abel_in x)
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)

g $o f $o abel_unit $== abel_unit
X, Y: Type
f:= FreeAbGroup_rec (fun X0 : X * Y => (fun (x : X) (y : Y) => tensor (freeabgroup_in x) (freeabgroup_in y)) (fst X0) (snd X0)): FreeAbGroup (X * Y) $-> ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y)
g:= ab_tensor_prod_rec (fun x : FreeAbGroup X => FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) (fun (x : FreeAbGroup X) (y y' : FreeAbGroup Y) => grp_homo_op (FreeAbGroup_rec (fun y0 : Y => (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x)) y y') (fun x x' : FreeAbGroup X => Abel_ind_hprop (FreeGroup Y) (fun x0 : Abel (FreeGroup Y) => (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) (x + x') x0 = (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x x0 + (fun x1 : FreeAbGroup X => grp_homo_map (FreeAbGroup_rec (fun y : Y => (FreeAbGroup_rec (fun x2 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x2, y))) : FreeAbGroup X -> FreeAbGroup (X * Y)) x1))) x' x0) (FreeGroup_ind_homotopy (fun y : Y => FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) (x + x')) y @ (grp_homo_op (FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y)))) x x' @ ap011 sg_op (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x) y)^ (FreeGroup_rec_beta Y (fun y0 : Y => FreeAbGroup_rec (fun x0 : X => let X0 := grp_homo_map abel_unit in X0 (freegroup_in (x0, y0))) x') y)^)))): ab_tensor_prod (FreeAbGroup X) (FreeAbGroup Y) $-> FreeAbGroup (X * Y)

forall x : X * Y, (g $o f $o abel_unit) (freegroup_in x) = abel_unit (freegroup_in x)
reflexivity. Defined. (** ** Tensor products distribute over direct sums *)
A, B, C: AbGroup

ab_tensor_prod A (ab_biprod B C) $<~> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
A, B, C: AbGroup

ab_tensor_prod A (ab_biprod B C) $<~> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
A, B, C: AbGroup

ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
A, B, C: AbGroup
f:= ?Goal: ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)
A, B, C: AbGroup
f:= ?Goal: ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ?Goal0: ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)
f $o g $== Id (ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C))
A, B, C: AbGroup
f:= ?Goal: ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ?Goal0: ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)
g $o f $== Id (ab_tensor_prod A (ab_biprod B C))
A, B, C: AbGroup

ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
A, B, C: AbGroup

A -> ab_biprod B C -> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
A, B, C: AbGroup
forall (a : A) (b b' : ab_biprod B C), ?f a (b + b') = ?f a b + ?f a b'
A, B, C: AbGroup
forall (a a' : A) (b : ab_biprod B C), ?f (a + a') b = ?f a b + ?f a' b
A, B, C: AbGroup

A -> ab_biprod B C -> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
A, B, C: AbGroup
a: A
bc: ab_biprod B C

ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
exact (tensor a (fst bc), tensor a (snd bc)).
A, B, C: AbGroup

forall (a : A) (b b' : ab_biprod B C), (fun (a0 : A) (bc : ab_biprod B C) => (tensor a0 (fst bc), tensor a0 (snd bc))) a (b + b') = (fun (a0 : A) (bc : ab_biprod B C) => (tensor a0 (fst bc), tensor a0 (snd bc))) a b + (fun (a0 : A) (bc : ab_biprod B C) => (tensor a0 (fst bc), tensor a0 (snd bc))) a b'
A, B, C: AbGroup
a: A
bc, bc': ab_biprod B C

(tensor a (fst (bc + bc')), tensor a (snd (bc + bc'))) = (tensor a (fst bc), tensor a (snd bc)) + (tensor a (fst bc'), tensor a (snd bc'))
snapply path_prod'; snapply tensor_dist_l.
A, B, C: AbGroup

forall (a a' : A) (b : ab_biprod B C), (fun (a0 : A) (bc : ab_biprod B C) => (tensor a0 (fst bc), tensor a0 (snd bc))) (a + a') b = (fun (a0 : A) (bc : ab_biprod B C) => (tensor a0 (fst bc), tensor a0 (snd bc))) a b + (fun (a0 : A) (bc : ab_biprod B C) => (tensor a0 (fst bc), tensor a0 (snd bc))) a' b
A, B, C: AbGroup
a, a': A
bc: ab_biprod B C

(tensor (a + a') (fst bc), tensor (a + a') (snd bc)) = (tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))
snapply path_prod; snapply tensor_dist_r.
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)

ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)

ab_tensor_prod A B $-> ab_tensor_prod A (ab_biprod B C)
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
ab_tensor_prod A C $-> ab_tensor_prod A (ab_biprod B C)
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)

ab_tensor_prod A B $-> ab_tensor_prod A (ab_biprod B C)
exact (fmap01 ab_tensor_prod A ab_biprod_inl).
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)

ab_tensor_prod A C $-> ab_tensor_prod A (ab_biprod B C)
exact (fmap01 ab_tensor_prod A ab_biprod_inr).
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)

f $o g $== Id (ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C))
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)

f $o g $o ab_biprod_inl $== Id (ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)) $o ab_biprod_inl
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)
f $o g $o ab_biprod_inr $== Id (ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)) $o ab_biprod_inr
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)

f $o g $o ab_biprod_inl $== Id (ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)) $o ab_biprod_inl
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)

g $o ab_biprod_inl $== ?Goal
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)
f $o ?Goal $== Id (ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)) $o ab_biprod_inl
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)

f $o fmap01 ab_tensor_prod A ab_biprod_inl $== Id (ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)) $o ab_biprod_inl
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)

forall (a : A) (b : B), (f $o fmap01 ab_tensor_prod A ab_biprod_inl) (tensor a b) = (Id (ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)) $o ab_biprod_inl) (tensor a b)
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)
a: A
b: B

(f $o fmap01 ab_tensor_prod A ab_biprod_inl) (tensor a b) = (Id (ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)) $o ab_biprod_inl) (tensor a b)
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)
a: A
b: B

tensor a b = tensor a b
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)
a: A
b: B
tensor a group_unit = congquot_mon_unit
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)
a: A
b: B

tensor a b = tensor a b
reflexivity.
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)
a: A
b: B

tensor a group_unit = congquot_mon_unit
snapply tensor_zero_r.
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)

f $o g $o ab_biprod_inr $== Id (ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)) $o ab_biprod_inr
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)

g $o ab_biprod_inr $== ?Goal
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)
f $o ?Goal $== Id (ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)) $o ab_biprod_inr
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)

f $o fmap01 ab_tensor_prod A ab_biprod_inr $== Id (ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)) $o ab_biprod_inr
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)

forall (a : A) (b : C), (f $o fmap01 ab_tensor_prod A ab_biprod_inr) (tensor a b) = (Id (ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)) $o ab_biprod_inr) (tensor a b)
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)
a: A
b: C

(f $o fmap01 ab_tensor_prod A ab_biprod_inr) (tensor a b) = (Id (ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)) $o ab_biprod_inr) (tensor a b)
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)
a: A
b: C

tensor a group_unit = congquot_mon_unit
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)
a: A
b: C
tensor a b = tensor a b
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)
a: A
b: C

tensor a group_unit = congquot_mon_unit
snapply tensor_zero_r.
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)
a: A
b: C

tensor a b = tensor a b
reflexivity.
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)

g $o f $== Id (ab_tensor_prod A (ab_biprod B C))
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)

forall (a : A) (b : ab_biprod B C), (g $o f) (tensor a b) = Id (ab_tensor_prod A (ab_biprod B C)) (tensor a b)
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)
a: A
b: B
c: C

(g $o f) (tensor a (b, c)) = Id (ab_tensor_prod A (ab_biprod B C)) (tensor a (b, c))
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)
a: A
b: B
c: C

tensor a ((b, group_unit) + (group_unit, c)) = tensor a (b, c)
A, B, C: AbGroup
f:= ab_tensor_prod_rec (fun (a : A) (bc : ab_biprod B C) => (tensor a (fst bc), tensor a (snd bc))) (fun (a : A) (bc bc' : ab_biprod B C) => path_prod' (tensor_dist_l a (fst bc) (fst bc')) (tensor_dist_l a (snd bc) (snd bc')) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a (bc + bc') = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc') (fun (a a' : A) (bc : ab_biprod B C) => path_prod (tensor (a + a') (fst bc), tensor (a + a') (snd bc)) ((tensor a (fst bc), tensor a (snd bc)) + (tensor a' (fst bc), tensor a' (snd bc))) (tensor_dist_r a a' (fst bc)) (tensor_dist_r a a' (snd bc)) : (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) (a + a') bc = (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a bc + (fun (a0 : A) (bc0 : ab_biprod B C) => (tensor a0 (fst bc0), tensor a0 (snd bc0))) a' bc): ab_tensor_prod A (ab_biprod B C) $-> ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C)
g:= ab_biprod_rec (fmap01 ab_tensor_prod A ab_biprod_inl) (fmap01 ab_tensor_prod A ab_biprod_inr): ab_biprod (ab_tensor_prod A B) (ab_tensor_prod A C) $-> ab_tensor_prod A (ab_biprod B C)
a: A
b: B
c: C

(b, group_unit) + (group_unit, c) = (b, c)
symmetry; apply grp_prod_decompose. Defined.
A, B, C: AbGroup

ab_tensor_prod (ab_biprod A B) C $<~> ab_biprod (ab_tensor_prod A C) (ab_tensor_prod B C)
A, B, C: AbGroup

ab_tensor_prod (ab_biprod A B) C $<~> ab_biprod (ab_tensor_prod A C) (ab_tensor_prod B C)
A, B, C: AbGroup

ab_tensor_prod C (ab_biprod A B) $<~> ab_biprod (ab_tensor_prod C A) (ab_tensor_prod C B)
snapply ab_tensor_prod_dist_l. Defined. (** TODO: Show that the category of abelian groups is symmetric closed and therefore we have adjoint pair with the tensor and internal hom. This should allow us to prove lemmas such as tensors distributing over coproducts. *)