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


1. SmallCategory
2. SmallCategory
3. 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. functor-curry(A;B)functor-uncurry(C)=1
9. ∀x:Functor(A;FUN(B;C)). ((ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) x) x ∈ Functor(A;FUN(B;C)))
10. Functor(A;FUN(B;C))
11. Functor(A;FUN(B;C))
12. nat-trans(A;FUN(B;C);x;y)
⊢ (arrow(functor-comp(functor-uncurry(C);functor-curry(A;B))) f)
f
∈ (A1:cat-ob(A) ⟶ (cat-arrow(FUN(B;C)) (ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) x) A1) 
                    (ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) y) A1)))
BY
((FunExt THENA Auto) THEN Reduce 0) }

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


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.  functor-curry(A;B)functor-uncurry(C)=1
9.  \mforall{}x:Functor(A;FUN(B;C)).  ((ob(functor-comp(functor-uncurry(C);functor-curry(A;B)))  x)  =  x)
10.  x  :  Functor(A;FUN(B;C))
11.  y  :  Functor(A;FUN(B;C))
12.  f  :  nat-trans(A;FUN(B;C);x;y)
\mvdash{}  (arrow(functor-comp(functor-uncurry(C);functor-curry(A;B)))  x  y  f)  =  f


By


Latex:
((FunExt  THENA  Auto)  THEN  Reduce  0)




Home Index