Step
*
2
1
1
1
of Lemma
functor-uncurry_wf
1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. f : Functor(A;FUN(B;C))
5. g : Functor(A;FUN(B;C))
6. h : Functor(A;FUN(B;C))
7. t1 : nat-trans(A;FUN(B;C);f;g)
8. t2 : nat-trans(A;FUN(B;C);g;h)
9. a1 : cat-ob(A)
10. b1 : cat-ob(B)
11. a2 : cat-ob(A)
12. b2 : cat-ob(B)
13. xa : cat-arrow(A) a1 a2
14. xb : cat-arrow(B) b1 b2
15. t1 a1 o t2 a1 o h a1 a2 xa = f a1 a2 xa o t1 a2 o t2 a2 ∈ (A:cat-ob(B) ⟶ (cat-arrow(C) (f a1 A) (h a2 A)))
16. ∀A,B@0:cat-ob(B). ∀g@0:cat-arrow(B) A B@0.
((cat-comp(C) (f a1 A) (h a2 A) (h a2 B@0) (t1 a1 o t2 a1 o h a1 a2 xa A) (h a2 A B@0 g@0))
= (cat-comp(C) (f a1 A) (f a1 B@0) (h a2 B@0) (f a1 A B@0 g@0) (t1 a1 o t2 a1 o h a1 a2 xa B@0))
∈ (cat-arrow(C) (f a1 A) (h a2 B@0)))
⊢ (cat-comp(C) (f a1 b1) (h a1 b2) (h a2 b2)
(cat-comp(C) (f a1 b1) (g a1 b2) (h a1 b2) (cat-comp(C) (f a1 b1) (f a1 b2) (g a1 b2) (f a1 b1 b2 xb) (t1 a1 b2))
(t2 a1 b2))
(h a1 a2 xa b2))
= (cat-comp(C) (f a1 b1) (g a2 b2) (h a2 b2)
(cat-comp(C) (f a1 b1) (f a2 b2) (g a2 b2)
(cat-comp(C) (f a1 b1) (f a1 b2) (f a2 b2) (f a1 b1 b2 xb) (f a1 a2 xa b2))
(t1 a2 b2))
(t2 a2 b2))
∈ (cat-arrow(C) (f a1 b1) (h a2 b2))
BY
{ ((Assert ⌜∀b:cat-ob(B)
((t1 a1 o t2 a1 o h a1 a2 xa b) = (f a1 a2 xa o t1 a2 o t2 a2 b) ∈ (cat-arrow(C) (f a1 b) (h a2 b)))⌝⋅
THENA Auto
)
THEN skip{(Reduce -1 THEN (RWO "cat-comp-assoc" 0 THENA Auto) THEN RWO "-1" 0 THEN Auto)}
) }
1
1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. f : Functor(A;FUN(B;C))
5. g : Functor(A;FUN(B;C))
6. h : Functor(A;FUN(B;C))
7. t1 : nat-trans(A;FUN(B;C);f;g)
8. t2 : nat-trans(A;FUN(B;C);g;h)
9. a1 : cat-ob(A)
10. b1 : cat-ob(B)
11. a2 : cat-ob(A)
12. b2 : cat-ob(B)
13. xa : cat-arrow(A) a1 a2
14. xb : cat-arrow(B) b1 b2
15. t1 a1 o t2 a1 o h a1 a2 xa = f a1 a2 xa o t1 a2 o t2 a2 ∈ (A:cat-ob(B) ⟶ (cat-arrow(C) (f a1 A) (h a2 A)))
16. ∀A,B@0:cat-ob(B). ∀g@0:cat-arrow(B) A B@0.
((cat-comp(C) (f a1 A) (h a2 A) (h a2 B@0) (t1 a1 o t2 a1 o h a1 a2 xa A) (h a2 A B@0 g@0))
= (cat-comp(C) (f a1 A) (f a1 B@0) (h a2 B@0) (f a1 A B@0 g@0) (t1 a1 o t2 a1 o h a1 a2 xa B@0))
∈ (cat-arrow(C) (f a1 A) (h a2 B@0)))
17. ∀b:cat-ob(B). ((t1 a1 o t2 a1 o h a1 a2 xa b) = (f a1 a2 xa o t1 a2 o t2 a2 b) ∈ (cat-arrow(C) (f a1 b) (h a2 b)))
⊢ (cat-comp(C) (f a1 b1) (h a1 b2) (h a2 b2)
(cat-comp(C) (f a1 b1) (g a1 b2) (h a1 b2) (cat-comp(C) (f a1 b1) (f a1 b2) (g a1 b2) (f a1 b1 b2 xb) (t1 a1 b2))
(t2 a1 b2))
(h a1 a2 xa b2))
= (cat-comp(C) (f a1 b1) (g a2 b2) (h a2 b2)
(cat-comp(C) (f a1 b1) (f a2 b2) (g a2 b2)
(cat-comp(C) (f a1 b1) (f a1 b2) (f a2 b2) (f a1 b1 b2 xb) (f a1 a2 xa b2))
(t1 a2 b2))
(t2 a2 b2))
∈ (cat-arrow(C) (f a1 b1) (h a2 b2))
Latex:
Latex:
1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. f : Functor(A;FUN(B;C))
5. g : Functor(A;FUN(B;C))
6. h : Functor(A;FUN(B;C))
7. t1 : nat-trans(A;FUN(B;C);f;g)
8. t2 : nat-trans(A;FUN(B;C);g;h)
9. a1 : cat-ob(A)
10. b1 : cat-ob(B)
11. a2 : cat-ob(A)
12. b2 : cat-ob(B)
13. xa : cat-arrow(A) a1 a2
14. xb : cat-arrow(B) b1 b2
15. t1 a1 o t2 a1 o h a1 a2 xa = f a1 a2 xa o t1 a2 o t2 a2
16. \mforall{}A,B@0:cat-ob(B). \mforall{}g@0:cat-arrow(B) A B@0.
((cat-comp(C) (f a1 A) (h a2 A) (h a2 B@0) (t1 a1 o t2 a1 o h a1 a2 xa A) (h a2 A B@0 g@0))
= (cat-comp(C) (f a1 A) (f a1 B@0) (h a2 B@0) (f a1 A B@0 g@0)
(t1 a1 o t2 a1 o h a1 a2 xa B@0)))
\mvdash{} (cat-comp(C) (f a1 b1) (h a1 b2) (h a2 b2)
(cat-comp(C) (f a1 b1) (g a1 b2) (h a1 b2)
(cat-comp(C) (f a1 b1) (f a1 b2) (g a1 b2) (f a1 b1 b2 xb) (t1 a1 b2))
(t2 a1 b2))
(h a1 a2 xa b2))
= (cat-comp(C) (f a1 b1) (g a2 b2) (h a2 b2)
(cat-comp(C) (f a1 b1) (f a2 b2) (g a2 b2)
(cat-comp(C) (f a1 b1) (f a1 b2) (f a2 b2) (f a1 b1 b2 xb) (f a1 a2 xa b2))
(t1 a2 b2))
(t2 a2 b2))
By
Latex:
((Assert \mkleeneopen{}\mforall{}b:cat-ob(B). ((t1 a1 o t2 a1 o h a1 a2 xa b) = (f a1 a2 xa o t1 a2 o t2 a2 b))\mkleeneclose{}\mcdot{}
THENA Auto
)
THEN skip\{(Reduce -1 THEN (RWO "cat-comp-assoc" 0 THENA Auto) THEN RWO "-1" 0 THEN Auto)\}
)
Home
Index