---

Step * 1 1 1 1 of Lemma functor-curry-iso


1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. functor-uncurry(C) ∈ Functor(FUN(A;FUN(B;C));FUN(A × B;C))
5. functor-curry(A;B) ∈ Functor(FUN(A × B;C);FUN(A;FUN(B;C)))
6. ∀x:Functor(A × B;C). ((ob(functor-comp(functor-curry(A;B);functor-uncurry(C))) x) = x ∈ Functor(A × B;C))
7. ∀f:Functor(A;FUN(B;C)). ∀a:cat-ob(A).
     ((ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) f) a) = (ob(f) a) ∈ cat-ob(FUN(B;C)))
8. x : Functor(A × B;C)
9. y : Functor(A × B;C)
10. f : nat-trans(A × B;C;x;y)
11. A2 : cat-ob(A)
12. A3 : cat-ob(B)
⊢ (arrow(functor-comp(functor-curry(A;B);functor-uncurry(C))) x y f <A2, A3>)
= (f <A2, A3>)
∈ (cat-arrow(C) (ob(ob(functor-comp(functor-curry(A;B);functor-uncurry(C))) x) <A2, A3>) (ob(ob(functor-comp(functor-cur\000Cry(A;B);functor-uncurry(C))) y) <A2, A3>))
BY
{ (RepUR ``functor-comp functor-curry functor-uncurry`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  SmallCategory
2.  B  :  SmallCategory
3.  C  :  SmallCategory
4.  functor-uncurry(C)  \mmember{}  Functor(FUN(A;FUN(B;C));FUN(A  \mtimes{}  B;C))
5.  functor-curry(A;B)  \mmember{}  Functor(FUN(A  \mtimes{}  B;C);FUN(A;FUN(B;C)))
6.  \mforall{}x:Functor(A  \mtimes{}  B;C).  ((ob(functor-comp(functor-curry(A;B);functor-uncurry(C)))  x)  =  x)
7.  \mforall{}f:Functor(A;FUN(B;C)).  \mforall{}a:cat-ob(A).
          ((ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B)))  f)  a)  =  (ob(f)  a))
8.  x  :  Functor(A  \mtimes{}  B;C)
9.  y  :  Functor(A  \mtimes{}  B;C)
10.  f  :  nat-trans(A  \mtimes{}  B;C;x;y)
11.  A2  :  cat-ob(A)
12.  A3  :  cat-ob(B)
\mvdash{}  (arrow(functor-comp(functor-curry(A;B);functor-uncurry(C)))  x  y  f  <A2,  A3>)  =  (f  <A2,  A3>)


By

---

Latex:
(RepUR  ``functor-comp  functor-curry  functor-uncurry``  0  THEN  Auto)

---

Home Index