---

Step * 2 2 of Lemma functor-curry-iso


1. A : SmallCategory@i'
2. B : SmallCategory@i'
3. C : SmallCategory@i'
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). ((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).
     ((functor-comp(functor-uncurry(C);functor-curry(A;B)) f a) = (f a) ∈ cat-ob(FUN(B;C)))
8. functor-curry(A;B)functor-uncurry(C)=1
9. ∀x:Functor(A;FUN(B;C)). ((functor-comp(functor-uncurry(C);functor-curry(A;B)) x) = x ∈ Functor(A;FUN(B;C)))
⊢ functor-comp(functor-uncurry(C);functor-curry(A;B)) = 1 ∈ Functor(FUN(A;FUN(B;C));FUN(A;FUN(B;C)))
BY
{ ((BLemma `equal-functors` THENW Auto) THEN RepUR ``id_functor`` 0 THEN Try (Trivial) THEN Intros) }

1
1. A : SmallCategory@i'
2. B : SmallCategory@i'
3. C : SmallCategory@i'
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). ((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).
     ((functor-comp(functor-uncurry(C);functor-curry(A;B)) f a) = (f a) ∈ cat-ob(FUN(B;C)))
8. functor-curry(A;B)functor-uncurry(C)=1
9. ∀x:Functor(A;FUN(B;C)). ((functor-comp(functor-uncurry(C);functor-curry(A;B)) x) = x ∈ Functor(A;FUN(B;C)))
10. x : Functor(A;FUN(B;C))@i
11. y : Functor(A;FUN(B;C))@i
12. f : nat-trans(A;FUN(B;C);x;y)@i
⊢ (functor-comp(functor-uncurry(C);functor-curry(A;B)) x y f)
= f
∈ nat-trans(A;FUN(B;C);functor-comp(functor-uncurry(C);functor-curry(A;B)) 
                       x;functor-comp(functor-uncurry(C);functor-curry(A;B)) y)

---

Latex:

---

Latex:

1.  A  :  SmallCategory@i'
2.  B  :  SmallCategory@i'
3.  C  :  SmallCategory@i'
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).  ((functor-comp(functor-curry(A;B);functor-uncurry(C))  x)  =  x)
7.  \mforall{}f:Functor(A;FUN(B;C)).  \mforall{}a:cat-ob(A).
          ((functor-comp(functor-uncurry(C);functor-curry(A;B))  f  a)  =  (f  a))
8.  functor-curry(A;B)functor-uncurry(C)=1
9.  \mforall{}x:Functor(A;FUN(B;C)).  ((functor-comp(functor-uncurry(C);functor-curry(A;B))  x)  =  x)
\mvdash{}  functor-comp(functor-uncurry(C);functor-curry(A;B))  =  1


By

---

Latex:
((BLemma  `equal-functors`  THENW  Auto)  THEN  RepUR  ``id\_functor``  0  THEN  Try  (Trivial)  THEN  Intros)

---

Home Index