---

Step * of Lemma functor-uncurry_wf

∀[A,B,C:SmallCategory].  (functor-uncurry(C) ∈ Functor(FUN(A;FUN(B;C));FUN(A × B;C)))
BY
{ (Auto
   THEN (Assert ∀f:Functor(A;FUN(B;C))
                  (functor(ob(p) = f (fst(p)) (snd(p));
                           arrow(x,y,p) = cat-comp(C) (f (fst(x)) (snd(x))) (f (fst(y)) (snd(x))) (f (fst(y)) (snd(y))) 
                                          (f (fst(x)) (fst(y)) (fst(p)) (snd(x))) 
                                          (f (fst(y)) (snd(x)) (snd(y)) (snd(p)))) ∈ cat-ob(FUN(A × B;C))) BY
               (Auto THEN RW CatNormC 0 THEN Auto))
   THEN ProveWfLemma
   THEN Reduce 0
   THEN Try (((NatTransEq THENA Auto) THEN Reduce 0 THEN Try ((NormCatEq THEN Auto))))
   THEN All Reduce
   THEN DProds
   THEN All Reduce) }

1
1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. ∀f:Functor(A;FUN(B;C))
     (functor(ob(p) = f (fst(p)) (snd(p));
              arrow(x,y,p) = cat-comp(C) (f (fst(x)) (snd(x))) (f (fst(y)) (snd(x))) (f (fst(y)) (snd(y))) 
                             (f (fst(x)) (fst(y)) (fst(p)) (snd(x))) 
                             (f (fst(y)) (snd(x)) (snd(y)) (snd(p)))) ∈ Functor(A × B;C))
5. f : Functor(A;FUN(B;C))
6. g : Functor(A;FUN(B;C))
7. T : nat-trans(A;FUN(B;C);f;g)
8. A2 : cat-ob(A)
9. A3 : cat-ob(B)
10. B2 : cat-ob(A)
11. B3 : cat-ob(B)
12. g2 : cat-arrow(A) A2 B2
13. g3 : cat-arrow(B) A3 B3
⊢ (cat-comp(C) (f A2 A3) (g A2 A3) (g B2 B3) (T A2 A3) 
   (cat-comp(C) (g A2 A3) (g B2 A3) (g B2 B3) (g A2 B2 g2 A3) (g B2 A3 B3 g3)))
= (cat-comp(C) (f A2 A3) (f B2 B3) (g B2 B3) 
   (cat-comp(C) (f A2 A3) (f B2 A3) (f B2 B3) (f A2 B2 g2 A3) (f B2 A3 B3 g3)) 
   (T B2 B3))
∈ (cat-arrow(C) (f A2 A3) (g B2 B3))

2
1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. ∀f:Functor(A;FUN(B;C))
     (functor(ob(p) = f (fst(p)) (snd(p));
              arrow(x,y,p) = cat-comp(C) (f (fst(x)) (snd(x))) (f (fst(y)) (snd(x))) (f (fst(y)) (snd(y))) 
                             (f (fst(x)) (fst(y)) (fst(p)) (snd(x))) 
                             (f (fst(y)) (snd(x)) (snd(y)) (snd(p)))) ∈ Functor(A × B;C))
5. f : Functor(A;FUN(B;C))
6. g : Functor(A;FUN(B;C))
7. z : Functor(A;FUN(B;C))
8. T : nat-trans(A;FUN(B;C);f;g)
9. g1 : nat-trans(A;FUN(B;C);g;z)
10. A1 : cat-ob(A)
11. A2 : cat-ob(B)
12. B1 : cat-ob(A)
13. B2 : cat-ob(B)
14. g3 : cat-arrow(A) A1 B1
15. g4 : cat-arrow(B) A2 B2
⊢ (cat-comp(C) (f A1 A2) (z A1 A2) (z B1 B2) (cat-comp(C) (f A1 A2) (g A1 A2) (z A1 A2) (T A1 A2) (g1 A1 A2)) 
   (cat-comp(C) (z A1 A2) (z B1 A2) (z B1 B2) (z A1 B1 g3 A2) (z B1 A2 B2 g4)))
= (cat-comp(C) (f A1 A2) (f B1 B2) (z B1 B2) 
   (cat-comp(C) (f A1 A2) (f B1 A2) (f B1 B2) (f A1 B1 g3 A2) (f B1 A2 B2 g4)) 
   (cat-comp(C) (f B1 B2) (g B1 B2) (z B1 B2) (T B1 B2) (g1 B1 B2)))
∈ (cat-arrow(C) (f A1 A2) (z B1 B2))

---

Latex:

---

Latex:
\mforall{}[A,B,C:SmallCategory].    (functor-uncurry(C)  \mmember{}  Functor(FUN(A;FUN(B;C));FUN(A  \mtimes{}  B;C)))


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}f:Functor(A;FUN(B;C))
                                (functor(ob(p)  =  f  (fst(p))  (snd(p));
                                                  arrow(x,y,p)  =  cat-comp(C)  (f  (fst(x))  (snd(x)))  (f  (fst(y))  (snd(x))) 
                                                                                (f  (fst(y))  (snd(y))) 
                                                                                (f  (fst(x))  (fst(y))  (fst(p))  (snd(x))) 
                                                                                (f  (fst(y))  (snd(x))  (snd(y))  (snd(p))))
                                  \mmember{}  cat-ob(FUN(A  \mtimes{}  B;C)))  BY
                          (Auto  THEN  RW  CatNormC  0  THEN  Auto))
  THEN  ProveWfLemma
  THEN  Reduce  0
  THEN  Try  (((NatTransEq  THENA  Auto)  THEN  Reduce  0  THEN  Try  ((NormCatEq  THEN  Auto))))
  THEN  All  Reduce
  THEN  DProds
  THEN  All  Reduce)

---

Home Index